Safe Haskell | Safe-Inferred |
---|
Morte is a minimalist implementation of the calculus of constructions that comes with a parser, type-checker, optimizer, and pretty-printer.
You can think of Morte as a very low-level intermediate language for functional languages. This virtual machine was designed with the following design principles, in descending order of importance:
- Be super-optimizable - by disabling unrestricted recursion
- Be portable - so you can transmit code between different languages
- Be efficient - so that Morte can scale to large code bases
- Be simple - so people can reason about Morte's soundness
This library does not provide any front-end or back-end language for Morte. These will be provided as separate libraries in the future.
The "Introduction" section walks through basic usage of the compiler and library.
The "Desugaring" section explains how to desugar complex abstractions to Morte's core calculus.
The "Optimization" section explains how Morte optimizes programs, providing several long-form example programs and their optimized output.
Introduction
You can test out your first Morte program using the morte
executable
provided by this library. This executable reads a Morte program from
stdin
, outputs the type of the program to stderr
, and outputs the
optimized program to stdout
.
We'll begin by translating Haskell's identity function to Morte. For
reference, id
is defined in Haskell as:
id :: a -> a id x = x
We will enter the equivalent Morte program at the command line:
$ morte \(a : *) -> \(x : a) -> x <Enter> <Ctrl-D> ∀(a : *)
Desugaring
The Expr
type defines Morte's syntax, which is very simple:
data Expr = Const Const -- Type system constants | Var Var -- Bound variables | Lam Var Expr Expr -- Lambda | Pi Var Expr Expr -- "forall" | App Expr Expr -- Function application
For example, you can see what id'
from the previous section expands out to
by using the Show
instance for Expr
:
Lam (V "String" 0) (Const Star) ( App (Lam (V "a" 0) (Const Star) ( Lam (V "x" 0) (Var (V "a" 0)) (Var (V "x" 0)))) (Var (V "String" 0)))
... although Morte provides syntactic sugar for building expressions by
hand using the OverloadedStrings
instance, so you could instead write:
Lam "String" (Const Star) ( App (Lam "a" (Const Star)( Lam "x" "a" "a")) "String" )
Note that Morte's syntax does not include:
-
let
expressions -
case
expressions - Built-in values other than functions
- Built-in types other than function types
-
newtype
s - Support for multiple expressions/statements
- Modules or imports
- Recursion / Corecursion
Future front-ends to Morte will support these higher-level abstractions, but for now you must desugar all of these to lambda calculus before Morte can type-check and optimize your program. The following sections explain how to desugar these abstractions from a Haskell-like language.
Let
Given a non-recursive let
statement of the form:
let var1 :: type1 var1 = expr1 var2 :: type2 var2 = expr2 ... varN :: typeN varN = exprN in result
You can desugar that to:
(\(var1 : type1) -> \(var2 : type2) -> ... -> \(varN : typeN) -> result) expr1 expr2 ... exprN
Remember that whitespace is not significant, so you can also write that as:
( \(var1 : type1) -> \(var2 : type2) -> ... -> \(varN : typeN) -> result ) expr1 expr2 ... exprN
The Morte compiler does not mistake expr1
through exprN
for additional
top-level expresions, because a Morte program only consists of a single
expression.
Carefully note that the following expression:
let var1 : type1 var1 = expr1 var2 : type2 var2 = type2 in result
... is not the same as:
let var1 : type1 var1 = expr1 in let var2 : type2 var2 = expr2 in result
They desugar to different Morte code and sometimes the distinction between the two is significant.
Using let
, you can desugar this:
let id : forall (a : *) -> a -> a id = \(a : *) -> \(x : *) -> x in id (forall (a : *) -> a -> a) id
... into this:
-- id2.mt ( \(id : forall (a : *) -> a -> a) -> id (forall (a : *) -> a -> a) id -- Apply the identity function to itself ) -- id (\(a : *) -> \(x : a) -> x)
... and the compiler will type-check and optimize that to:
$ morte < id2.mt ∀(a : *)
Simple types
The following sections use a technique known as Boehm-Berarducci encoding to convert recursive data types to lambda terms. If you already know what Boehm-Berarducci encoding is then you can skip these sections. You might already recognize this technique by the names of overlapping techniques such as CPS-encoding, Church-encoding, or F-algebras.
I'll first explain how to desugar a somewhat complicated non-recursive type and then show how this trick specializes to simpler types. The first example is quite long, but you'll see that it gets much more compact in the simpler examples.
Given the following non-recursive type:
let data T a b c = A | B a | C b c in result
You can desugar that to the following Morte code:
-- The type constructor ( \(T : * -> * -> * -> *) -- The value constructors -> \(A : forall (a : *) -> forall (b : *) -> forall (c : *) -> T a b c) -> \(B : forall (a : *) -> forall (b : *) -> forall (c : *) -> a -> T a b c) -> \(C : forall (a : *) -> forall (b : *) -> forall (c : *) -> b -> c -> T a b c) -- Pattern match on T -> \( matchT : forall (a : *) -> forall (b : *) -> forall (c : *) -> T a b c -> forall (r : *) -> r -- `A` branch of the pattern match -> (a -> r) -- `B` branch of the pattern match -> (b -> c -> r) -- `C` branch of the pattern match -> r ) -> result ) -- A value of type `T a b c` is just a preformed pattern match ( \(a : *) -> \(b : *) -> \(c : *) -> forall (r : *) -> r -- A branch of the pattern match -> (a -> r) -- B branch of the pattern match -> (b -> c -> r) -- C branch of the pattern match -> r ) -- Constructor for A ( \(a : *) -> \(b : *) -> \(c : *) -> \(r : *) -> \(A : r) -> \(B : a -> r) -> \(C : b -> c -> r) -> A ) -- Constructor for B ( \(a : *) -> \(b : *) -> \(c : *) -> \(va : a) -> \(r : *) -> \(A : r) -> \(B : a -> r) -> \(C : b -> c -> r) -> B va ) -- Constructor for C ( \(a : *) -> \(b : *) -> \(c : *) -> \(vb : b) -> \(vc : c) -> \(r : *) -> \(A : r) -> \(B : a -> r) -> \(C : b -> c -> r) -> C vb vc ) -- matchT is just the identity function ( \(a : *) -> \(b : *) -> \(c : *) -> \(t : forall (r : *) -> r -> (a -> r) -> (b -> c -> r) -> r) -> t )
Within the result
expression, you could assemble values of type 'T'
using the constructors:
Context: String : * Int : * Bool : * s : String i : Int b : Bool A String Int Bool : T String Int Bool B String Int Bool s : T String Int Bool C String Int Bool i b : T String Int Bool
... and you could pattern match on any value of type 'T'
using matchT
:
Context: String : * Int : * Bool : * r : * -- The result type of all three case branches t : T String Int Bool matchT String Int Bool r t ( ...) -- Branch if you match `A` (\(s : String) -> ...) -- Branch if you match `B` (\(i : Int ) -> \(b : Bool) -> ...) -- Branch if you match `C`
Now let's see how this specializes to a simpler example: Haskell's Bool
type.
-- let data Bool = True | False -- -- in result ( \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> \(if : Bool -> forall (r : *) -> r -> r -> r) -> result ) -- Bool (forall (r : *) -> r -> r -> r) -- True (\(r : *) -> \(x : r) -> \(_ : r) -> x) -- False (\(r : *) -> \(_ : r) -> \(x : r) -> x) -- if (\(b : forall (r : *) -> r -> r -> r) -> b)
Notice that if
is our function to pattern match on a Bool
. The two
branches of the if
correspond to the then
and else
clauses.
Using this definition of Bool
we can define a simple program:
-- bool.mt -- let data Bool = True | False -- -- in if True then One else Zero ( \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> \(if : Bool -> forall (r : *) -> r -> r -> r) -> \(Int : *) -> \(Zero : Int) -> \(One : Int) -> if True Int One Zero ) -- Bool (forall (r : *) -> r -> r -> r) -- True (\(r : *) -> \(x : r) -> \(_ : r) -> x) -- False (\(r : *) -> \(_ : r) -> \(x : r) -> x) -- if (\(b : forall (r : *) -> r -> r -> r) -> b)
If you type-check and optimize this, you get:
$ morte < bool.mt ∀(Int : *)
Newtypes
Defining a newtype is no different than defining a data type with a single constructor with one field:
-- let newtype Name = MkName { getName :: String } -- -- in result ( \(Name : *) -> \(MkName : String -> Name ) -> \(getName : Name -> String) -> result ) -- Name String -- MkName (\(str : String) -> str) -- getName (\(str : String) -> str)
Within the expression result
, Name
is actually a new type, meaning that
a value of type Name
will not type-check as a String
and, vice versa, a
value of type String
will not type-check as a Name
. You would have to
explicitly convert back and forth between Name
and String
using the
MkName
and getName
functions.
We can prove this using the following example program:
-- newtype.mt -- let newtype Name = MkName { getName :: String } -- -- in (f :: Name -> Name) (x :: String) ( \(Name : *) -> \(MkName : String -> Name ) -> \(getName : Name -> String) -> \(f : Name -> Name) -> \(x : String) -> f x ) -- Name String -- MkName (\(str : String) -> str) -- getName (\(str : String) -> str)
That program fails to type-check, giving the following error message:
$ morte < newtype.mt Context: Name : * MkName : String
Recursion
Defining a recursive data type is very similar to defining a non-recursive type. Let's use lists as an example:
let data List a = Cons a (List a) | Nil in result
The equivalent Morte code is:
-- let data List a = Cons a (List a) | Nil -- -- in result ( \(List : * -> *) -> \(Cons : forall (a : *) -> a -> List a -> List a) -> \(Nil : forall (a : *) -> List a) -> \( foldr : forall (a : *) -> List a -> forall (r : *) -> (a -> r -> r) -> r -> r ) -> result ) -- List ( \(a : *) -> forall (list : *) -> (a -> list -> list) -- Cons -> list -- Nil -> list ) -- Cons ( \(a : *) -> \(va : a) -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list) -> \(list : *) -> \(Cons : a -> list -> list) -> \(Nil : list) -> Cons va (vas list Cons Nil) ) -- Nil ( \(a : *) -> \(list : *) -> \(Cons : a -> list -> list) -> \(Nil : list) -> Nil ) -- foldr ( \(a : *) -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list) -> vas )
Here I use the list
type variable where previous examples would use
'r'
to emphasize that the continuations that a List
consumes both have
the same shape as the list constructors. You just replace all recursive
references to the data type with the type of the final result, pretending
that the final result is a list.
Let's extend the List
example with the Bool
code to implement Haskell's
all
function and use it on an actual List
of Bool
s:
-- all.mt -- let data Bool = True | False -- -- data List a = Cons a (List a) | Nil -- -- in let (&&) :: Bool -> Bool -> Bool -- (&&) b1 b2 = if b1 then b2 else False -- -- bools :: List Bool -- bools = Cons True (Cons True (Cons True Nil)) -- -- in foldr bools (&&) True ( \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> \(if : Bool -> forall (r : *) -> r -> r -> r) -> \(List : * -> *) -> \(Cons : forall (a : *) -> a -> List a -> List a) -> \(Nil : forall (a : *) -> List a) -> \( foldr : forall (a : *) -> List a -> forall (r : *) -> (a -> r -> r) -> r -> r ) -> ( \((&&) : Bool -> Bool -> Bool) -> \(bools : List Bool) -> foldr Bool bools Bool (&&) True ) -- (&&) (\(b@1 : Bool) -> \(b@2 : Bool) -> if b@1 Bool b@2 False) -- bools (Cons Bool True (Cons Bool True (Cons Bool True (Nil Bool)))) ) -- Bool (forall (r : *) -> r -> r -> r) -- True (\(r : *) -> \(x : r) -> \(_ : r) -> x) -- False (\(r : *) -> \(_ : r) -> \(x : r) -> x) -- if (\(b : forall (r : *) -> r -> r -> r) -> b) -- List ( \(a : *) -> forall (list : *) -> (a -> list -> list) -- Cons -> list -- Nil -> list ) -- Cons ( \(a : *) -> \(va : a) -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list) -> \(list : *) -> \(Cons : a -> list -> list) -> \(Nil : list) -> Cons va (vas list Cons Nil) ) -- Nil ( \(a : *) -> \(list : *) -> \(Cons : a -> list -> list) -> \(Nil : list) -> Nil ) -- foldr ( \(a : *) -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list) -> vas )
If you type-check and optimize the program, the compiler will statically
evaluate the entire computation, reducing the program to True
:
$ morte < all.mt ∀(r : *)
Existential Quantification
You can translate existential quantified types to use universal quantification. For example, consider the following existentially quantified Haskell type:
let data Example = forall s . MkExample s (s -> String) in result
The equivalent Morte program is:
-- let data Example = forall s . Example s (s -> String) -- -- in result \(String : *) -> ( \(Example : *) -> \(MkExample : forall (s : *) -> s -> (s -> String) -> Example) -> \( matchExample : Example -> forall (x : *) -> (forall (s : *) -> s -> (s -> String) -> x) -> x ) -> result ) -- Example ( forall (x : *) -> (forall (s : *) -> s -> (s -> String) -> x) -- MkExample -> x ) -- MkExample ( \(s : *) -> \(vs : s) -> \(fs : s -> String) -> \(x : *) -> \(MkExample : forall (s : *) -> s -> (s -> String) -> x) -> MkExample s vs fs ) -- matchExample ( \(e : forall (x : *) -> (forall (s : *) -> s -> (s -> String) -> x) -> x) -> e )
More generally, for every constructor that you existentially quantify with a
type variable 's'
you just add a (forall (s : *) -> ...)
prefix to
that constructor's continuation. If you "pattern match" against the
constructor corresponding to that continuation you will bind the
existentially quantified type.
For example, we can pattern match against the MkExample
constructor like
this:
\(e : Example) -> matchExample e (\(s : *) -> (x : s) -> (f : s -> String) -> expr)
The type 's'
will be in scope for expr
and we can safely apply the
bound function to the bound value if we so chose to extract a String
,
despite not knowing which type 's'
we bound:
\(e : Example) -> matchExample e (\(s : *) -> (x : s) -> (f : s -> String) -> f x)
The two universal quantifiers in the definition of the Example
type
statically forbid the type 's'
from leaking from the pattern match.
Corecursion
Recursive types can only encode finite data types. If you want a potentially infinite data type (such as an infinite list), you must encode the type in a different way.
For example, consider the following infinite stream type:
codata Stream a = Cons a (Stream a)
If you tried to encode that as a recursive type, you would end up with this Morte type:
\(a : *) -> forall (x : *) -> (a -> x -> x) -> x
However, this type is uninhabited, meaning that you cannot create a value of
the above type for any choice of 'a'
. Try it, if you don't believe
me.
Potentially infinite types must be encoded using a dual trick, where we store them as an existentially quantified seed and a generating step function that emits one layer alongside a new seed.
For example, the above Stream
type would translate to the following
non-recursive representation. The StreamF
constructor represents one
layer and the Stream
type lets us generate an infinite number of layers
by providing an initial seed of type s
and a generation function of type
(s -> StreamF a s)
:
-- Replace the corecursive occurrence of `Stream` with `s` data StreamF a s = Cons a s data Stream a = forall s . MkStream s (s -> StreamF a s)
The above type will work for any type 's'
as the 's'
is
existentially quantified. The end user of the Stream
will never be able
to detect what the original type of s
was, because the MkStream
constructor closes over that information permanently.
An example Stream
is the following lazy stream of natural numbers:
nats :: Stream Int nats = MkStream 0 (\n -> Cons n (n + 1))
Internally, the above Stream
uses an Int
as its internal state, but
that is completely invisible to all downstream code, which cannot access
the concrete type of the internal state any longer.
In fact, this trick of using a seed and a generating step function is a special case of a F-coalgebra encoding of a corecursive type, which is anything of the form:
exists s . (s, s -> F s)
... where F
is a strictly-positive functor.
Once you F-coalgebra encode the Stream
type you can translate the type to
Morte using the rules for existential quantification given in the previous
section:
(forall (x : *) -> (forall (s : *) -> s -> (s -> StreamF a s) -> x) -> x
See the next section for some example Stream
code.
Optimization
You might wonder why Morte forbids recursion, forcing us to encode data types F-algebras or F-coalgebras. Morte imposes this restriction this in order to super-optimize your program. For example, consider the following program which maps the identity function over a list:
-- mapid1.mt ( \(List : * -> *) -> \(map : forall (a : *) -> forall (b : *) -> (a -> b) -> List a -> List b) -> \(id : forall (a : *) -> a -> a) -> \(a : *) -> map a a (id a) ) -- List (\(a : *) -> forall (x : *) -> (a -> x -> x) -> x -> x) -- map ( \(a : *) -> \(b : *) -> \(f : a -> b) -> \(l : forall (x : *) -> (a -> x -> x) -> x -> x) -> \(x : *) -> \(Cons : b -> x -> x) -> \(Nil: x) -> l x (\(va : a) -> \(vx : x) -> Cons (f va) vx) Nil ) -- id (\(a : *) -> \(va : a) -> va)
If we examine the compiler output, we'll see that the compiler fuses away
the map
, leaving behind the identity function on lists:
$ morte < mapid1.mt ∀(a : *)
Normalization
Morte has a very simple optimization scheme. The only thing that Morte does to optimize programs is beta-reduce them and eta-reduce them to their normal form. Since Morte's core calculus is non-recursive, this reduction is guaranteed to terminate.
The way Morte compares expressions for equality is just to compare their normal forms. Note that this definition of equality does not detect all equal programs. Here's an example of an equality that Morte does not currently detect (but might detect in the future):
k : forall (x : *) -> (a -> x) -> x k (f . g) = f (k g)
This is an example of a free theorem: an equality that can be deduced purely
from the type of k
. Morte may eventually use free theorems to further
normalize expression, but for now it does not.
Normalization leads to certain emergent properties when optimizing recursive
code or corecursive code. If you optimize a corecursive loop you will
produce code equivalent an while
loop where the seed is the initial state
of the loop and the generating step function unfolds one iteration of the
loop. If you optimize a recursive loop you will generate an unrolled loop.
See the next section for an example of Morte generating a very large
unrolled loop.
Normalization confers one very useful property: the runtime performance of a Morte program is completely impervious to abstraction. Adding additional abstraction layers may increase compile time, but runtime performance will remain constant. The runtime performance of a program is solely a function of the program's normal form, and adding additional abstraction layers never changes the normal form your program.
Effects
Morte uses the Haskell approach to effects, where effects are represented as terms within the language and evaluation order has no impact on order of effects. This is by necessity: if evaluation triggered side effects then Morte would be unable to optimize expressions by normalizing them.
The following example encodes IO
within Morte as an abstract syntax tree
of effects (a.k.a. a free monad). Encoding IO
as a free monad is not
strictly necessary, but doing so makes Morte aware of the monad laws, which
allows it to greatly simplify the program:
-- recursive.mt -- The Haskell code we will translate to Morte: -- -- import Prelude hiding ( -- (+), (*), IO, putStrLn, getLine, (>>=), (>>), return ) -- -- -- Simple prelude -- -- data Nat = Succ Nat | Zero -- -- zero :: Nat -- zero = Zero -- -- one :: Nat -- one = Succ Zero -- -- (+) :: Nat -> Nat -> Nat -- Zero + n = n -- Succ m + n = m + Succ n -- -- (*) :: Nat -> Nat -> Nat -- Zero * n = Zero -- Succ m * n = n + (m * n) -- -- foldNat :: Nat -> (a -> a) -> a -> a -- foldNat Zero f x = x -- foldNat (Succ m) f x = f (foldNat m f x) -- -- data IO r = PutStrLn String (IO r) | GetLine (String -> IO r) | Return r -- -- putStrLn :: String -> IO U -- putStrLn str = PutStrLn str (Return Unit) -- -- getLine :: IO String -- getLine = GetLine Return -- -- return :: a -> IO a -- return = Return -- -- (>>=) :: IO a -> (a -> IO b) -> IO b -- PutStrLn str io >>= f = PutStrLn str (io >>= f) -- GetLine k >>= f = GetLine (\str -> k str >>= f) -- Return r >>= f = f r -- -- -- Derived functions -- -- (>>) :: IO U -> IO U -> IO U -- m >> n = m >>= \_ -> n -- -- two :: Nat -- two = one + one -- -- three :: Nat -- three = one + one + one -- -- four :: Nat -- four = one + one + one + one -- -- five :: Nat -- five = one + one + one + one + one -- -- six :: Nat -- six = one + one + one + one + one + one -- -- seven :: Nat -- seven = one + one + one + one + one + one + one -- -- eight :: Nat -- eight = one + one + one + one + one + one + one + one -- -- nine :: Nat -- nine = one + one + one + one + one + one + one + one + one -- -- ten :: Nat -- ten = one + one + one + one + one + one + one + one + one + one -- -- replicateM_ :: Nat -> IO U -> IO U -- replicateM_ n io = foldNat n (io >>) (return Unit) -- -- ninetynine :: Nat -- ninetynine = nine * ten + nine -- -- main_ :: IO U -- main_ = getLine >>= putStrLn -- "Free" variables ( \(String : * ) -> \(U : *) -> \(Unit : U) -- Simple prelude -> ( \(Nat : *) -> \(zero : Nat) -> \(one : Nat) -> \((+) : Nat -> Nat -> Nat) -> \((*) : Nat -> Nat -> Nat) -> \(foldNat : Nat -> forall (a : *) -> (a -> a) -> a -> a) -> \(IO : * -> *) -> \(return : forall (a : *) -> a -> IO a) -> \((>>=) : forall (a : *) -> forall (b : *) -> IO a -> (a -> IO b) -> IO b ) -> \(putStrLn : String -> IO U) -> \(getLine : IO String) -- Derived functions -> ( \((>>) : IO U -> IO U -> IO U) -> \(two : Nat) -> \(three : Nat) -> \(four : Nat) -> \(five : Nat) -> \(six : Nat) -> \(seven : Nat) -> \(eight : Nat) -> \(nine : Nat) -> \(ten : Nat) -> ( \(replicateM_ : Nat -> IO U -> IO U) -> \(ninetynine : Nat) -> replicateM_ ninetynine ((>>=) String U getLine putStrLn) ) -- replicateM_ ( \(n : Nat) -> \(io : IO U) -> foldNat n (IO U) ((>>) io) (return U Unit) ) -- ninetynine ((+) ((*) nine ten) nine) ) -- (>>) ( \(m : IO U) -> \(n : IO U) -> (>>=) U U m (\(_ : U) -> n) ) -- two ((+) one one) -- three ((+) one ((+) one one)) -- four ((+) one ((+) one ((+) one one))) -- five ((+) one ((+) one ((+) one ((+) one one)))) -- six ((+) one ((+) one ((+) one ((+) one ((+) one one))))) -- seven ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one)))))) -- eight ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one))))))) -- nine ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one)))))))) -- ten ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one))))))))) ) -- Nat ( forall (a : *) -> (a -> a) -> a -> a ) -- zero ( \(a : *) -> \(Succ : a -> a) -> \(Zero : a) -> Zero ) -- one ( \(a : *) -> \(Succ : a -> a) -> \(Zero : a) -> Succ Zero ) -- (+) ( \(m : forall (a : *) -> (a -> a) -> a -> a) -> \(n : forall (a : *) -> (a -> a) -> a -> a) -> \(a : *) -> \(Succ : a -> a) -> \(Zero : a) -> m a Succ (n a Succ Zero) ) -- (*) ( \(m : forall (a : *) -> (a -> a) -> a -> a) -> \(n : forall (a : *) -> (a -> a) -> a -> a) -> \(a : *) -> \(Succ : a -> a) -> \(Zero : a) -> m a (n a Succ) Zero ) -- foldNat ( \(n : forall (a : *) -> (a -> a) -> a -> a) -> n ) -- IO ( \(r : *) -> forall (x : *) -> (String -> x -> x) -> ((String -> x) -> x) -> (r -> x) -> x ) -- return ( \(a : *) -> \(va : a) -> \(x : *) -> \(PutStrLn : String -> x -> x) -> \(GetLine : (String -> x) -> x) -> \(Return : a -> x) -> Return va ) -- (>>=) ( \(a : *) -> \(b : *) -> \(m : forall (x : *) -> (String -> x -> x) -> ((String -> x) -> x) -> (a -> x) -> x ) -> \(f : a -> forall (x : *) -> (String -> x -> x) -> ((String -> x) -> x) -> (b -> x) -> x ) -> \(x : *) -> \(PutStrLn : String -> x -> x) -> \(GetLine : (String -> x) -> x) -> \(Return : b -> x) -> m x PutStrLn GetLine (\(va : a) -> f va x PutStrLn GetLine Return) ) -- putStrLn ( \(str : String) -> \(x : *) -> \(PutStrLn : String -> x -> x ) -> \(GetLine : (String -> x) -> x) -> \(Return : U -> x) -> PutStrLn str (Return Unit) ) -- getLine ( \(x : *) -> \(PutStrLn : String -> x -> x ) -> \(GetLine : (String -> x) -> x) -> \(Return : String -> x) -> GetLine Return ) )
If you type-check and normalize this program, the compiler will produce an unrolled syntax tree representing a program that echoes 99 lines from standard input to standard output:
$ morte < recursive.mt ∀(String : *)
Portability
You can use Morte as a standard format for transmitting code between functional languages. This requires you to encode the source language to Morte and decode the Morte into the destination language.
If every functional language has a Morte encoder/decoder, then eventually
there can be a code utility analogous to pandoc
that converts code written
any of these languages to code written in any other of these language.
Additionally, Morte provides a standard Binary
interface that
you can use for serializing and deserializing code. You may find this
useful for transmitting code between distributed services, even within
the same language.
Conclusion
The primary purpose of Morte is a proof-of-concept that a non-recursive calculus of constructions is the ideal system for the super-optimization of functional programs. Morte uses a simple, yet powerful, optimization scheme that consists entirely of normalizing terms using the ordinary reduction rules of lambda calculus. Morte emphasizes pushing optimization complexity out of the virtual machine and into the translation of abstractions to the calculus of constructions. However, that means that the hard work has only just begun and Morte still needs front-end compilers to translate from high-level functional languages to the calculus of constructions.
The secondary purpose of Morte is to serve as a standardized format for encoding and transmission of functional code between distributed services or different functional languages. Morte restricts itself to lambda calculus in order to reuse the large body of research for translating programming abstractions to and from the polymorphic lambda calculus.
Finally, you can use Morte as a equational reasoning engine to learn how high-level abstractions reduce to low-level abstractions. If you are teaching lambda calculus you can use Morte as a teaching tool for how to encode abstractions within lambda calculus.
If you have problems, questions, or feature requests, you can open an issue on the issue tracker on Github: