Safe Haskell | Safe-Infered |
---|
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.
- data Var = V Text Int
- data Const
- data Expr
- type Context = [(Var, Expr)]
- typeWith :: Context -> Expr -> Either TypeError Expr
- typeOf :: Expr -> Either TypeError Expr
- normalize :: Expr -> Expr
- prettyExpr :: Expr -> Text
- prettyTypeError :: TypeError -> Text
- data TypeError = TypeError {
- context :: Context
- current :: Expr
- typeMessage :: TypeMessage
- data TypeMessage
Syntax
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 ExprSource
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.
normalize :: Expr -> ExprSource
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 -> TextSource
Pretty-print an expression
The result is a syntactically valid Morte program
prettyTypeError :: TypeError -> TextSource
Pretty-print a type error
Errors
A structured type error that includes context
TypeError | |
|
data TypeMessage Source
The specific type error