This repo corresponds to my 4th year Integrated Masters, Mathematics and Computer Science dissertation. It is not intended to be used outside of this context.

We assume a full installation of Haskell.

The monomorphic type inference implementation is contained within the Monomorphic module. To use this implementation, add the following imports:

import Monomorphic.Types
import Monomorphic.Terms
import Monomorphic.Context
import qualified Monomorphic.Simple.Inference
import qualified Monomorphic.Annotated.Inference

Types are defined within the Monomorphic.Types sub-module. They are defined closely to their corresponding grammar.

As an example, to construct a type representing a lambda abstraction from a natural number to the unit type, you can write:

(Abstraction Natural Unit)

Or, a pair of identity functions, the left for natural numbers, and the right for units

(Product (Abstraction Natural Natural) (Abstraction Unit Unit))

Terms are defined within the Monomorphic.Terms sub-module. They are defined closely to their corresponding grammar.

Variables are just strings

To define the identity for natural numbers function:

(Lambda "x" Natural (Var "x"))

Contexts are defined in the sub-module Monomorphic.Contexts. They are defined closely to their corresponding grammar and the cons Haskell operator.

To create a modal context consisting of two variables:

MCons "v" Unit (MCons "u" Natural MEmpty)

Two inference functions are provided: one simple inference method, which only returns the type, and an annotated one, which returns an annotation tree.

The first is located in the sub-module Monomorphic.Simple.Inference, the second is in Monomorphic.Annotated.Inference.

Once one is chosen, you can infer the type of a term, under some contexts as:

infer MEmpty OEmpty (Anno (Lambda "x" Natural (Var "x")) (Abstraction Natural Natural))

Some example terms are provided in the Monomorphic module.

Similar to the monomorphic inference, except the following imports are required instead:

import Polymorphic.Types
import Polymorphic.Terms
import Polymorphic.Context
import qualified Polymorphic.Simple.Inference

Only simple polymorphic inference has been implemented.

Some example terms are provided in the Polymorphic module.