From e54697f0f401f19d5c5b284768b74e1ff0c3fb93 Mon Sep 17 00:00:00 2001
From: reijix <leon.vatthauer@fau.de>
Date: Sun, 11 Jun 2023 14:24:48 +0200
Subject: [PATCH] Implemented the hindley-milner algorithm for STLC

---
 .gitignore           | 23 +++++++++++++
 LICENSE              | 20 ++++++++++++
 app/Main.hs          | 36 +++++++++++++++++++++
 app/Terms.hs         | 17 ++++++++++
 app/TypeInference.hs | 44 +++++++++++++++++++++++++
 app/Types.hs         | 49 ++++++++++++++++++++++++++++
 app/Unification.hs   | 35 ++++++++++++++++++++
 type-inference.cabal | 77 ++++++++++++++++++++++++++++++++++++++++++++
 8 files changed, 301 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 LICENSE
 create mode 100644 app/Main.hs
 create mode 100644 app/Terms.hs
 create mode 100644 app/TypeInference.hs
 create mode 100644 app/Types.hs
 create mode 100644 app/Unification.hs
 create mode 100644 type-inference.cabal

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..4c9e245
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,23 @@
+dist
+dist-*
+cabal-dev
+*.o
+*.hi
+*.hie
+*.chi
+*.chs.h
+*.dyn_o
+*.dyn_hi
+.hpc
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+*.prof
+*.aux
+*.hp
+*.eventlog
+.stack-work/
+cabal.project.local
+cabal.project.local~
+.HTF/
+.ghc.environment.*
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..6cc1311
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2023 Leon Vatthauer
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
index 0000000..c28a063
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,36 @@
+module Main where
+
+import qualified Data.Map.Strict as Map
+
+import Types ( TermInContext, Type(Arrow, BaseType), emptyContext )
+import Terms ( Term(..) )
+import TypeInference ( inferType )
+
+-- some base types
+int :: Type
+int = BaseType "int"
+string :: Type
+string = BaseType "string"
+
+-- ThProg: sheet 07, exercise 2, 1.
+term1 :: Term
+term1 = Abs "x" $ Abs "y" $ Abs "z" $ App (Var "x") (App (Var "y") (Var "z"))
+exercise1 :: Maybe TermInContext
+exercise1 = inferType emptyContext term1
+
+-- ThProg: sheet 07, exercise 2, 2.
+term2 :: Term
+term2 = Abs "x" $ App (Var "add") (App (Var "length") (Var "x"))
+exercise2 :: Maybe TermInContext
+exercise2 = inferType (Map.fromList [("add", Arrow int (Arrow int int)), ("length", Arrow string int)]) term2
+
+omega :: Term
+omega = Abs "x" $ App (Var "x") (Var "x")
+
+main :: IO ()
+main = do 
+    print exercise1
+    print exercise2
+
+    putStrLn "Trying to type '\\x.xx' in empty context:"
+    print $ inferType emptyContext omega
diff --git a/app/Terms.hs b/app/Terms.hs
new file mode 100644
index 0000000..fbb841f
--- /dev/null
+++ b/app/Terms.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE InstanceSigs #-}
+module Terms where
+
+-- Lambda-Terms
+data Term
+    = Var String
+    | App Term Term
+    | Abs String Term
+    deriving (Eq, Ord)
+instance Show Term where
+    show :: Term -> String
+    show (Var x) = x
+    show (App t1 t2) = show t1 ++ " " ++ go t2
+        where
+            go (App t3 t4) = "(" ++ show t3 ++ " " ++ go t4 ++ ")"
+            go t = show t
+    show (Abs x t) = "\\" ++ x ++ ". " ++ show t
\ No newline at end of file
diff --git a/app/TypeInference.hs b/app/TypeInference.hs
new file mode 100644
index 0000000..96ffa3f
--- /dev/null
+++ b/app/TypeInference.hs
@@ -0,0 +1,44 @@
+module TypeInference where
+
+import Control.Monad.State.Strict
+    ( gets, modify, evalState, State )
+import qualified Data.Map.Strict as Map
+
+import Terms ( Term(..) )
+import Types ( TermInContext(..), Context, Type(TypeVar, Arrow) )
+import Unification ( Unifier, unify, applyMgu )
+
+-- state needed for algorithm W
+newtype PTState = PTState {
+        varCount :: Int
+    }
+type PTMonad = State PTState
+
+-- returns a fresh type var in algorithm W
+getNewTypeVar :: PTMonad String
+getNewTypeVar = do
+    count <- gets varCount
+    modify (\s -> s {varCount = count + 1})
+    return $ 'a' : show count
+
+-- implementation of algorithm W, this builds a list of terms to be unified in the next step
+pt :: Context -> Term -> Type -> PTMonad Unifier
+pt gamma (Var x) alpha = return [(alpha, gamma Map.! x)]
+pt gamma (Abs x t) alpha = do
+    a <- TypeVar <$> getNewTypeVar
+    b <- TypeVar <$> getNewTypeVar
+    result <- pt (Map.insert x a gamma) t b
+    return $ result ++ [(Arrow a b, alpha)]
+pt gamma (App t s) alpha = do
+    a <- TypeVar <$> getNewTypeVar
+    result1 <- pt gamma t (Arrow a alpha)
+    result2 <- pt gamma s a
+    return $ result1 ++ result2
+
+-- infer the type of a term in context (if any)
+inferType :: Context -> Term -> Maybe TermInContext
+inferType ctx term = do
+    let unificationProblem = evalState (pt ctx term (TypeVar "a0")) (PTState 1)
+    mgu <- unify unificationProblem
+    let principalType = applyMgu (TypeVar "a0") mgu
+    return $ TermInContext ctx term principalType
\ No newline at end of file
diff --git a/app/Types.hs b/app/Types.hs
new file mode 100644
index 0000000..1564dcc
--- /dev/null
+++ b/app/Types.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE InstanceSigs #-}
+module Types where
+
+import Data.Map (Map)
+import qualified Data.Map.Strict as Map
+import Data.List ( intercalate )
+
+import Terms ( Term )
+
+-- Types
+data Type
+    = TypeVar String
+    | BaseType String
+    | Arrow Type Type
+    deriving (Eq, Ord)
+instance Show Type where
+    show :: Type -> String
+    show (TypeVar v) = v
+    show (BaseType b) = b
+    show (Arrow t1 t2) = go t1 ++ " -> " ++ show t2
+        where
+            go (Arrow t3 t4) = "(" ++ go t3 ++ " -> " ++ show t4 ++ ")"
+            go t = show t
+
+-- type variables occuring in type
+typeVars :: Type -> [String]
+typeVars (TypeVar v) = [v]
+typeVars (BaseType _) = []
+typeVars (Arrow t1 t2) = typeVars t1 ++ typeVars t2
+
+-- substitute a type for a type variable
+typeSubst :: Type -> String -> Type -> Type
+typeSubst tp@(TypeVar x) y sp = if x == y then sp else tp
+typeSubst tp@(BaseType _) _ _ = tp
+typeSubst (Arrow tp1 tp2) y tp3 = Arrow (typeSubst tp1 y tp3) (typeSubst tp2 y tp3)
+
+-- Contexts
+type Context = Map String Type
+showContext :: Context -> String
+showContext ctx | Map.null ctx = ""
+showContext ctx = "[" ++ intercalate ", " (map (\(name, tp) -> name ++ " : " ++ show tp) $ Map.toList ctx) ++ "]"
+emptyContext :: Context
+emptyContext = Map.empty
+
+-- Term in Context
+data TermInContext = TermInContext Context Term Type
+instance Show TermInContext where
+    show :: TermInContext -> String
+    show (TermInContext ctx term tp) = showContext ctx ++ " |- " ++ show term ++ " : " ++ show tp
\ No newline at end of file
diff --git a/app/Unification.hs b/app/Unification.hs
new file mode 100644
index 0000000..92ddaf1
--- /dev/null
+++ b/app/Unification.hs
@@ -0,0 +1,35 @@
+module Unification where
+
+import Types ( Type(..), typeVars, typeSubst )
+
+type Unifier = [(Type, Type)]
+
+-- unification algorithm of martelli montanari
+unify :: Unifier -> Maybe Unifier
+unify [] = Just []
+-- (delete)
+unify ((TypeVar x, TypeVar y) : rest) | x == y = unify rest
+-- (decomp)
+unify ((Arrow t1 t2, Arrow t1' t2') : rest) = unify $ [(t1, t1'), (t2, t2')] ++ rest
+unify ((BaseType b1, BaseType b2) : rest) | b1 == b2 = unify rest
+-- (conflict)
+unify ((BaseType b1, BaseType b2) : _) | b1 /= b2 = Nothing
+-- (orient)
+unify ((Arrow t1 t2, TypeVar x) : rest) = unify $ (TypeVar x, Arrow t1 t2) : rest
+unify ((BaseType b, TypeVar x) : rest) = unify $ (TypeVar x, BaseType b) : rest
+-- (occurs)
+unify ((TypeVar x, t) : _) | x `elem` typeVars t && TypeVar x /= t = Nothing
+-- (elim)
+unify ((TypeVar x, t) : rest) | notElem x (typeVars t) && x `elem` concatMap (\(t1, t2) -> typeVars t1 ++ typeVars t2) rest = unify $ (TypeVar x, t) : map (\(t1, t2) -> (typeSubst t1 x t, typeSubst t2 x t)) rest
+-- descent
+unify ((t, s) : rest) = do
+    rest' <- unify rest
+    return $ (t, s) : rest'
+
+-- apply a mgu to some type
+applyMgu :: Type -> Unifier -> Type
+applyMgu (TypeVar x) [] = TypeVar x
+applyMgu (TypeVar x) ((TypeVar y, tp) : rest) = if x == y then tp else applyMgu (TypeVar x) rest
+applyMgu (BaseType b) _ = BaseType b
+applyMgu (Arrow t1 t2) mgu = Arrow (applyMgu t1 mgu) (applyMgu t2 mgu)
+applyMgu _ (tp : _) = error $ "Non primitive type '" ++ show tp ++ "' on left side of mgu"
\ No newline at end of file
diff --git a/type-inference.cabal b/type-inference.cabal
new file mode 100644
index 0000000..abdf971
--- /dev/null
+++ b/type-inference.cabal
@@ -0,0 +1,77 @@
+cabal-version:      3.0
+-- The cabal-version field refers to the version of the .cabal specification,
+-- and can be different from the cabal-install (the tool) version and the
+-- Cabal (the library) version you are using. As such, the Cabal (the library)
+-- version used must be equal or greater than the version stated in this field.
+-- Starting from the specification version 2.2, the cabal-version field must be
+-- the first thing in the cabal file.
+
+-- Initial package description 'type-inference' generated by
+-- 'cabal init'. For further documentation, see:
+--   http://haskell.org/cabal/users-guide/
+--
+-- The name of the package.
+name:               type-inference
+
+-- The package version.
+-- See the Haskell package versioning policy (PVP) for standards
+-- guiding when and how versions should be incremented.
+-- https://pvp.haskell.org
+-- PVP summary:     +-+------- breaking API changes
+--                  | | +----- non-breaking API additions
+--                  | | | +--- code changes with no API change
+version:            0.1.0.0
+
+-- A short (one-line) description of the package.
+synopsis:
+    A small implementation of the hindley milner type inference algorithm (Algorithm W)
+
+-- A longer description of the package.
+-- description:
+
+-- The license under which the package is released.
+license:            MIT
+
+-- The file containing the license text.
+license-file:       LICENSE
+
+-- The package author(s).
+author:             Leon Vatthauer
+
+-- An email address to which users can send suggestions, bug reports, and patches.
+-- maintainer:
+
+-- A copyright notice.
+-- copyright:
+category:           Language
+build-type:         Simple
+
+-- Extra source files to be distributed with the package, such as examples, or a tutorial module.
+-- extra-source-files:
+
+common warnings
+    ghc-options: -Wall
+
+executable type-inference
+    -- Import common warning flags.
+    import:           warnings
+
+    -- .hs or .lhs file containing the Main module.
+    main-is:          Main.hs
+
+    -- Modules included in this executable, other than Main.
+    -- other-modules:
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends:    base ^>=4.16.4.0, containers, mtl
+
+    -- Directories containing source files.
+    hs-source-dirs:   app
+
+    other-modules:    Terms, Types, Unification, TypeInference
+
+    -- Base language which the package is written in.
+    default-language: Haskell2010