オレオレ型推論

gistfile1.hs

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List (partition)
import Control.Arrow (first, second)
import Control.Applicative
infixr 9 :->
infixl 8 >$

type Name = String
data Type = Var Name | Type :-> Type | Rigid Name | Any deriving (Show, Eq, Ord, Read)
data TypeError = Conflict Type Type | Infinite Type deriving (Show)

subst :: Name -> Type -> Type -> Type
subst v t (x :-> y) = subst v t x :-> subst v t y
subst v t (Var v') | v == v' = t
subst _ _ x = x

corresponds :: Type -> Type -> Either TypeError [(Name, Type)]
corresponds Any x = Right []
corresponds (Rigid x) (Rigid x') | x == x' = Right []
corresponds (Rigid x) t = Left $ Conflict (Rigid x) t
corresponds (Var x) (Var x') | x == x' = Right []
corresponds (Var x) t = Right [(x, t)]
corresponds (s :-> t) (u :-> v) = (,) <$> cs <*> (foldr (uncurry subst) t <$> cs >>= flip corresponds v) >>= union
    where
        union (xs, ys) = case (partition $ (==1) . length . snd)
                              $ map (second Set.toList)
                              $ Map.toList $ Map.fromListWith (Set.union)
                              $ map (second Set.singleton) $ xs ++ ys of
                              (_, (_, (x:y:_)):_) -> Left $ Conflict x y
                              (xs, _) -> Right $ map (second head) xs
        
        cs = corresponds s u
corresponds x y = Left $ Conflict y x

apply :: Type -> Type -> Either TypeError Type
apply (a :-> b) x = foldr (uncurry subst) b <$> corresponds a x
apply x y = Left $ Conflict (y :-> Any) x

typeS = (Var "a" :-> Var "b" :-> Var "c") :-> (Var "a" :-> Var "b") :-> Var "a" :-> Var "c"
typeK = Var "a" :-> Var "b" :-> Var "a"
typeI = Var "a" :-> Var "a"

(>$) :: Type -> Type -> Type
(>$) = (either (error.show) id .) . apply