Safe Haskell  SafeInferred 

Language  Haskell98 
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/enus/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
 You test expressions for equality of their normal forms using
Strong normalization comes at a price: Morte forbids recursion. Instead, you must translate all recursion to Falgebras and translate all corecursion to Fcoalgebras. 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/freerectypes/freerectypes.txt
Morte is designed to be a superoptimizing intermediate language with a simple optimization scheme. You optimize a Morte expression by just normalizing the expression. If you normalize a longlived program encoded as an Fcoalgebra you typically get a state machine, and if you normalize a longlived program encoded as an Falgebra 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.
 data Var = V Text Int
 data Const
 data Expr
 type Context = [(Text, Expr)]
 typeWith :: Context > Expr > Either TypeError Expr
 typeOf :: Expr > Either TypeError Expr
 normalize :: Expr > Expr
 used :: Text > Expr > Bool
 shift :: Int > Text > Expr > Expr
 prettyExpr :: Expr > Text
 prettyTypeError :: TypeError > Text
 data TypeError = TypeError {
 context :: Context
 current :: Expr
 typeMessage :: TypeMessage
 data TypeMessage
 buildConst :: Const > Builder
 buildVar :: Var > Builder
 buildExpr :: Expr > Builder
 buildTypeMessage :: TypeMessage > Builder
 buildTypeError :: TypeError > Builder
Syntax
Label for a bound variable
The Text
field is the variable's name (i.e. "x
").
The Int
field disambiguates variables with the same name if there are
multiple bound variables of the same name in scope. Zero refers to the
nearest bound variable and the index increases by one for each bound variable
of the same name going outward. The following diagram may help:
+refers to+   v  \(x : *) > \(y : *) > \(x : *) > x@0 +refers to+   v  \(x : *) > \(y : *) > \(x : *) > x@1
This Int
behaves like a De Bruijn index in the special case where all
variables have the same name.
You can optionally omit the index if it is 0
:
+refers to+   v  \(x : *) > \(y : *) > \(x : *) > x
Zero indices are omitted when prettyprinting Var
s and nonzero indices
appear as a numeric suffix.
Constants for the calculus of constructions
The only axiom is:
⊦ * : □
... and all four rule pairs are valid:
⊦ * ↝ * : * ⊦ □ ↝ * : * ⊦ * ↝ □ : □ ⊦ □ ↝ □ : □
Syntax tree for expressions
Core functions
typeWith :: Context > Expr > Either TypeError Expr Source
Typecheck an expression and return the expression's type if typechecking suceeds or an error if typechecking fails
typeWith
does not necessarily normalize the type since full normalization
is not necessary for just typechecking. If you actually care about the
returned type then you may want to normalize
it afterwards.
normalize :: Expr > Expr Source
Reduce an expression to its normal form, performing both beta reduction and eta reduction
normalize
does not typecheck the expression. You may want to typecheck
expressions before normalizing them since normalization can convert an
illtyped expression into a welltyped expression.
Utilities
used :: Text > Expr > Bool Source
Determine whether a Pi
bound variable should be displayed
Notice that if any variable within the body of a Pi
shares the same name and
an equal or greater DeBruijn index we display the Pi
bound variable. To
illustrate why we don't just check for equality, consider this type:
forall (a : *) > forall (a : *) > a@1
The a@1
refers to the outer a
(i.e. the left one), but if we hid the
inner a
(the right one), the type would make no sense:
forall (a : *) > * > a@1
... because the a@1
would misleadingly appear to be an unbound variable.
shift :: Int > Text > Expr > Expr Source
shift n x
adds n
to the index of all free variables named x
within an
Expr
prettyExpr :: Expr > Text Source
Prettyprint an expression
The result is a syntactically valid Morte program
prettyTypeError :: TypeError > Text Source
Prettyprint a type error
Errors
A structured type error that includes context
TypeError  

data TypeMessage Source
The specific type error
Builders
buildTypeMessage :: TypeMessage > Builder Source
Render a prettyprinted TypeMessage
as a Builder