Checks only applications, there are no lets or lambda abstractions :)
Control.Unification comes from unification-fd
package.
Unifier.Unifier
and Unifier.Restricted
can be copy-pasted from https://github.com/nponeccop/HNC/tree/master/Unifier
Checks only applications, there are no lets or lambda abstractions :)
Control.Unification comes from unification-fd
package.
Unifier.Unifier
and Unifier.Restricted
can be copy-pasted from https://github.com/nponeccop/HNC/tree/master/Unifier
{-# LANGUAGE LambdaCase #-} | |
import Unifier.Unifier | |
import Unifier.Restricted | |
import Control.Monad.Identity | |
import Control.Unification (freeVar, freshen, applyBindings) | |
import Control.Unification.IntVar | |
import Control.Monad.Trans | |
import qualified Data.Map as M | |
data Expression = Atom String | App Expression Expression | |
check :: Lib -> Expression -> Stack Type | |
check lib = \case | |
Atom a -> look lib a | |
App a b -> do | |
UTerm (TT [argA, res]) <- check lib a | |
argB <- check lib b | |
unify argA argB | |
return res | |
-- Boilerplate | |
type Stack = WithExcept (WithEnv Identity) | |
type Lib = M.Map String Type | |
run x = runIdentity $ runIntBindingT x | |
look :: Lib -> String -> Stack Type | |
look b a = case M.lookup a b of Just a -> freshen a | |
runCheck x = run $ runErrorT2 $ do | |
lib <- lift makeLib | |
check lib x >>= applyBindings | |
-- Examples | |
makeLib :: WithEnv Identity Lib | |
makeLib = do | |
a <- UVar <$> freeVar | |
b <- UVar <$> freeVar | |
return $ UTerm <$> M.fromList | |
[ ("id", TT [a, a]) | |
, ("one", T "Int") | |
, ("const", TT [a, UTerm $ TT [b, a]]) | |
] | |
check1 = Atom "one" | |
check2 = App (Atom "const") (Atom "one") | |
check3 = App (App (Atom "const") (Atom "one")) (Atom "id") |