Commit 8935b656 authored by Levente Kurusa's avatar Levente Kurusa
Browse files

Add Lev's solutions



Signed-off-by: default avatarLevente Kurusa <levex@linux.com>
parent d881a0f1
-- Levente Kurusa
import Control.Applicative
import Control.Arrow
import Control.Monad
import Data.List
import Data.Maybe
import Debug.Trace
-- general notes
-- (<$>) = fmap
-- ~(pattern) = lazy pattern matching
-- join => from Control.Monad
-- join :: Monad m => m (m a) -> m a (functions are monads)
-- (***) => from Control.Arrow
-- (***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c')
-- allows you to split a computation. functions are arrows.
-- only here to silence hlint
main = forever $ return ()
data Expr = Number Int |
Boolean Bool |
Id String |
Prim String |
Cond Expr Expr Expr |
App Expr Expr |
Fun String Expr
deriving (Eq, Show)
data Type = TInt |
TBool |
TFun Type Type |
TVar String |
TErr
deriving (Eq, Show)
showT :: Type -> String
showT TInt
= "Int"
showT TBool
= "Bool"
showT (TFun t t')
= "(" ++ showT t ++ " -> " ++ showT t' ++ ")"
showT (TVar a)
= a
showT TErr
= "Type error"
type TypeTable = [(String, Type)]
type TEnv
= TypeTable -- i.e. [(String, Type)]
type Sub
= TypeTable -- i.e. [(String, Type)]
-- Built-in function types...
primTypes :: TypeTable
primTypes
= [("+", TFun TInt (TFun TInt TInt)),
(">", TFun TInt (TFun TInt TBool)),
("==", TFun TInt (TFun TInt TBool)),
("not", TFun TBool TBool)]
------------------------------------------------------
-- PART I
-- Pre: The search item is in the table
lookUp :: Eq a => a -> [(a, b)] -> b
lookUp
= (.) fromJust . lookup
tryToLookUp :: Eq a => a -> b -> [(a, b)] -> b
tryToLookUp val def p
= case lookup val p of
Nothing -> def
Just v -> v
-- Pre: The given value is in the table
reverseLookUp :: Eq b => b -> [(a, b)] -> [a]
reverseLookUp x d
= fst <$> filter ((== x) . snd) d
occurs :: String -> Type -> Bool
occurs s (TVar v)
= s == v
occurs s (TFun f1 f2)
= occurs s f1 || occurs s f2
occurs _ _
= False
------------------------------------------------------
-- PART II
-- Pre: There are no user-defined functions (constructor Fun)
-- Pre: All type variables in the expression have a binding in the given
-- type environment
inferType :: Expr -> TEnv -> Type
inferType (Number _) _
= TInt
inferType (Boolean _) _
= TBool
inferType (Id s) e
= lookUp s e
inferType (Prim s) _
= lookUp s primTypes
inferType (Cond p e1 e2) env
| inferType p env /= TBool = TErr
| inferType e1 env /= e2t = TErr
| otherwise = e2t
where
e2t = inferType e2 env
inferType (App f a) env
| not . isFun $ ft = TErr
| fa /= inferType a env = TErr
| otherwise = fr
where
~ft@(TFun fa fr) = inferType f env
at = inferType a env
isFun :: Type -> Bool
isFun (TFun _ _) = True
isFun _ = False
------------------------------------------------------
-- PART III
applySub :: Sub -> Type -> Type
applySub sub t@(TVar str)
= tryToLookUp str t sub
applySub sub (TFun t1 t2)
= TFun (applySub sub t1) (applySub sub t2)
applySub _ t
= t
unify :: Type -> Type -> Maybe Sub
unify t t'
= unifyPairs [(t, t')] []
unifyPairs :: [(Type, Type)] -> Sub -> Maybe Sub
unifyPairs ((TInt, TInt) : ts) sub
= unifyPairs ts sub
unifyPairs ((TBool, TBool) : ts) sub
= unifyPairs ts sub
unifyPairs (t@(TVar v, TVar v') : ts) sub
| v == v' = unifyPairs ts sub
| otherwise = unifyVars (TVar v) v' ts sub
unifyPairs ((t, TVar v) : ts) sub
= unifyVars t v ts sub
unifyPairs ((TVar v, t) : ts) sub
= unifyVars t v ts sub
unifyPairs ((TFun t1 t2, TFun t1' t2') : ts) sub
= unifyPairs ((t1, t1') : (t2, t2') : ts) sub
unifyPairs (_ : _) _
= Nothing
unifyPairs [] sub
= Just sub
unifyVars :: Type -> String -> [(Type, Type)] -> Sub -> Maybe Sub
unifyVars t v ts sub
| v `occurs` t = Nothing
| otherwise = unifyPairs nts (subst : sub)
where
nts = join (***) (applySub [subst]) <$> ts
subst = (v, t)
------------------------------------------------------
-- PART IV
updateTEnv :: TEnv -> Sub -> TEnv
updateTEnv tenv tsub
= map modify tenv
where
modify (v, t) = (v, applySub tsub t)
combine :: Sub -> Sub -> Sub
combine sNew sOld
= sNew ++ updateTEnv sOld sNew
-- In combineSubs [s1, s2,..., sn], s1 should be the *most recent* substitution
-- and will be applied *last*
combineSubs :: [Sub] -> Sub
combineSubs
= foldr1 combine
inferPolyType :: Expr -> Type
inferPolyType (Number _)
= TInt
inferPolyType (Boolean _)
= TBool
inferPolyType (Prim s)
= lookUp s primTypes
inferPolyType e
= t
where
(_, t, _) = inferPolyType' e [] 1
-- You may optionally wish to use one of the following helper function declarations
-- as suggested in the specification.
-- inferPolyType' :: Expr -> TEnv -> [String] -> (Sub, Type, [String])
-- inferPolyType'
-- = undefined
inferPolyType' :: Expr -> TEnv -> Int -> (Sub, Type, Int)
inferPolyType' (Number _) _ i
= ([], TInt, i)
inferPolyType' (Boolean _) _ i
= ([], TBool, i)
inferPolyType' (Id s) env i
| ot == TErr = ([(s, nt)], nt, i + 1)
| otherwise = ([], ot, i)
where
ot = tryToLookUp s TErr env
nt = TVar . mkVarName $ i
inferPolyType' (Prim s) _ i
= ([], lookUp s primTypes, i)
inferPolyType' (Fun x e) env i
| te == TErr = ([], TErr, i)
| otherwise = ([], TFun tx te, i)
where
nenv = (x, nvar) : env
(sub, te, ni) = inferPolyType' e nenv (i + 1)
nvar = TVar . mkVarName $ i
tx = applySub sub nvar
inferPolyType' (App f e) env i
| isNothing unified = ([], TErr, i)
| otherwise = (rsub, rt, ri + 1)
where
(sub, ft, ni) = inferPolyType' f env (i + 1)
(esub, et, eni) = inferPolyType' e (updateTEnv env sub) ni
var = (TVar $ mkVarName i)
unified = unify ft (TFun et var)
rsub = combineSubs $ (fromJust unified) : esub : sub : []
ri = eni
rt = applySub (fromJust unified) var
-- Cond is work in progress
inferPolyType' (Cond p q r) env i
= ([], pt, i)
where
(psub, pt, p_i) = inferPolyType' p env i
mkVarName :: Int -> String
mkVarName n
= "a" ++ show n
------------------------------------------------------
-- Monomorphic type inference test cases from Table 1...
env :: TEnv
env = [("x",TInt),("y",TInt),("b",TBool),("c",TBool)]
ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8 :: Expr
type1, type2, type3, type4, type5, type6, type7, type8 :: Type
ex1 = Number 9
type1 = TInt
ex2 = Boolean False
type2 = TBool
ex3 = Prim "not"
type3 = TFun TBool TBool
ex4 = App (Prim "not") (Boolean True)
type4 = TBool
ex5 = App (Prim ">") (Number 0)
type5 = TFun TInt TBool
ex6 = App (App (Prim "+") (Boolean True)) (Number 5)
type6 = TErr
ex7 = Cond (Boolean True) (Boolean False) (Id "c")
type7 = TBool
ex8 = Cond (App (Prim "==") (Number 4)) (Id "b") (Id "c")
type8 = TErr
------------------------------------------------------
-- Unification test cases from Table 2...
u1a, u1b, u2a, u2b, u3a, u3b, u4a, u4b, u5a, u5b, u6a, u6b :: Type
sub1, sub2, sub3, sub4, sub5, sub6 :: Maybe Sub
u1a = TFun (TVar "a") TInt
u1b = TVar "b"
sub1 = Just [("b",TFun (TVar "a") TInt)]
u2a = TFun TBool TBool
u2b = TFun TBool TBool
sub2 = Just []
u3a = TFun (TVar "a") TInt
u3b = TFun TBool TInt
sub3 = Just [("a",TBool)]
u4a = TBool
u4b = TFun TInt TBool
sub4 = Nothing
u5a = TFun (TVar "a") TInt
u5b = TFun TBool (TVar "b")
sub5 = Just [("b",TInt),("a",TBool)]
u6a = TFun (TVar "a") (TVar "a")
u6b = TVar "a"
sub6 = Nothing
------------------------------------------------------
-- Polymorphic type inference test cases from Table 3...
ex9, ex10, ex11, ex12, ex13, ex14 :: Expr
type9, type10, type11, type12, type13, type14 :: Type
ex9 = Fun "x" (Boolean True)
type9 = TFun (TVar "a1") TBool
ex10 = Fun "x" (Id "x")
type10 = TFun (TVar "a1") (TVar "a1")
ex11 = Fun "x" (App (Prim "not") (Id "x"))
type11 = TFun TBool TBool
ex12 = Fun "x" (Fun "y" (App (Id "y") (Id "x")))
type12 = TFun (TVar "a1") (TFun (TFun (TVar "a1") (TVar "a3")) (TVar "a3"))
ex13 = Fun "x" (Fun "y" (App (App (Id "y") (Id "x")) (Number 7)))
type13 = TFun (TVar "a1") (TFun (TFun (TVar "a1") (TFun TInt (TVar "a3")))
(TVar "a3"))
ex14 = Fun "x" (Fun "y" (App (Id "x") (Prim "+")))
type14 = TFun (TFun (TFun TInt (TFun TInt TInt)) (TVar "a3"))
(TFun (TVar "a2") (TVar "a3"))
-- Test for Cond
ex15 = Cond (App (Prim "not") (Boolean False)) (Boolean True) (Boolean False)
type15 = TBool
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment