SimpleChecker.hs

README.md

A part of Hindley Milner type inference/checker

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

gistfile1.txt

{-# 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")