From 56bfdd230d22d3dbf96bbc21ae483b28b41c27f5 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 19 Jul 2018 15:01:13 +0200
Subject: [PATCH] inference from haskell writing

---
 infer.dcl |  2 ++
 infer.icl | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 52 insertions(+), 5 deletions(-)

diff --git a/infer.dcl b/infer.dcl
index 1c1d294..c284a33 100644
--- a/infer.dcl
+++ b/infer.dcl
@@ -9,3 +9,5 @@ from Data.Map import :: Map
 	| CharType
 	| Arrow Type Type
 :: Scheme = Forall [String] Type
+
+infer :: Expression -> Infer Type
diff --git a/infer.icl b/infer.icl
index fadc684..a9a4108 100644
--- a/infer.icl
+++ b/infer.icl
@@ -10,14 +10,17 @@ import Data.Func
 import Data.Either
 import Data.List
 import Data.Maybe
+import Data.GenEq
 import Control.Applicative
 import Control.Monad
 import Control.Monad.Trans
 import qualified Control.Monad.State as MS
-import Control.Monad.RWST
+import Control.Monad.State => qualified gets, put, modify
+import Control.Monad.RWST => qualified put
 
 import ast
 
+derive gEq Type
 :: TypeEnv :== 'DM'.Map String Scheme
 :: Constraint :== (Type, Type)
 :: Subst :== 'DM'.Map String Type
@@ -25,7 +28,11 @@ import ast
 :: Infer a :== RWST TypeEnv [Constraint] InferState (Either TypeError) a
 :: InferState = { count :: Int }
 :: Solve a :== 'MS'.StateT Unifier (Either TypeError) a
-:: TypeError = UnboundVariable String
+:: TypeError
+	= UnboundVariable String
+	| UnificationFail Type Type
+	| UnificationMismatch [Type] [Type]
+	| InfiniteType String Type
 
 nullSubst :: Subst
 nullSubst = 'DM'.newMap
@@ -40,7 +47,7 @@ letters :: [String]
 letters = map toString $ [1..] >>= flip replicateM ['a'..'z']
 
 fresh :: Infer Type
-fresh = get >>= \s=:{count}->put {s & count=count + 1} >>| pure (VarType $ letters !! count)
+fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (VarType $ letters !! count)
 
 lookupEnv :: String -> Infer Type
 lookupEnv x = asks ('DM'.get x)
@@ -72,8 +79,12 @@ where
 	ftv t = foldr ('DS'.union o ftv) 'DS'.newSet t
 
 instance Substitutable TypeEnv where
-  apply s env = fmap (apply s) env
-  ftv env = ftv $ 'DM'.elems env
+	apply s env = fmap (apply s) env
+	ftv env = ftv $ 'DM'.elems env
+
+instance Substitutable Constraint where
+	apply s (t1, t2) = (apply s t1, apply s t2)
+	ftv (t1, t2) = 'DS'.union (ftv t1) (ftv t2)
 
 instantiate ::  Scheme -> Infer Type
 instantiate (Forall as t) = mapM (const fresh) as
@@ -108,3 +119,37 @@ infer (Code c) = fresh >>= \v->pure case c of
 	"div" = Arrow v (Arrow v v)
 	"and" = Arrow v (Arrow v BoolType)
 	"or"  = Arrow v (Arrow v BoolType)
+
+unifies :: Type Type -> Solve Unifier
+unifies t1 t2
+	| t1 === t2 = pure ('DM'.newMap, [])
+unifies (VarType v) t = tbind v t
+unifies t (VarType v) = tbind v t
+unifies (Arrow t1 t2) (Arrow t3 t4) = unifyMany [t1, t2] [t3, t4]
+unifies t1 t2 = liftT (Left (UnificationFail t1 t2))
+
+unifyMany :: [Type] [Type] -> Solve Unifier
+unifyMany [] [] = pure ('DM'.newMap, [])
+unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
+	>>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
+	>>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
+unifyMany t1 t2 = liftT (Left (UnificationMismatch t1 t2))
+
+(`compose`) infix 1 :: Subst Subst -> Subst
+(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
+
+tbind ::  String Type -> Solve Unifier
+tbind a t
+	| t === VarType a = pure ('DM'.newMap, [])
+	| occursCheck a t = liftT $ Left $ InfiniteType a t
+	= pure $ ('DM'.singleton a t, [])
+
+occursCheck ::  String a -> Bool | Substitutable a
+occursCheck a t = 'DS'.member a $ ftv t
+
+solver :: Solve Subst
+solver = getState >>= \(su, cs)->case cs of
+	[] = pure su
+	[(t1, t2):cs0] = unifies t1 t2
+		>>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
+		>>| solver
-- 
2.20.1