I've written an implementation of the Hindley-Milner type system as a "Core" language for use in writing compilers of typed functional languages. This is meant to be used as a library by compilers of more complex languages, providing an in-memory intermediate representation after parsing, type inference, and typechecking in more elaborate systems.
Goals:
Provide a correct type system with literal Int and Bool types, as well as if-then-else expressions.
Allow evaluation of well-typed expressions in the language.
Deliberate non-goals:
- Provide type inference.
- Allow Haskell-style typeclasses.
- Provide parsing from text.
- Provide end-to-end typing and evaluation.
The code is currently separated into three modules, as well as one module for testing. I'm primarily looking for general stylistic critique, as well as making sure the typechecking algorithm is correct. One other specific issue I'd like feedback on is how to handle partial functions in the Eval module; they're intentionally partial, as only ill-typed expressions shouldn't evaluate successfully, but I'm not sure how best to handle this and what sort of API to provide.
Syntax.hs:
module Syntax where
type Identifier = String
data Literal = LInt Integer
| LBool Bool
deriving (Show, Eq)
--division deliberately omitted to avoid dealing with integer division complexity
data BinOp = Add
| Subtract
| Multiply
| Equals
deriving (Show, Eq)
data CoreExpr = Var Identifier
| Lit Literal
| Apply CoreExpr CoreExpr --function, then argument
| Lambda Identifier Type CoreExpr --name of argument, type of argument, then body
| Let Identifier CoreExpr CoreExpr --let a b e is equivalent to let a = b in e
| If CoreExpr CoreExpr CoreExpr --if cond a b is equivalent to if cond then a else b
| Op BinOp CoreExpr CoreExpr
| Fix CoreExpr
deriving (Show, Eq)
type Decl = (String, CoreExpr) -- top-level let declaration
data Program = Program [Decl] CoreExpr -- last CoreExpr is the main function
type TypeVariable = String
data Type = TVariable TypeVariable
| TConstructor String
| TFunction Type Type
deriving (Show, Eq)
tInt, tBool :: Type
tInt = TConstructor "Int"
tBool = TConstructor "Bool"
Type.hs:
{-# LANGUAGE LambdaCase #-}
module Type (
TypeError(..)
, typeOf
) where
-- need the MTL versions of these libraries for auto-lifting
import Control.Monad.Except
import Control.Monad.Reader
import qualified Data.Map as Map
import Syntax
data TypeError = Mismatch Type Type
| NotFunction Type -- attempting to apply a non-function to an argument, or fix a non-function
| NotInScope Identifier
deriving (Show, Eq)
type TypingEnv = Map.Map Identifier Type
type TypingSubstitution = Map.Map TypeVariable Type
-- monad stack to store typing environment, typing errors
type Check a = ExceptT TypeError (Reader (TypingEnv, TypingSubstitution)) a
extendEnv :: Identifier -> Type -> TypingEnv -> TypingEnv
extendEnv = Map.insert
extendSub :: TypeVariable -> Type -> TypingSubstitution -> TypingSubstitution
extendSub = Map.insert
-- add name: typ to the environment, then run a typecheck
checkInEnv :: Identifier -> Type -> Check a -> Check a
checkInEnv name typ = local $ \(env, sub) -> (extendEnv name typ env, sub)
lookupVar :: Identifier -> Check Type
lookupVar name = do
(env, _) <- ask
case Map.lookup name env of
Just t -> return t
Nothing -> throwError $ NotInScope name
typeCheck :: CoreExpr -> Check Type
typeCheck = \case
Lit (LInt _) -> return tInt
Lit (LBool _) -> return tBool
Var name -> lookupVar name
Lambda name typ body -> do
rhs <- checkInEnv name typ (typeCheck body)
return $ TFunction typ rhs
Apply func arg -> do
funcType <- typeCheck func
argType <- typeCheck arg
(_, subst) <- ask
case funcType of
TFunction a b -> case a of
TVariable tvar -> return $ applySubstitution (extendSub tvar argType subst) b
-- TConstructor, TFunction
_ -> if a == argType
then return b
else throwError $ Mismatch argType a
nonFunc -> throwError $ NotFunction nonFunc
Let name value body -> do
valueType <- typeCheck value
checkInEnv name valueType (typeCheck body)
If cond tr fl -> do
condType <- typeCheck cond
trueType <- typeCheck tr
falseType <- typeCheck fl
if condType /= tBool
then throwError $ Mismatch condType tBool
else if trueType /= falseType
then throwError $ Mismatch trueType falseType
else return trueType
Op op left right -> do
leftType <- typeCheck left
rightType <- typeCheck right
case op of
-- only define equality on ints
Equals -> if leftType == tInt
then if rightType == tInt
then return tBool
else throwError $ Mismatch tInt rightType
else throwError $ Mismatch leftType tInt
-- Add, Subtract, Multiply
_ -> if leftType == tInt
then if rightType == tInt
then return tInt
else throwError $ Mismatch tInt rightType
else throwError $ Mismatch leftType tInt
Fix expr -> do
innerType <- typeCheck expr
case innerType of
TFunction a b | a == b -> return a
| otherwise -> throwError $ Mismatch a b
nonFunc -> throwError $ NotFunction nonFunc
-- make this a typeclass method later, when it can be applied to other type-containing structures?
applySubstitution :: TypingSubstitution -> Type -> Type
applySubstitution subst typ = case typ of
TVariable tvar -> case Map.lookup tvar subst of
Just typ' -> typ'
Nothing -> typ
TConstructor _ -> typ
TFunction tArg tBody -> TFunction (applySubstitution subst tArg) (applySubstitution subst tBody)
runTypecheck :: (TypingEnv, TypingSubstitution) -> Check a -> Either TypeError a
runTypecheck (env, sub) checker = runReader (runExceptT checker) (env, sub)
typeOf :: CoreExpr -> Either TypeError Type
typeOf expr = runTypecheck (Map.empty, Map.empty) (typeCheck expr)
Eval.hs:
{-# LANGUAGE LambdaCase #-}
module Eval (
eval
, evalProgram
, Value(..)
) where
import Syntax
import qualified Data.Map as Map
type Environment = Map.Map String Value
data Value = VInt Integer
| VBool Bool
| VClosure String CoreExpr Environment
deriving Eq
instance Show Value where
show (VInt n) = show n
show (VBool b) = show b
show (VClosure{}) = "<closure>"
eval :: Environment -> CoreExpr -> Value
eval env = \case
Lit (LInt n) -> VInt n
Lit (LBool b) -> VBool b
Var name -> case Map.lookup name env of
(Just val) -> val
Nothing -> error $ "Variable " ++ show name ++ " not in scope"
-- ignore type; we presume it's already been typechecked
Lambda name _ body -> VClosure name body env
Apply func arg -> apply (eval env func) (eval env arg)
Let name value body -> eval env' body
where env' = Map.insert name (eval env value) env
If cond tr fl -> case eval env cond of
VBool check -> if check then eval env tr else eval env fl
_ -> error "Non-boolean used as condition"
Op op left right -> case op of
Add -> VInt $ m + n
Subtract -> VInt $ m - n
Multiply -> VInt $ m * n
Equals -> VBool $ m == n
where (VInt m) = eval env left --accept that these are partial for now,
(VInt n) = eval env right --will eliminate possibility of error with typechecker later
Fix expr -> eval env (Apply expr (Fix expr))
--beta reduction: replace a bound variable in the lambda with the argument to the lambda
apply :: Value -> Value -> Value
apply (VClosure name body env) arg = eval (Map.insert name arg env) body
apply _ _ = error "Tried to apply a non-closure"
evalProgram :: Program -> Value
evalProgram (Program decls main) = eval populatedEnv main
where populatedEnv = foldr addDecl Map.empty decls
addDecl (ident, expr) env = Map.insert ident (eval env expr) env
Test.hs:
import qualified Data.Map as Map
import Hedgehog ((===))
import qualified Hedgehog as HH
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Test.Tasty
import Test.Tasty.ExpectedFailure
import Test.Tasty.Hedgehog
import Test.Tasty.HUnit
import Eval
import Syntax
import Type
main = defaultMain tests
tests :: TestTree
tests = testGroup "All Tests" [properties, units]
-- property-based testing
properties :: TestTree
properties = testGroup "Properties" [ combinators, evaluation, typechecking ]
combinators :: TestTree
combinators = testGroup "Lambda calculus combinators" [identity, kConst, skki]
evaluation :: TestTree
evaluation = testGroup "Basic evaluation" [ifTrue, ifFalse, addOp, subOp, mulOp, eqOp]
typechecking :: TestTree
typechecking = testGroup "Type checking" [ intType
, boolType
, appliedFuncType
, arithOpType
, mismatchedArithOpLeft
, mismatchedArithOpRight
]
identity = testProperty "I combinator is identity" propIdentity
kConst = testProperty "K combinator is const" propKConst
skki = testProperty "SKK == I" propSKKI
ifTrue = testProperty "if true a b == a" propIfTrue
ifFalse = testProperty "if false a b == b" propIfFalse
addOp = testProperty "Add a b == a + b" propAddOp
subOp = testProperty "Subtract a b == a - b" propSubOp
mulOp = testProperty "Multiply a b == a * b" propMulOp
eqOp = testProperty "Equals a b == (a == b)" propEqOp
intType = testProperty "typeof (any integer) == tInt" propIntType
boolType = testProperty "typeof (any boolean) == tBool" propBoolType
appliedFuncType = testProperty "typeof (\\x : Int -> x) (any integer) == tInt" propAppliedFunc
arithOpType = testProperty "typeof (any Add/Subtract/Multiply) (any int) (any int) == tInt" propArithOp
mismatchedArithOpLeft = testProperty "typeof (Add/Subtract/Multiply) (any bool) (any int) == Mismatch tBool tInt" propArithMismatchLeft
mismatchedArithOpRight = testProperty "typeof (Add/Subtract/Multiply) (any int) (any bool) == Mismatch tInt tBool" propArithMismatchRight
-- generators
genAnyInt :: HH.Gen Integer
genAnyInt = Gen.integral (Range.linear (-10000) 10000)
genArithOp :: HH.Gen BinOp
genArithOp = Gen.element [Add, Subtract, Multiply]
-- lambda calculus combinators
iComb :: CoreExpr
iComb = Lambda "x" (TVariable "a") (Var "x")
kComb :: CoreExpr
kComb = Lambda "x" (TVariable "a") (Lambda "y" (TVariable "b") (Var "x"))
sComb :: CoreExpr
sComb = Lambda "f" (TFunction (TVariable "a") (TFunction (TVariable "b") (TVariable "c"))) (Lambda "g" (TFunction (TVariable "a") (TVariable "b")) (Lambda "x" (TVariable "a") (Apply (Apply (Var "f") (Var "x")) (Apply (Var "g") (Var "x")))))
-- tests
propIdentity :: HH.Property
propIdentity = HH.property $ do
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
let vn = VInt n
eval (Map.empty) (Apply iComb ln) === vn
propKConst :: HH.Property
propKConst = HH.property $ do
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
let vm = VInt m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
eval (Map.empty) (Apply (Apply kComb lm) ln) === vm
propSKKI :: HH.Property
propSKKI = HH.property $ do
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
let vn = VInt n
eval (Map.empty) (Apply (Apply (Apply sComb kComb) kComb) ln) === vn
propIfTrue :: HH.Property
propIfTrue = HH.property $ do
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
let vm = VInt m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
eval Map.empty (If (Lit (LBool True)) lm ln) === vm
propIfFalse :: HH.Property
propIfFalse = HH.property $ do
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
let vn = VInt n
eval Map.empty (If (Lit (LBool False)) lm ln) === vn
propAddOp :: HH.Property
propAddOp = HH.property $ do
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
eval Map.empty (Op Add lm ln) === VInt (m + n)
propSubOp :: HH.Property
propSubOp = HH.property $ do
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
eval Map.empty (Op Subtract lm ln) === VInt (m - n)
propMulOp :: HH.Property
propMulOp = HH.property $ do
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
eval Map.empty (Op Multiply lm ln) === VInt (m * n)
propEqOp :: HH.Property
propEqOp = HH.property $ do
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
eval Map.empty (Op Equals lm ln) === VBool (m == n)
propIntType :: HH.Property
propIntType = HH.property $ do
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
typeOf ln === Right tInt
propBoolType :: HH.Property
propBoolType = HH.property $ do
b <- HH.forAll Gen.bool
let lb = Lit . LBool $ b
typeOf lb === Right tBool
propAppliedFunc :: HH.Property
propAppliedFunc = HH.property $ do
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
typeOf (Apply (Lambda "x" tInt (Var "x")) ln) === Right tInt
propArithOp :: HH.Property
propArithOp = HH.property $ do
op <- HH.forAll genArithOp
m <- HH.forAll genAnyInt
let lm = Lit . LInt $ m
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
typeOf (Op op lm ln) === Right tInt
propArithMismatchLeft :: HH.Property
propArithMismatchLeft = HH.property $ do
op <- HH.forAll genArithOp
b <- HH.forAll Gen.bool
let lb = Lit . LBool $ b
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
typeOf (Op op lb ln) === Left (Mismatch tBool tInt)
propArithMismatchRight :: HH.Property
propArithMismatchRight = HH.property $ do
op <- HH.forAll genArithOp
n <- HH.forAll genAnyInt
let ln = Lit . LInt $ n
b <- HH.forAll Gen.bool
let lb = Lit . LBool $ b
typeOf (Op op ln lb) === Left (Mismatch tInt tBool)
-- unit testing
units :: TestTree
units = testGroup "Unit Tests" [letExample, fixExample, typeTests, programExample]
letExample :: TestTree
letExample = testCase "let x = 3 in x evaluates to 3" $ do
let letExpression = Let "x" (Lit (LInt 3)) (Var "x")
eval Map.empty letExpression @?= VInt 3
fixExample :: TestTree
fixExample = testCase "factorial 3 == 6" $ do
let factorial = Fix (Lambda "fact" (TFunction tInt tInt) (Lambda "x" tInt (If (Op Equals (Var "x") (Lit (LInt 0))) (Lit (LInt 1)) (Op Multiply (Var "x") (Apply (Var "fact") (Op Subtract (Var "x") (Lit (LInt 1))))))))
eval Map.empty (Apply factorial (Lit (LInt 3))) @?= VInt 6
typeTests :: TestTree
typeTests = testGroup "Unit tests of typechecker" [ funcAndVar
, outOfScope
, appliedToWrongType
, applyNonFunction
, nonBoolIfCondition
, mismatchedThenElse
, mismatchedEqualsLeft
, mismatchedEqualsRight
, correctIfElse
, correctEquals
, correctFix
, fixMismatch
, fixNonFunction
, correctApply
, correctLet
, letScopeCheck
, letInnerError
, letOuterError
, polymorphicLambda
, polymorphicLambdaMulti
, polymorphicApplied
, polymorphicAppliedMulti
, polymorphicPartialApplied
]
funcAndVar :: TestTree
funcAndVar = testCase "typeof (\\x : Int -> x) = TFunction tInt tInt" $ do
let lambdaExpr = Lambda "x" tInt (Var "x")
typeOf lambdaExpr @?= Right (TFunction tInt tInt)
outOfScope :: TestTree
outOfScope = testCase "typeof x == NotInScope" $ do
typeOf (Var "x") @?= Left (NotInScope "x")
appliedToWrongType :: TestTree
appliedToWrongType = testCase "typeof (\\x : Int -> x) True == Mismatch tBool tInt" $ do
let lambdaExpr = Lambda "x" tInt (Var "x")
typeOf (Apply lambdaExpr (Lit (LBool True))) @?= Left (Mismatch tBool tInt)
applyNonFunction :: TestTree
applyNonFunction = testCase "typeof (1 1) == NotFunction tInt" $ do
typeOf (Apply (Lit (LInt 1)) (Lit (LInt 1))) @?= Left (NotFunction tInt)
nonBoolIfCondition :: TestTree
nonBoolIfCondition = testCase "typeof (if 1 then True else False) == Mismatch tInt tBool" $ do
let ifExpr = If (Lit (LInt 1)) (Lit (LBool True)) (Lit (LBool False))
typeOf ifExpr @?= Left (Mismatch tInt tBool)
mismatchedThenElse :: TestTree
mismatchedThenElse = testCase "typeof (if True then 1 else False) == Mismatch tInt tBool" $ do
let ifExpr = If (Lit (LBool True)) (Lit (LInt 1)) (Lit (LBool False))
typeOf ifExpr @?= Left (Mismatch tInt tBool)
mismatchedEqualsLeft :: TestTree
mismatchedEqualsLeft = testCase "typeof (True == 1) == Mismatch tBool tInt" $ do
let eqExpr = Op Equals (Lit (LBool True)) (Lit (LInt 1))
typeOf eqExpr @?= Left (Mismatch tBool tInt)
mismatchedEqualsRight :: TestTree
mismatchedEqualsRight = testCase "typeof (1 == True) == Mismatch tInt tBool" $ do
let eqExpr = Op Equals (Lit (LInt 1)) (Lit (LBool True))
typeOf eqExpr @?= Left (Mismatch tInt tBool)
correctIfElse :: TestTree
correctIfElse = testCase "typeof (if True then 1 else 2) == tInt" $ do
let ifExpr = If (Lit (LBool True)) (Lit (LInt 1)) (Lit (LInt 2))
typeOf ifExpr @?= Right tInt
correctEquals :: TestTree
correctEquals = testCase "typeof (1 == 2) == tBool" $ do
let eqExpr = Op Equals (Lit (LInt 1)) (Lit (LInt 2))
typeOf eqExpr @?= Right tBool
correctFix :: TestTree
correctFix = testCase "typeof Fix factorial == TFunction tInt tInt" $ do
let factorial = Fix (Lambda "fact" (TFunction tInt tInt) (Lambda "x" tInt (If (Op Equals (Var "x") (Lit (LInt 0))) (Lit (LInt 1)) (Op Multiply (Var "x") (Apply (Var "fact") (Op Subtract (Var "x") (Lit (LInt 1))))))))
typeOf factorial @?= Right (TFunction tInt tInt)
fixMismatch :: TestTree
fixMismatch = testCase "typeof Fix (\\x : Bool -> 1) == Mismatch tBool tInt" $ do
let badFunc = Fix (Lambda "x" tBool (Lit (LInt 1)))
typeOf badFunc @?= Left (Mismatch tBool tInt)
fixNonFunction :: TestTree
fixNonFunction = testCase "typeof Fix 1 == NotFunction tInt" $ do
typeOf (Fix (Lit (LInt 1))) @?= Left (NotFunction tInt)
correctApply :: TestTree
correctApply = testCase "typeof ((\\x : Int -> x)1) == tInt" $ do
let applyExpr = Apply (Lambda "x" tInt (Var "x")) (Lit (LInt 1))
typeOf applyExpr @?= Right tInt
correctLet :: TestTree
correctLet = testCase "typeof (let x = 1 in True) == tBool" $ do
let letExpr = Let "x" (Lit (LInt 1)) (Lit (LBool True))
typeOf letExpr @?= Right tBool
-- make sure that the "let x = a" part of let...in is in scope when checking "in b"
letScopeCheck :: TestTree
letScopeCheck = testCase "typeof (let x = 1 in x) == tInt" $ do
let letExpr = Let "x" (Lit (LInt 1)) (Var "x")
typeOf letExpr @?= Right tInt
-- error in the "let x = a" part of let...in
letInnerError :: TestTree
letInnerError = testCase "typeof (let x = ((\\n : Int -> 1)True) in True) == Mismatch tBool tInt" $ do
let letExpr = Let "x" (Apply (Lambda "n" tInt (Lit (LInt 1))) (Lit (LBool True))) (Lit (LBool True))
typeOf letExpr @?= Left (Mismatch tBool tInt)
-- error in the "in b" part of let...in
letOuterError :: TestTree
letOuterError = testCase "typeof (let x = 1 in y) == NotInScope" $ do
let letExpr = Let "x" (Lit (LInt 1)) (Var "y")
typeOf letExpr @?= Left (NotInScope "y")
-- convert to property test?
polymorphicLambda :: TestTree
polymorphicLambda = testCase "typeof (\\x : a -> x) == TFunction (TVariable\"a\") (TVariable \"a\")" $ do
let idExpr = Lambda "x" (TVariable "a") (Var "x")
typeOf idExpr @?= Right (TFunction (TVariable "a") (TVariable "a"))
-- convert to property test?
polymorphicLambdaMulti :: TestTree
polymorphicLambdaMulti = testCase "typeof (\\x : a -> (\\y : b -> x)) == TFunction (TVariable \"a\" (TFunction (TVariable \"b\") (TVariable \"a\"))" $ do
let constExpr = Lambda "x" (TVariable "a") (Lambda "y" (TVariable "b") (Var "x"))
typeOf constExpr @?= Right (TFunction (TVariable "a") (TFunction (TVariable "b") (TVariable "a")))
-- convert to property test?
polymorphicApplied :: TestTree
polymorphicApplied = testCase "typeof ((\\x : a -> x)True) == tBool" $ do
let idExpr = Lambda "x" (TVariable "a") (Var "x")
typeOf (Apply idExpr (Lit (LBool True))) @?= Right tBool
-- convert to property test?
polymorphicAppliedMulti :: TestTree
polymorphicAppliedMulti = testCase "typeof (((\\x : a -> (\\y : b -> x))3)True) == tInt" $ do
let constExpr = Lambda "x" (TVariable "a") (Lambda "y" (TVariable "b") (Var "x"))
typeOf (Apply (Apply constExpr (Lit (LInt 3))) (Lit (LBool True))) @?= Right tInt
-- convert to property test?
polymorphicPartialApplied :: TestTree
polymorphicPartialApplied = testCase "typeof ((\\x : a -> (\\y : b -> x))3) == TFunction (TVariable\"b\") tInt" $ do
let constExpr = Lambda "x" (TVariable "a") (Lambda "y" (TVariable "b") (Var "x"))
typeOf (Apply constExpr (Lit (LInt 3))) @?= Right (TFunction (TVariable "b") tInt)
programExample :: TestTree
programExample = testCase "evalProgram (program to calculate 1 + 2) == 3" $ do
let mDecl = ("m", Lit (LInt 1))
let nDecl = ("n", Lit (LInt 2))
let mainExpr = Op Add (Var "m") (Var "n")
evalProgram (Program [mDecl, nDecl] mainExpr) @?= VInt 3
The full repository is available on GitHub; the code above is from commit ecaace0b8054eb1eaf8fce005be9740c4d2b2b77.
