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 (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 Vars and non-zero indices appear as a numeric suffix.

Constructors

V Text Int

Instances

Eq Var

Defined in Morte.Core

Methods

(==) :: Var -> Var -> Bool

(/=) :: Var -> Var -> Bool

Show Var

Defined in Morte.Core

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

IsString Var

Defined in Morte.Core

Methods

fromString :: String -> Var

Binary Var

Defined in Morte.Core

Methods

put :: Var -> Put

get :: Get Var

putList :: [Var] -> Put

NFData Var

Defined in Morte.Core

Methods

rnf :: Var -> ()

Buildable Var

Defined in Morte.Core

Methods

build :: Var -> Builder

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

Defined in Morte.Core

Methods

minBound :: Const

maxBound :: Const

Enum Const

Defined in Morte.Core

Methods

succ :: Const -> Const

pred :: Const -> Const

toEnum :: Int -> Const

fromEnum :: Const -> Int

enumFrom :: Const -> [Const]

enumFromThen :: Const -> Const -> [Const]

enumFromTo :: Const -> Const -> [Const]

enumFromThenTo :: Const -> Const -> Const -> [Const]

Eq Const

Defined in Morte.Core

Methods

(==) :: Const -> Const -> Bool

(/=) :: Const -> Const -> Bool

Show Const

Defined in Morte.Core

Methods

showsPrec :: Int -> Const -> ShowS

show :: Const -> String

showList :: [Const] -> ShowS

Binary Const

Defined in Morte.Core

Methods

put :: Const -> Put

get :: Get Const

putList :: [Const] -> Put

NFData Const

Defined in Morte.Core

Methods

rnf :: Const -> ()

Buildable Const

Defined in Morte.Core

Methods

build :: Const -> Builder

data Path

Path to an external resource

Constructors

File FilePath

URL Text

Instances

Eq Path

Defined in Morte.Core

Methods

(==) :: Path -> Path -> Bool

(/=) :: Path -> Path -> Bool

Ord Path

Defined in Morte.Core

Methods

compare :: Path -> Path -> Ordering

(<) :: Path -> Path -> Bool

(<=) :: Path -> Path -> Bool

(>) :: Path -> Path -> Bool

(>=) :: Path -> Path -> Bool

max :: Path -> Path -> Path

min :: Path -> Path -> Path

Show Path

Defined in Morte.Core

Methods

showsPrec :: Int -> Path -> ShowS

show :: Path -> String

showList :: [Path] -> ShowS

Buildable Path

Defined in Morte.Core

Methods

build :: Path -> Builder

data Expr a

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 a) (Expr a)

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

Pi Text (Expr a) (Expr a)

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

App (Expr a) (Expr a)

App f a        ~  f a

Embed a

Embed path     ~  #path

Instances

Monad Expr

Defined in Morte.Core

Methods

(>>=) :: Expr a -> (a -> Expr b) -> Expr b

(>>) :: Expr a -> Expr b -> Expr b

return :: a -> Expr a

fail :: String -> Expr a

Functor Expr

Defined in Morte.Core

Methods

fmap :: (a -> b) -> Expr a -> Expr b

(<$) :: a -> Expr b -> Expr a

Applicative Expr

Defined in Morte.Core

Methods

pure :: a -> Expr a

(<*>) :: Expr (a -> b) -> Expr a -> Expr b

liftA2 :: (a -> b -> c) -> Expr a -> Expr b -> Expr c

(*>) :: Expr a -> Expr b -> Expr b

(<*) :: Expr a -> Expr b -> Expr a

Foldable Expr

Defined in Morte.Core

Methods

fold :: Monoid m => Expr m -> m

foldMap :: Monoid m => (a -> m) -> Expr a -> m

foldr :: (a -> b -> b) -> b -> Expr a -> b

foldr' :: (a -> b -> b) -> b -> Expr a -> b

foldl :: (b -> a -> b) -> b -> Expr a -> b

foldl' :: (b -> a -> b) -> b -> Expr a -> b

foldr1 :: (a -> a -> a) -> Expr a -> a

foldl1 :: (a -> a -> a) -> Expr a -> a

toList :: Expr a -> [a]

null :: Expr a -> Bool

length :: Expr a -> Int

elem :: Eq a => a -> Expr a -> Bool

maximum :: Ord a => Expr a -> a

minimum :: Ord a => Expr a -> a

sum :: Num a => Expr a -> a

product :: Num a => Expr a -> a

Traversable Expr

Defined in Morte.Core

Methods

traverse :: Applicative f => (a -> f b) -> Expr a -> f (Expr b)

sequenceA :: Applicative f => Expr (f a) -> f (Expr a)

mapM :: Monad m => (a -> m b) -> Expr a -> m (Expr b)

sequence :: Monad m => Expr (m a) -> m (Expr a)

Eq a => Eq (Expr a)

Defined in Morte.Core

Methods

(==) :: Expr a -> Expr a -> Bool

(/=) :: Expr a -> Expr a -> Bool

Show a => Show (Expr a)

Defined in Morte.Core

Methods

showsPrec :: Int -> Expr a -> ShowS

show :: Expr a -> String

showList :: [Expr a] -> ShowS

IsString (Expr a)

Defined in Morte.Core

Methods

fromString :: String -> Expr a

Binary a => Binary (Expr a)

Defined in Morte.Core

Methods

put :: Expr a -> Put

get :: Get (Expr a)

putList :: [Expr a] -> Put

NFData a => NFData (Expr a)

Defined in Morte.Core

Methods

rnf :: Expr a -> ()

Buildable a => Buildable (Expr a)

Generates a syntactically valid Morte program

Defined in Morte.Core

Methods

build :: Expr a -> Builder

data Context a

Bound variable names and their types

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

Instances

Functor Context

Defined in Morte.Context

Methods

fmap :: (a -> b) -> Context a -> Context b

(<$) :: a -> Context b -> Context a

NFData a => NFData (Context a)

Defined in Morte.Context

Methods

rnf :: Context a -> ()

Core functions

typeWith :: Context (Expr Void) -> Expr Void -> Either TypeError (Expr Void)

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 Void -> Either TypeError (Expr Void)

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 a -> Expr a

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

shift :: Int -> Text -> Expr a -> Expr a

shift n x adds n to the index of all free variables named x within an Expr

subst :: Text -> Int -> Expr a -> Expr a -> Expr a

Substitute all occurrences of a variable with an expression

subst x n C B  ~  B[x@n := C]

pretty :: Buildable a => a -> Text

Pretty-print a value

buildExpr :: Buildable a => Expr a -> Builder

Pretty-print an expression as a Builder, using Unicode symbols

buildExprASCII :: Buildable a => Expr a -> Builder

Pretty-print an expression as a Builder, using ASCII symbols

Errors

data TypeError

A structured type error that includes context

Constructors

TypeError

Fields

• context :: Context (Expr Void)
• current :: Expr Void
• typeMessage :: TypeMessage

Instances

Show TypeError

Defined in Morte.Core

Methods

showsPrec :: Int -> TypeError -> ShowS

show :: TypeError -> String

showList :: [TypeError] -> ShowS

Exception TypeError

Defined in Morte.Core

Methods

toException :: TypeError -> SomeException

fromException :: SomeException -> Maybe TypeError

displayException :: TypeError -> String

NFData TypeError

Defined in Morte.Core

Methods

rnf :: TypeError -> ()

Buildable TypeError

Defined in Morte.Core

Methods

build :: TypeError -> Builder

data TypeMessage

The specific type error

Constructors

UnboundVariable

InvalidInputType (Expr Void)

InvalidOutputType (Expr Void)

NotAFunction

TypeMismatch (Expr Void) (Expr Void)

Untyped Const

Instances

Show TypeMessage

Defined in Morte.Core

Methods

showsPrec :: Int -> TypeMessage -> ShowS

show :: TypeMessage -> String

showList :: [TypeMessage] -> ShowS

NFData TypeMessage

Defined in Morte.Core

Methods

rnf :: TypeMessage -> ()

Buildable TypeMessage

Defined in Morte.Core

Methods

build :: TypeMessage -> Builder