36 lines
968 B
Haskell
36 lines
968 B
Haskell
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
|