src/Types/Unify.hs · elk

on 5ba2f27 help sign in

elk/src/Types/Unify.hs

57 lines 1.7 kB history raw

2module Unify where

4import Constrain

5import Control.Arrow (second)

6import Types

8unify expr = const expr `fmap` solver (constrain expr) []

10solver [] subs = Right subs

12-------- Destruct Type-constructors --------

14solver ((t1@(ADT n1 ts1) :<: t2@(ADT n2 ts2)) : cs) subs =

15 solver cs subs

16-- if n1 /= n2 then uniError t1 t2 else

17-- solver (zipWith (:<:) ts1 ts2 ++ cs) subs

19solver ((t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2)) : cs) subs =

20 solver cs subs

21-- if n1 /= n2 then uniError t1 t2 else

22-- solver (zipWith (:=:) ts1 ts2 ++ cs) subs

24solver ((LambdaT t1 t2 :<: LambdaT t1' t2') : cs) subs =

25 solver ([ t1 :<: t1', t2 :<: t2' ] ++ cs) subs

27solver ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =

28 solver ([ t1 :=: t1', t2 :=: t2' ] ++ cs) subs

30-------- subtypes --------

32solver ((t :<: VarT x) : cs) subs = solver cs' subs

33 where cs' = if all isSubtype cs then (t :=: VarT x : cs) else (cs ++ [t :<: VarT x])

34solver ((t1 :<: t2) : cs) subs = solver ((t1 :=: t2) : cs) subs

36-------- Type-equality --------

38solver ((VarT x :=: t) : cs) subs =

39 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs

40solver ((t :=: VarT x) : cs) subs =

41 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs

42solver ((t1 :=: t2) : cs) subs =

43 if t1 /= t2 then uniError t1 t2 else solver cs subs

46cSub k v (t1 :=: t2) = tSub k v t1 :=: tSub k v t2

47cSub k v (t1 :<: t2) = tSub k v t1 :<: tSub k v t2

49tSub k v (VarT x) = if k == x then v else (VarT x)

50tSub k v (LambdaT t1 t2) = LambdaT (tSub k v t1) (tSub k v t2)

51tSub _ _ t = t

53isSubtype (_ :<: _) = True

54isSubtype _ = False

56uniError t1 t2 =

57 Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2