milner.hs

{-# LANGUAGE LambdaCase #-}

import Data.List 
    
data Term = Var String | App Term Term | Abs String Term
    deriving (Eq, Ord)


data Type = Const | TVar String | Fun Type Type
    deriving (Eq)

instance Show Term where
  show (Var n)      = n
  show (App e1@(Abs _ _) e2) = "(" ++ show e1 ++ ")" ++ show e2
  show (App e (Var n)) = show e ++ n
  show (App e1 e2) = show e1 ++ "(" ++ show e2 ++ ")"
  show (Abs n e) = "\\" ++ n ++ "." ++ show e


instance Show Type where
  show Const              = "*"
  show (TVar n)       = n
  show (Fun Const t2) = "* -> " ++ show t2
  show (Fun (TVar n) t2) = n ++ " -> " ++ show t2
  show (Fun t1  t2) = "(" ++ show t1 ++ ") -> " ++ show t2


_tvarsStream = [l:show d | d <- [1..10], l <- ['a'..'z']]

identity = Abs "x" (Var "x")

scomb = Abs "x" $ Abs "y" $ Abs "z" $ App (App (Var "x") (Var "z")) (App (Var "y") (Var "z"))

kcomb = (Abs "x" (Abs "y" (Var "x")))

inferType :: Term 
          -> [String] 
          -> [(Term, Type)] 
          -> ([(Term, Type)],  [String])

inferType term@(Var _) names@(n:ns) env = 
    if    term `elem` (map fst env)
    then  (env, names)
    else  ((term, TVar n):env,ns)

inferType term@(Abs x inner) typevars@(tv:tvars) env = 
    if (Var x) `elem` (map fst env)
    then error "FAIL1"
    else case lookup (Var x) env1 of
        Just tp -> ((term, Fun tp tp1):env1, tvs1)
        Nothing -> ((term, Fun (TVar x) tp1):env2, tvs1)
    where
        (env1, tvs1) = inferType inner tvars env
        env2 = (Var x, TVar tv):env1
        Just tp1 = lookup inner env1


getEqs :: Term -> [String] -> [(Term, Type)]
getEqs term@(Var x) (tv:tvs) = [(term, TVar tv)]

getEqs term@(Abs x inner) (tv1:tv2:tvs) = 
    (Var x, TVar tv1)
    :(inner, TVar tv2)
    :(term, Fun (TVar tv2) (TVar tv2))
    :getEqs inner tvs

getEqs term@(App f g) (tv1:tv2:tvs) = 
      (f, Fun (TVar tv1) (TVar tv2))
    : (g, TVar tv1)
    : (term, TVar tv2)
    : getEqs f (tvs1)
    ++ getEqs g (tvs2)
      where l = length tvs `div` 2
            tvs1 = take l tvs
            tvs2 = take l $ reverse tvs

preUnify :: [(Term, Type)] -> [[Type]]
preUnify =  map simplifyEquation
          . map (map snd) 
          . groupBy (\a b -> (fst a) == (fst b)) 
          . sortBy (\a b -> compare (fst a) (fst b))

simplifyEquation ts
    | all (\case 
              TVar s -> True 
              _     -> False) ts = take 1 ts
    | otherwise = ts