Morte.Core

This module contains the core calculus for the Morte language. This language is a minimalist implementation of the calculus of constructions, which is in turn a specific kind of pure type system. If you are new to pure type systems you may wish to read "Henk: a typed intermediate language".

http://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz

Morte is a strongly normalizing language, meaning that:

• Every expression has a unique normal form computed by normalize
• You test expressions for equality of their normal forms using ==
• Equational reasoning preserves normal forms

Strong normalization comes at a price: Morte forbids recursion. Instead, you must translate all recursion to F-algebras and translate all corecursion to F-coalgebras. If you are new to F-(co)algebras then you may wish to read Morte.Tutorial or read "Recursive types for free!":

http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt

Morte is designed to be a super-optimizing intermediate language with a simple optimization scheme. You optimize a Morte expression by just normalizing the expression. If you normalize a long-lived program encoded as an F-coalgebra you typically get a state machine, and if you normalize a long-lived program encoded as an F-algebra you typically get an unrolled loop.

Strong normalization guarantees that all abstractions encodable in Morte are "free", meaning that they may increase your program's compile times but they will never increase your program's run time because they will normalize to the same code.

Syntax

data Var

Label for a bound variable

The Text field is the variable's name.

The Int field disambiguates variables with the same name. Zero is a good default. Non-zero values will appear as a numeric suffix when pretty-printing the Var.

Constructors

V Text Int

Instances

Eq Var

Show Var

IsString Var

Binary Var

data Const

Constants for the calculus of constructions

The only axiom is:

 ⊦ * : □

... and all four rule pairs are valid:

 ⊦ * ↝ * : *
 ⊦ □ ↝ * : *
 ⊦ * ↝ □ : □
 ⊦ □ ↝ □ : □

Constructors

Star

Box

Instances

Bounded Const

Enum Const

Eq Const

Show Const

Binary Const

data Expr

Syntax tree for expressions

Constructors

Const Const

 Const c        ~  c

Var Var

 Var (V x 0)    ~  x
 Var (V x n)    ~  x@n

Lam Var Expr Expr

 Lam x     A b  ~  λ(x : A) → b

Pi Var Expr Expr

 Pi x      A B  ~  ∀(x : A) → B
 Pi unused A B  ~        A  → B

App Expr Expr

 App f a        ~  f a

Instances

Eq Expr

Show Expr

IsString Expr

Binary Expr

type Context = [(Var, Expr)]

Bound variables and their types

Earlier Vars shadow later matching Vars

Core functions

typeWith :: Context -> Expr -> Either TypeError Expr

Type-check an expression and return the expression's type if type-checking suceeds or an error if type-checking fails

typeWith does not necessarily normalize the type since full normalization is not necessary for just type-checking. If you actually care about the returned type then you may want to normalize it afterwards.

typeOf :: Expr -> Either TypeError Expr

typeOf is the same as typeWith with an empty context, meaning that the expression must be closed (i.e. no free variables), otherwise type-checking will fail.

normalize :: Expr -> Expr

Reduce an expression to its normal form, performing both beta reduction and eta reduction

normalize does not type-check the expression. You may want to type-check expressions before normalizing them since normalization can convert an ill-typed expression into a well-typed expression.

Utilities

prettyExpr :: Expr -> Text

Pretty-print an expression

The result is a syntactically valid Morte program

prettyTypeError :: TypeError -> Text

Pretty-print a type error

Errors

data TypeError

A structured type error that includes context

Constructors

TypeError

Fields

context :: Context

current :: Expr

typeMessage :: TypeMessage

Instances

Show TypeError

Typeable TypeError

Exception TypeError

data TypeMessage

The specific type error

Constructors

UnboundVariable

InvalidInputType Expr

InvalidOutputType Expr

NotAFunction

TypeMismatch Expr Expr

Untyped Const

Instances

Show TypeMessage

Typeable TypeMessage