morte-1.1.2: A bare-bones calculus of constructions

Morte.Core

Description

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!":

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.

Synopsis

Syntax

data Var Source

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 pretty-printing `Var`s and non-zero indices appear as a numeric suffix.

Constructors

 V Text Int

Instances

 Eq Var Show Var IsString Var Binary Var NFData Var

data Const Source

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 NFData Const

data Expr Source

Syntax tree for expressions

Constructors

 Const Const `Const c ~ c` Var Var ```Var (V x 0) ~ x Var (V x n) ~ x@n``` Lam Text Expr Expr `Lam x A b ~ λ(x : A) → b` Pi Text 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 NFData Expr

type Context = [(Text, Expr)] Source

Bound variable names and their types

Variable names may appear more than once in the `Context`. The `Var` `x@n` refers to the `n`th occurrence of `x` in the `Context` (using 0-based numbering).

Core functions

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` 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.

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

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`

Pretty-print an expression

The result is a syntactically valid Morte program

Pretty-print a type error

Errors

data TypeError Source

A structured type error that includes context

Constructors

 TypeError Fieldscontext :: Context current :: Expr typeMessage :: TypeMessage

Instances

 Show TypeError Exception TypeError NFData TypeError Typeable * TypeError

The specific type error

Instances

 Show TypeMessage NFData TypeMessage

Builders

Render a pretty-printed `Const` as a `Builder`

Render a pretty-printed `Var` as a `Builder`

Render a pretty-printed `Expr` as a `Builder`

Render a pretty-printed `TypeMessage` as a `Builder`

Render a pretty-printed `TypeError` as a `Builder`