Safe Haskell	Safe-Inferred

Annah.Tutorial

Contents

Introduction
Let
Data types
Imports
Autogenerate Types
Folds
Recursive types
Prelude
Natural numbers
Lists
Monoids
Commands
IO
Paths
Conclusion

Description

Annah is a tiny language that serves to illustrate how various programming constructs can be desugared to lambda calculus. The most sophisticated feature that Annah supports is desugaring mutually recursive datatypes to non-recursive lambda expressions.

Annah is not intended to be used as a production language. Rather, Annah is a step along the way towards a production language that I factored out as a reusable library that others can learn from and possibly fork for their own use cases.

Under the hood, all Annah expressions are translated to a minimalist implementation of the calculus of constructions called Morte, which only supports non-recursive lambda expressions and their types. You can find the Morte compiler and library here:

http://hackage.haskell.org/package/morte

Annah piggybacks on Morte meaning all Annah expressions are translated to Morte expressions and then those Morte expressions are type-checked and evaluated. You cannot directly type-check or evaluate Annah expressions; you have to desugar them to Morte expressions first before you can do anything else with them.

Annah is not very user-friendly (and I apologize for that!). For example, Annah reuses Morte's type-checker which means that error messages are in terms of low-level lambda calculus expressions and not in terms of the original Annah source code.

Most notably, Annah does not provide support for text, due to the gross inefficiency of encoding even basic ASCII text in lambda calculus. Text handling would be better served by a backend with primitive support for text literals and operations on text.

This tutorial assumes that you have first read the Morte tutorial, which you can find here:

http://hackage.haskell.org/package/morte/docs/Morte-Tutorial.html

Annah is a superset of Morte that implements many of the higher-level constructs mentioned in the Morte tutorial, which is why you should not skip reading the Morte tutorial.

Synopsis

Introduction

This library comes with a binary executable that you can use to compile Annah expressions to Morte expressions. This executable can be used in two separate ways.

First, you can read an Annah expression from standard input and the program will output the equivalent low-level Morte expression to standard output:

 $ annah
 type Bool
 data True
 data False
 fold if
 in                                                   
     
 let not (b : Bool) : Bool = if b Bool False True
 in  not False
 <Ctrl-D>
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

Second, you can read an Annah expression in from a file if you provide the file name on the command line using the compile subcommand:

 $ cat example.annah
 type Bool
 data True
 data False
 fold if
 in                                                   
     
 let not (b : Bool) : Bool = if b Bool False True
 in  not False

 $ annah compile example.annah
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

Annah is a superset of Morte, so any Morte expression is also a valid Annah expression:

 $ annah
 \(a : *) -> \(x : a) -> x
 <Ctrl-D>
 λ(a : *) → λ(x : a)

Like Morte, Annah is an explicitly typed language (i.e. no type inference).

Let

Annah supports let expressions which can be used to introduce functions and values. For example, this is how you can define the polymorphic identity function in Annah:

 $ annah
 let id (a : *) (x : a) : a = x
 in  id
 <Ctrl-D>
 λ(a : *) → λ(x : a)

You can define more than one thing in a let expression as long as you prefix each definition with let:

 $ annah
 let id (a : *) (x : a) : a = x  
 let const (a : *) (b : *) (x : a) (y : b) : a = x
 in  id
 <Ctrl-D>
 λ(a : *) → λ(x : a)

The general form of a let expression is:

 let f0 (x00 : _A00) (x01 : _A01) ... (x0j : _A0j) _B0 = b0
 let f1 (x10 : _A10) (x11 : _A11) ... (x1j : _A1j) _B1 = b1
 ...
 let fi (xi0 : _Ai0) (xi1 : _Ai1) ... (xij : _Aij) _Bi = bi
 in  e

The above let expression desugars to the following lambda expression:

 (   λ(f0 : ∀(x00 : _A00) → ∀(x01 : _A01) → ... → ∀(x0j : _A0j) →  →   λ(f1 : ∀(x10 : _A10) → ∀(x11 : _A11) → ... → ∀(x1j : _A1j) → →   ... →   λ(fi : ∀(xi0 : _Ai0) → ∀(xi1 : _Ai1) → ... → ∀(xij : _Aij) → →   e )
 
 (λ(x00 : _A00) → λ(x01 : _A01) → ... → λ(x0j : _A0j) (λ(x10 : _A10) → λ(x11 : _A11) → ... → λ(x1j : _A1j) ...
 (λ(xi0 : _Ai0) → λ(xi1 : _Ai1) → ... → λ(xij : _Aij)

The above 'e' is the "body" of the let expression and f0 through fi are the "let-bound terms". Due to the above translation, each "let-bound" term is only in scope for the "body" of the let-expression and the types of subsequent "let-bound" terms.

To give a concrete example, our original id+const let expression:

 let id (a : *) (x : a) : a = x  
 let const (a : *) (b : *) (x : a) (y : b) : a = x
 in  id

... was equivalent to:

 (   λ(id : ∀(a : *) → ∀(x : a) →  →   λ(const : ∀(a : *) → ∀(b : *) → ∀(x : a) → ∀(y : b →   id )

 (λ(a : *) → λ(x : a) → (λ(a : *) → λ(b : *) → λ(x : a) → λ(y :

... which normalizes to:

 λ(a : *) → λ(x : a)

The definition of const is dead code that is optimized away by β-reduction because the let-bound const term is never used within the body of the let expression.

Data types

Annah lets you define datatypes that scope over an expression. For example, if you write:

 type Bool
 data True
 data False
 fold if
 in e

... then within the expression 'e' you will be able to use the Bool type, the True and False values, and the if fold.

The above definition of Bool desugars to the following let expression:

 let Bool  : *    = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo let True  : Bool = λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → let False : Bool = λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →  let if : Bool → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Boo     λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) in  e

... which in turn desugars to:

 (   λ(Bool : *) →   λ(True : Bool →   λ(False : Bool →   λ(if : Bool → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) →  →   e )
 
 (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Boo (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →  (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → F (λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)

Annah also supports recursive datatypes. For example, you can define natural numbers like this:

 $ annah
 type Nat
 data Succ (pred : Nat)
 data Zero
 in   Succ (Succ (Succ Zero))
 <Ctrl-D>
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ

Notice how we can omit the fold line, which is optional.

You can also omit field names, too, and this code is also valid:

 $ annah
 type Nat
 data Succ Nat
 data Zero
 in   Succ (Succ (Succ Zero))
 λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ

Field names are just used to give nicer names to bound variables in the desugared datatype definition and field names default to '_' if you omit the name.

You can find out how any given type or constructor is encoded by just returning the constructor as the result of the let expression:

 $ annah
 type Nat
 data Succ (pred : Nat)
 data Zero
 in   Succ
 λ(pred : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (pred Na

Imports

Annah supports imports using the same syntax as Morte but you may only import Morte expressions (not Annah expressions). You can embed a file path or http URL anywhere within an expression and Annah will substitute in the Morte expression (encoded as plain text) located at that path or URL.

The reason Annah does not support importing Annah expressions is that Annah does not actually resolve the imports. Annah piggybacks off of Morte's support for imports, and Morte only supports importing Morte expressions.

Imports are extremely useful when combined with datatypes because you can create a separate file for each type and constructor of a datatype. To illustrate this we'll manually encode Bool, True, False, and if as separate Annah files (and later we will see how we can auto-generate these files):

 $ cat Bool.annah
 type Bool
 data True
 data False
 fold if
 in   Bool

 $ cat True.annah
 type Bool
 data True
 data False
 fold if
 in   True

 $ cat False.annah
 type Bool
 data True
 data False
 fold if
 in   False

 $ cat if.annah
 type Bool
 data True
 data False
 fold if
 in   if

Then we will translate each of them to a file encoding the equivalent Morte expression without the ".annah" file suffix:

 $ annah compile  Bool.annah >  Bool
 $ annah compile  True.annah >  True
 $ annah compile False.annah > False
 $ annah compile    if.annah >    if

Now that we've created a file for each type and term we can import them within other expressions. For example, now we can define the not function in terms of imported types and values:

 $ cat not.annah
 let not (b : ./Bool ) : ./Bool = ./if b ./Bool ./False ./True
 in  not

Don't worry if you don't understand what the above expression means just yet. This tutorial will explain what the right-hand side means in the section on "Folds".

We can run this file through Annah, which will desugar and normalize the expression, but will preserve the original imports:

 $ annah compile not.annah > not
 $ cat not
 λ(b : ./Bool ) → ./if  b ./Bool  ./False  ./Tru

Annah actually does resolve the imports for the purposes of type-checking the expression, but deliberately does not resolve the imports for the final normalized expression. Annah does this to keep the expression "dynamically linked" so that the expression can continue to reflect changes to dependencies.

If you prefer to statically link the expression then you can use Morte:

 $ echo "./not" | morte
 ∀(b : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool)  
 λ(b : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → b (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False) (λ(Bool : *) → λ(True : Bool) → λ(Fa

... and you can also expand derived expressions, too:

 $ morte
 ./not ./True
 <Ctrl-D>
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo 
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

... desugaring them with Annah if necessary:

 $ annah | morte
 let doubleNegate (b : ./Bool ) : /Bool = ./not (./not b)
 in  doubleNegate ./True
 <Ctrl-D>
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

Autogenerate Types

Creating one file per type, fold, and data constructor gets tedious pretty quickly, so the annah executable provides a convenient subcommand named types for auto-generating these files.

Just run the annah types command and provide a datatype definition on standard input:

 $ annah types
 type Bool
 data True
 data False
 fold if
 <Ctrl-D>

... and annah will create one directory for each type in the datatype definition:

 $ ls
 Bool/  Bool.annah

Each type's directory will have two files per data constructor associated with the type and two files for the fold, too:

 $ ls Bool
 @  False  False.annah  if  if.annah  True  True.annah

Everything comes in two flavors: the original Annah code and the equivalent Morte code:

 $ cat Bool/True.annah 
 type Bool
 data True
 data False
 fold if
 in   True
 $ cat Bool/True
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

The Morte code for the type is located as a file named @ underneath the type's directory:

 $ cat Bool.annah
 type Bool
 data True
 data False
 fold if
 in   Bool
 $ cat Bool/@
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo

This is because Morte supports importing the directory by name if there is a file named @ underneath the directory. So, for example if you import .Bool@ and it's a directory then Morte will import @.\Bool/@ instead:

 $ morte
 ./Bool
 <Ctrl-D>
 *
 
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo

Folds

Every datatype definition comes with an optional fold which you can use to pattern match on a value of that type. You can see what arguments the pattern match expects just by querying the type of the fold:

 $ morte
 ./Bool/if
 <Ctrl-D>
 ∀(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool)  
 λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)

... and we can use imports to simplify the type to:

 ∀(x : ./Bool ) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → B

This type says that if expects the following arguments:

A value named x of type ./Bool to pattern match on (like ./Bool/True or ./Bool/False) * The type of the result for each branch of the pattern match * The result to return if our value equals ./Bool/True * The result to return if our value equals ./Bool/False

Carefully note that the second argument is named Bool but can actually be any type. Similarly, the third and fourth arguments are named after the True and False constructors but they actually represent how to handle each branch of the pattern match.

So, for example, when we write:

 let not (b : ./Bool ) : ./Bool = ./if b ./Bool ./False ./True
 in  not

... it's as if we wrote the following Haskell code using pattern matching:

 let not :: Bool -> Bool
     not b = case b of
             True  -> False
             False -> True
 in  not

We could even format our code to parallel the layout of a Haskell pattern match:

 let not (b : ./Bool ) : ./Bool =
     ./if b ./Bool
     ./False
     ./True
 in  not

The only difference is that in the Annah code we have to explicitly supply the expected type of the result after the value that we pattern match on (i.e. the .Bool@ immediately after the @.if b).

Our .not@ function technically did not need to use the @.if fold. For example, we could instead write:

 $ cat not.annah
 let not (b : ./Bool ) : ./Bool = b ./Bool ./False ./True
 in  not

The ./if was unnecessary because it was just the identity function on ./Bools:

 $ cat if
 λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)

.. which is the same as:

 λ(x : ./Bool ) →

The reason we can omit the if is that all values of type ./Bool are already preformed pattern matches. We can prove this to ourselves by consulting the definitions of ./Bool/True and ./Bool/False:

 $ morte < ./Bool/True
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo 
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → $ morte < ./Bool/False
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo 
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

In other words, ./Bool/True is just a preformed pattern match that always returns the first branch that you supply. Vice versa, ./Bool/False is just a preformed pattern match that always returns the second branch that you supply.

In fact, all folds are optional when you save a type and associated data constructors as separate files. The only time we truly require the fold is when we pattern match on the type within the body of a datatype expression, like in our very first example:

 type Bool
 data True
 data False
 fold if
 in -- Everything below here is the "body" of the `Bool` datatype definition

 let not (b : Bool) : Bool = if b Bool False True
 in  not False

Bool and ./Bool are not the same type within the body of the Bool datatype definition. If you omit the if then you will get the following type error:

 $ annah
 type Bool
 data True
 data False
 fold if
 in
 
 let not (b : Bool) : Bool = b Bool False True
 in  not False
 <Ctrl-D>
 annah: 
 Context:
 Bool : *
 True : Bool
 False : Bool
 if : ∀(x : Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → B b : Bool
 
 Expression: b Bool
 
 Error: Only functions may be applied to values

The Context the compiler prints in the error message shows that the type-checker views the Bool type as abstract and not the type of a pattern match. However, the same Context says that if has the correct type to convert between the abstract Bool type and the type we expect for a pattern match:

 if : ∀(x : Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → B

... which we can simplify to just:

 -- The type of the bound variable named `if`
 if : ∀(x : Bool) → ./Bool

In other words, Bool and ./Bool are different types from the type checker's point of view. That is why you must explicitly convert from Bool to ./Bool using if while inside that context.

However, once you save .Bool@, @.True, .False@ and @.if to separate files the distinction between Bool and ./Bool vanishes. The type of ./if (the file) is not the same as the type of if (the bound variable):

 -- The type of the file named `./if`
 ./if : ∀(x : ./Bool ) → ./Bool

You can deduce why the distinction disappears when you save things to separate files if you desugar the datatype definitions. For example our if.annah file was defined as:

 type Bool
 data True
 data False
 fold if
 in   if

We can use the annah desugar subcommand to see what that code desugars to before normalization:

 $ annah desugar < ./Bool/if.annah
 (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → λ(if : ∀(x : Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → if) (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True) (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False) (λ(x : ∀(Bool : *) → ∀(True : Bool)

... which we can clean up a bit to get:

 (   λ(Bool : *) →   λ(True : Bool →   λ(False : Bool →   λ(if : Bool → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) →  →   if )
 
 (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Boo (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →  (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → F (λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)

That then normalizes to;

 $ annah desugar < ./Bool/if.annah | morte
 ∀(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool)  
 λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)

There is also another use for storing folds as files and using them, even if they are not immediately necessary. Saving a fold to a file lets you provide a stable interface for pattern matching on a value if you ever want to change the internal implementation of a type without breaking backwards compatibility.

For example, suppose that a user writes the following not function using ./if:

 let not (b : ./Bool ) : ./Bool = ./if b ./Bool ./False ./True
 in  not

... but we later decide we want to flip the order of of the True and False constructors in our datatype definition:

 $ annah types
 type Bool
 data False
 data True

The above changes would break the user's code unless we change ./if to export the pattern match order that the user expects:

 $ cat > if
     \(b : ./Bool )
 ->  \(Bool : *)
 ->  \(True : Bool)
 ->  \(False : Bool)
 ->  b Bool False True
 <Ctrl-D>

Now the user's code continues to work as if nothing ever happened.

So saving folds to files and using them to pattern match is not strictly necessary, but if you do use them then you can change the underlying implementation of the type without breaking backwards compatibility.

There's no way that you can force users to use the fold that you provide since all saved expressions are encoded in lambda calculus, which does not provide any support for implementation hiding or encapsulation. The best you can do is to simply warn users that you might break their code some day if they perform a "raw pattern match" (i.e. a pattern match without the use of a saved fold).

Recursive types

Annah supports recursive and mutually recursive types. We saw an example of recursive types with natural numbers:

 $ annah
 type Nat
 data Succ (pred : Nat)
 data Zero
 fold foldNat

 in   Succ (Succ (Succ Zero))
 <Ctrl-D>
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ

What might not be obvious is that if you save each type and constructor to a separate file then you can build a natural number just from the files.

To illustrate this, we will compile our datatype definition to separate files:

 $ annah types
 type Nat
 data Succ (pred : Nat)
 data Zero
 fold foldNat
 <Ctrl-D>

... and now we can build natural numbers using these files:

 $ morte
 ./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ

This gives the exact same result as before, but now we are programming directly at the top level using files instead of programming inside the body of a datatype definition.

We can also fold natural numbers using our ./Nat/foldNat function. Let's consult the type of the function:

 ∀(x : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Na 
 λ(x : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat

If we clean up that type we get:

     ∀(x : ./Nat )
 →   ∀(Nat : *) →   ∀(Succ : ∀(pred : Nat) → Nat →   ∀(Zero : Nat) →   Nat

Conceptually, when we fold a .Nat@ value using @.\Nat/foldNat we just replace each ./Nat/Succ constructor with the argument of the fold labeled Succ (i.e. the third argument). Similarly, we substitute each ./Nat/Zero constructor with the fourth argument labeled Zero.

We also supply a type parameter named Nat as the second argument. This type parameter must match the input and output of whatever we use to replace the ./Nat/Succ and ./Nat/Zero.

For example, suppose that we wanted to write a function to test if a ./Nat was an even number. We would just substitute every Zero constructor with ./Bool/True and substitute every ./Nat/Succ constructor with ./not. The code for that would be:

 $ cat not.annah  # Update `not.annah` to use our new file layout
 let not (b : ./Bool ) : ./Bool =
     ./Bool/if b ./Bool
         ./Bool/False
         ./Bool/True
 in  not

 $ cat isEven.annah 
 let isEven (n : ./Nat ) : ./Bool =
     ./Nat/foldNat n ./Bool
         ./not       -- Replace every `./Nat/Succ` with `./not`
         ./Bool/True -- Replace every `./Nat/Zero` with `./Bool/True`
 in  isEven

The let definitions are not strictly necessary since we could just write:

 $ cat not.annah
 \(b : ./Bool ) ->
     ./Bool/if b ./Bool
         ./Bool/False
         ./Bool/True

 $ cat isEven.annah
 \(n : ./Nat ) ->
     ./Nat/foldNat n ./Bool
         ./not
         ./Bool/True

... but the let definitions help the readability of the code by naming the functions and documenting their expected return types.

Then we can compile our Annah expression to Morte code:

 $ annah compile    not.annah > not
 $ annah compile isEven.annah > isEven

... and test that ./isEven works:

 $ morte
 ./isEven (./Nat/Succ (./Nat/Succ ./Nat/Zero ))
 <Ctrl-D>
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo 
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

It works! The result is identical to ./Bool/True:

 $ morte
 ./Bool/True
 <Ctrl-D>
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

Conceptually, what happened was that ./isEven just performed the desired substitutions, replacing every ./Nat/Succ with ./not and replacing every ./Nat/Zero with ./Bool/True:

 ./isEven (./Nat/Succ (./Nat/Succ ./Nat/Zero ))

 -- Constructor substitution
 = ./not (./not ./Bool/True )

 -- β-reduce = ./Bool/True

Note that this is not really the path the compiler takes under the hood, but it's equivalent.

We can also encode mutually recursive types such as the following type declaration for even and odd numbers:

 $ annah
 type Even
 data SuccE (predE : Odd)
 data ZeroE
 fold foldEven
 
 type Odd
 data SuccO (predO : Even)
 fold foldOdd
 
 in SuccE (SuccO ZeroE)
 λ(Even : *) → λ(Odd : *) → λ(SuccE : ∀(predE : Odd) → Even) → λ(ZeroE : Even) → λ(SuccO : ∀(predO : Even) → Odd) → SuccE (S

Like before, we can encode each type and term separately as files and the files:

 annah types
 type Even
 data SuccE (predE : Odd)
 data ZeroE
 fold foldEven
 
 type Odd
 data SuccO (predO : Even)
 fold foldOdd
 <Ctrl-D>

... and now these files can be used to build .Even@ or @.Odd values:

 $ morte
 ./Even/SuccE (./Odd/SuccO ./Even/ZeroE )
 <Ctrl-D>
 ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd)  
 λ(Even : *) → λ(Odd : *) → λ(SuccE : ∀(predE : Odd) → Even) → λ(ZeroE : Even) → λ(SuccO : ∀(predO : Even) → Odd) → SuccE (S

We can also consume mutually recursive types just by folding them. Each type is already a preformed fold and we can consult each type's respective fold function to see what arguments the fold expects:

 $ morte
 ./Even/foldEven
 <Ctrl-D>
 ∀(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Even) → ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) 
 λ(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → E

 $ morte
 ./Odd/foldOdd
 ∀(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Odd) → ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even 
 λ(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) →

If we clean up the type of the ./Even/foldEven function we get this:

     ∀(x : ./Even )
 →   ∀(Even : *) →   ∀(Odd : *) →   ∀(SuccE : ∀(predE : Odd) → Even →   ∀(ZeroE : Even) →   ∀(SuccO : ∀(predO : Even) → Odd →   Even

Conceptually, when we fold an .Even@ value using @.\Even/foldEven we just replace each ./Even/SuccE constructor with the argument of the fold labeled SuccE (i.e. the fourth argument). Similarly, we substitute each ./Even/ZeroE constructor with the fifth argument named ZeroE and substitute each ./Odd/SuccO constructor with the sixth argument named SuccO.

We also supply two type parameters named Even and Odd. These type parameters must match the input and output of whatever we use to replace the SuccE, ZeroE and SuccO constructors.

For example, suppose that we wanted to write a function that converts an .Even@ value to a @.Nat. We would just replace every ./Even/SuccE and ./Odd/SuccO constructor with Succ and replace every ./Even/ZeroE constructor with Zero, like this:

 $ cat evenToNat.annah
 let evenToNat (e : ./Even ) : ./Nat =
     ./Even/foldEven e ./Nat ./Nat
         ./Nat/Succ  -- Replace every `./Even/SuccE` with `Succ`
         ./Nat/Zero  -- Replace every `./Even/ZeroE` with `Zero`
         ./Nat/Succ  -- Replace every `./Odd/SuccO`  with `Succ`
 in  evenToNat

Now we can "compile" our evenToNat function to Morte code:

 annah evenToNat.annah > evenToNat

... and test that it correctly converts ./Even values to their equivalent ./Nat values:

 $ morte
 ./evenToNat (./Even/SuccE (./Odd/SuccO ./Even/ZeroE ))
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ

It works! We can began with the number two, encoded as an ./Even number and ended with two encoded as a ./Nat.

As before, the ./evenTonat function was just performing the desired substitution, replacing each ./Even/SuccE and ./Odd/SuccO with ./Nat/Succ and replacing ./Odd/ZeroE with ./Nat/Zero:

 ./evenToNat (./Even/SuccE (./Odd/SuccO ./Even/ZeroE ))

 -- Constructor substitution
 = ./Nat/Succ (./Nat/Succ ./Nat/Zero )

Again, this is not the path the compiler takes under the hood, but it's equivalent.

Prelude

Annah also comes with a Prelude of utility types and terms. This Prelude is hosted remotely here:

http://sigil.place/prelude/annah/1.0/

You can visit the above link to browse the Prelude and see what is available.

There are several ways that you can use the Prelude. The most direct approach is to use expressions from the Prelude directly by referencing their URLs, like this:

 $ morte
 http://sigil.place/prelude/annah/1.0/Nat/Succ
 (   http://sigil.place/prelude/annah/1.0/Nat/Succ
     (   http://sigil.place/prelude/annah/1.0/Nat/Succ
         http://sigil.place/prelude/annah/1.0/Nat/Zero
     )
 )
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ

... or you can selectively "alias" remote references locally by creating local files that refer to the remote URLs:

 $ echo "http://sigil.place/prelude/annah/1.0/Nat/Succ" > Succ
 $ echo "http://sigil.place/prelude/annah/1.0/Nat/Zero" > Zero
 $ morte
 ./Succ (./Succ (./Succ ./Zero ))
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ

... or you can "import" the entire Prelude into your current directory using wget:

 $ wget -np -r --cut-dirs=3 http://sigil.place/prelude/annah/1.0/
 $ cd sigil.place
 $ ls
 (->)            Defer.annah    List.annah    Path         Sum0.annah
 (->).annah      Eq             Maybe         Path.annah   Sum1
 Bool            Eq.annah       Maybe.annah   Prod0        Sum1.annah
 Bool.annah      Functor        Monad         Prod0.annah  Sum2
 Category        Functor.annah  Monad.annah   Prod1        Sum2.annah
 Category.annah  index.html     Monoid        Prod1.annah
 Cmd             IO             Monoid.annah  Prod2
 Cmd.annah       IO.annah       Nat           Prod2.annah
 Defer           List           Nat.annah     Sum0

This tutorial will assume that you have imported the Prelude locally.

The Prelude is organized according to the following rules:

Each type (like .Bool@ or @.Nat) is a top-level directory. You can reference that type in your code by its directory * Each constructor of that type lives underneath the type's directory. For example, True is located underneath the ./Bool directory * Functions associated with each type are also located underneath the type's directory. For example, the length function is located underneath the ./List directory. * Every expression is provided as both the original Annah code (with a *.annah suffix) and Morte code (with no suffix). For example, you will find the Monoid.annah file which was the Annah expression used to create the Monoid file which is a Morte expression.

In order to use an expression within Morte you must explicitly import the expression within the Morte code, like this:

 $ echo "./List/length" | morte  # Good
 ∀(a : *) → ∀(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Nil :  
 λ(a : *) → λ(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → xs Nat (λ

Reading the expression through standard input will (usually) not work:

 $ morte < List/length  # Bad
 ../List: openFile: does not exist (No such file or directory)

The reason why is that everything in the Prelude uses relative imports to reference each other. This is what allows the Prelude to correctly function both when you reference the Prelude remotely and when you download the Prelude locally. If you read the expression through standard input then Morte incorrectly concludes that any further imports are relative to your current directory. However, if you explicitly import the expression within the code then Morte correctly concludes that transitive imports are relative to the imported file's path.

For example, the List/length file has the following contents:

 cat List/length
 λ(a : *) → λ(xs : ../List  a) → λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → xs Nat (λ(_ :

There is one relative reference within that file to ../List. That reference is relative to the current file's directory (i.e. relative to List/) which means that it still points to the same directory: List. We could have also used just . to refer to the current directory but that would be less readable.

However, if you read in List/length from standard input, then morte looks for ../List expression relative to your present working directory and fails.

Annah's Prelude has some similarities to Haskell's standard libraries and some differences. The rough correspondences are:

(->) corresponds to Haskell's (->) type constructor * Bool corresponds to Haskell's Bool type * Cmd corresponds to the operational monad (i.e. Control.Monad.Operational.Program) * Defer corresponds to Data.Functor.Coyoneda.Coyoneda * List corresponds to Haskell lists except that Annah Lists are always finite because they are encoded recursively * Maybe corresponds to Haskell's Maybe type constructor * Nat corresponds to Haskell's Natural type, except much less efficient than its Haskell counterpart * Path corresponds to a free category. As far as I know there is no standard Haskell implementation for free categories to reference * Prod0 corresponds to Haskell's () type. Mnemonic: "Product type with zero fields" * Prod1 corresponds to Haskell's Identity type constructor. Mnemonic: "Product type with one field" * Prod2 corresponds to Haskell's 2-tuple type constructor. Mnemonic: "Product type with two fields" * Sum0 corresponds to Haskell's Void type. Mnemonic: "Sum type with zero fields" * Sum1 also corresponds to Haskell's Identity type constructor. Mnemonic: "Sum type with one field" * Sum2 corresponds to Haskell's Either type constructor. Mnemonic: "Sum type with two fields" * IO corresponds to a very simple IO type constructor that only supports two operations:

 ./IO/get : ./IO ./Nat
 ./IO/put : ./Nat -> ./IO ./Prod0

In addition to those types, Annah also encodes several of Haskell's type classes as values. Neither Annah nor Morte supports type classes per se. Instead, each class is encoded as a type constructor and each instance is a term of the corresponding type:

Functor corresponds to Haskell's Functor class * Monoid corresponds to Haskell's Monoid class * Monad corresponds to Haskell's Monad class * Category corresponds to Haskell's Category class

However, the specification of each type class radically differs from how Haskell encodes things. We'll revisit this in a later section.

Natural numbers

The Prelude provides addition and multiplication for natural numbers:

 $ cat > three
 ./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))
 <Ctrl-D>

 $ morte
 ./Nat/(+) ./three ./three
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zer

 $ morte
 ./Nat/(*) ./three ./three
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))

Also, Annah provides basic syntactic support for natural number literals:

 $ annah | morte
 ./Nat/(+) 3 3
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zer

 $ annah | morte
 ./Nat/(*) 3 3
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))

Lists

The Prelude provides operations on lists, too:

 $ annah | morte
 ./List/replicate ./Bool 3 ./Bool/True
 <Ctrl-D>
 ∀(List : *) → ∀(Cons : ∀(head : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(tail : List) → List) → ∀(Nil : List) 
 λ(List : *) → λ(Cons : ∀(head : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(tail : List) → List) → λ(Nil : List) → Cons (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True) (Cons (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True) (Cons (λ(Bool : *) → λ(True : Bool) → λ

Annah also provides support for list literals:

 $ annah > bools
 [nil ./Bool , ./Bool/True , ./Bool/False , ./Bool/True ]
 <Ctrl-D>

 $ cat bools
 λ(List : *) → λ(Cons : ∀(head : ./Bool ) → ∀(tail : List) → List) → λ(Nil : List) → Cons ./Bool/True  (Cons ./Bool/False  (Cons ./Bool/True

The general format for lists is:

 [nil elementType, element0, element1, ..., elementN]

Here are some examples of operations on lists:

 $ morte
 ./List/null ./Bool ./bools
 <Ctrl-D>
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo 
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

 $ morte
 ./List/length ./Bool (./List/(++) ./Bool ./bools ./bools )
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Nil : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Nil : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Ni

 $ annah | morte
 \(a : *) -> \(xs : ./List a) -> ./List/(++) a xs [nil a]
 <Ctrl-D>
 ∀(a : *) → ∀(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → ∀(List : *) → ∀(Cons : a → List → List) → ∀(Nil : L 
 λ(a : *) → λ(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → Li

The last example shows how morte can optimized away xs ++ [] to just xs.

Monoids

Annah also provides several folds on lists, like sum or and:

 $ annah | morte
 <Ctrl-D>
 ./Nat/sum [nil ./Nat , 1, 2, 3, 4]
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))

 $ annah | morte
 <Ctrl-D>
 ./Bool/and [nil ./Bool , ./Bool/True , ./Bool/False , ./Bool/True ]
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo 
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

What's interesting about these folds is their type:

 $ cat Nat/sum.annah
 let sum : ../Monoid ../Nat = \(xs : ../List ../Nat ) -> xs ../Nat ./(+) 0
 in  sum

 $ cat Bool/and.annah
 let and : ../Monoid ../Bool =
     \(xs : ../List ../Bool ) -> xs ../Bool ./(&&) ./True
 in  and

You might have been expecting their types to be something like this:

 sum : ../List ../Nat  -> ../Nat
 and : ../List ../Bool -> ../Bool

... and you would have been right because that is actually what their types are! This is because of how ./Monoid.annah is defined:

 $ cat Monoid.annah
 let Monoid (m : *) : * = ./List m -> m
 in  Monoid

In other words, a Monoid "instance" for a type m is just a function that folds a .List@ of @m@s into a single @m@. The @.sum and ./and functions that fold lists also double as ./Monoid instances.

You can recover the traditional Haskell Monoid operations like mempty and mappend from the above ./Monoid definition:

 $ cat Monoid/mempty.annah
 let mempty (m : *) (monoid : ./Monoid m) : m =
     monoid [nil m]
 in  mempty

 $ cat Monoid/mappend.annah
 let mappend (m : *) (monoid : ./Monoid m) (l : m) (r : m) : m =  
     monoid [nil m, l, r]
 in  mappend

For example:

 $ morte
 ./Monoid/mempty ./Nat ./Nat/sum
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat)

 $ annah | morte
 ./Monoid/mappend ./Nat ./Nat/sum 4 5
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))

However, in practice it's easier to just use the folds directly instead of using ./Monoid/mempty or ./Monoid/mappend:

 $ annah | morte
 ./Nat/sum [nil ./Nat ]
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat)

 $ annah | morte
 ./Nat/sum [nil ./Nat , 4, 5]
 <Ctrl-D>
 ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →  
 λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))

Commands

Annah also provides syntactic support for chaining commands using do notation, in a style very similar to Haskell. The following examples will all give very large outputs so I will tidy the output results, although there is not a good way to tidy the output in general:

For example, here is how you write a list comprehension in Annah.

 $ annah | morte  # Output cleaned up by hand
 ./List/Monad ./Nat (do ./List {
     x : ./Nat <- [nil ./Nat , 1, 2, 3];
     y : ./Nat <- [nil ./Nat , 4, 5, 6];
     _ : ./Nat <- ./List/pure ./Nat (./Nat/(+) x y);
 })
 <Ctrl-D>
     ∀(List : *)
 →   ∀(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List) → →   ∀(Nil : List) →   List 
     λ(List : *) →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List)  →   λ(Nil : List →   Cons     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ Zer     (   Cons
         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero         (   Cons
             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)             (   Cons
                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero                 (   Cons
                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)                     (   Cons
                         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))                         (   Cons
                             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)                             (   Cons
                                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))                                 (   Cons
                                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))                                     Nil
                                 )
                             )
                         )
                     )
                 )
             )
         )
     )

... which is equivalent to:

 ./List ./Nat

 [nil ./Nat , 5, 6, 7, 6, 7, 8, 7, 8, 9]

Annah do notation has a few important differences from Haskell's do notation:

Every command's return type must be annotated; even the final command * Braces are required and semicolons are required on all lines * You must annotate the monad's type constructor right after the do * You (usually) wrap the do block in the ./Monad instance for your type constructor followed by the do block's return value

Here is an example diagram to illustrate the last rule:

 +-- Monad instance for ./List
 |
 |            +-- The return value of block ...
 |            |
 v            v
 ./List/Monad ./Nat (do ./List {
     x : ./Nat <- [nil ./Nat , 1, 2, 3];
     y : ./Nat <- [nil ./Nat , 4, 5, 6];
     _ : ./Nat <- ./List/pure ./Nat (./Nat/(+) x y);
 })      ^
         |
         +-- ... which must match this return value

You actually don't have to wrap the do block in a ./Monad instance, but you will get a different result. Let's see what happens if we omit the ./Monad instance:

 $ annah | morte  # Output cleaned up by hand
 do ./List {
     x : ./Nat <- [nil ./Nat , 1, 2, 3];
     y : ./Nat <- [nil ./Nat , 4, 5, 6];
     _ : ./Nat <- ./List/pure ./Nat (./Nat/(+) x y);
 }
 <Ctrl-D>
     ∀(Cmd : *)
 →   ∀(Bind : ∀(b : *) → (∀(List : *) → ∀(Cons : ∀(head : b) → ∀(tail : List) → List) → ∀(Nil : List) → List) → (b → Cm →   ∀(Pure : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → →   Cmd
     λ(Cmd : *) →   λ(Bind : ∀(b : *) → (∀(List : *) → ∀(Cons : ∀(head : b) → ∀(tail : List) → List) → ∀(Nil : List) → List) → (b → C →   λ(Pure : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat)  →   Bind     (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → N     (   λ(List : *)     →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List)      →   λ(Nil : List     →   Cons         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → S         (   Cons
             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ              (   Cons
                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Z                 Nil
             )
         )
     )
     (   λ(x : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →      →   Bind         (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → N         (   λ(List : *)         →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List)          →   λ(Nil : List         →   Cons             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze             (   Cons
                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ Zer                 (   Cons
                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero                     Nil
                 )
             )
         )
         (   λ(y : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) →          →   Bind             (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → N             (   λ(List : *)             →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List)              →   Cons                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → x Nat Succ (y Nat Succ              )
             Pure
         )
     )

... which is equivalent to:

 ./Cmd ./List./Nat

     λ(Cmd : *) →   λ(Bind : ∀(b : *) → ./List b → (b → Cmd) → →   λ(Pure : ./Nat → Cm →   Bind     ./Nat
     [nil ./Nat , 1, 2, 3]
     (   λ(x : ./Nat )     →   Bind         ./Nat
         [nil ./Nat 4, 5, 6]
         (   λ(y : ./Nat )         →   Bind             ./Nat
             [nil ./Nat (./Nat/(+) x y)]
             Pure
         )
     )

The do notation is desugaring to a data type named ./Cmd that inserts placeholders for each <- (pronounced: "bind"). In the Haskell world this datatype is commonly known as the "operational" monad.

So why did we wrap the do block in ./List/Monad? Well, let's check out the type of the ./List/Monad function:

 $ cat ./List/Monad.annah 
 let Monad: ../Monad ../List
     =   \(a : *)
     ->  \(m : ../Cmd ../List a)
     ->  m (../List a) (\(b : *) -> ./(>>=) b a) (./pure a)
 in  Monad

Hmmm, that's weird. Wasn't it supposed to be a function? Actually, it is! To see why, let's check out how ./Monad is defined:

 let Monad (m : * -> *) : * = forall (a : *) -> ./Cmd m a -> m a
 in  Monad

A .Monad m@ is a function that transforms a @.Cmd m a into an m a by replacing each Bind with the correct "bind" operation for that Monad and replaces each Pure with the correct "pure" operation for that Monad. Therefore a ./Monad ./List is a function that transforms a ./Cmd ./List a into a ./List a.

That's why we wrap the do block in ./List/Monad because the do block starts out with this type:

 do ./List { ... } : ./Cmd ./List ./Nat

... and then when we apply the ./List/Monad function we get back a bona-fide ./List:

 ./List/Monad ./Nat (do ./List { ... }) ./List ./Nat

There are a couple of parallels between Annah's .Monad@ + @.Cmd and Annah's .Monoid@ + @.List:

Both of them have syntactic support for building a placeholder of some sort. List notation builds a .List@ and @do@ notation builds a @.Cmd * Both of them have a way to fold the placeholder into a single value. .Monoid@s fold @.Lists and .Monad@s fold @.Cmds.

IO

Annah also supports a very simplistic ./IO type as a proof of concept for how you would model a foreign function interface. For example, here is an .IO@ action that reads a @.Nat and writes out the same ./Nat:

 $ annah
 ./IO/Monad ./Prod0 (do ./IO {
     n : ./Nat   <- ./IO/get  ;
     _ : ./Prod0 <- ./IO/put n;
 })
 <Ctrl-D>
 ./IO/Monad  ./Prod0  (λ(Cmd : *) → λ(Bind : ∀(b : *) → ./IO  b → (b → Cmd) → Cmd) → λ(Pure : ./Prod0  → Cmd) → Bind ./Nat  ./IO/get  (λ(n : ./Nat ) → Bind ./Prod0  (./IO/pu

Annah also provides utilities similar to Haskell for chaining commands, such as ./Monad/replicateM_.annah which lets you repeat a command a fixed number of times:

 $ cat Monad/replicateM_.annah
 let replicateM_ (m : * -> *) (n : ../Nat ) (cmd : m ../Prod0 )
   : ../Cmd m ../Prod0
   = ./sequence_ m (../List/replicate (m ../Prod0 ) n cmd)
 in  replicateM_

Notice that ./Monad/replicateM_ does not take a ./Monad instance as an argument. Instead, ./Monad/replicateM_ returns a ./Cmd which you can fold with the appropriate ./Monad instance:

For example:

 $ annah | morte  # Output cleaned up by hand
 ./IO/Monad ./Prod0 (./Monad/replicateM_ ./IO 10 (./IO/put 4))
     ∀(IO : *)
 →   ∀(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO) →   ∀(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO →   ∀(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) →  →   IO 
     λ(IO : *) →   λ(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO →   λ(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → I →   λ(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → →   Put_     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze     (   Put_
         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze         (   Put_
             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze             (   Put_
                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze                 (   Put_
                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze                     (   Put_
                         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze                         (   Put_
                             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze                             (   Put_
                                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze                                 (   Put_
                                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze                                     (   Put_
                                         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Ze                                         (Pure_ (λ(Prod0 : *) → λ(Make : Prod0) → Mak                                     )
                                 )
                             )
                         )
                     )
                 )
             )
         )
     )

If you clean that up a bit you get a syntax tree for printing 4 10 times:

     λ(IO : *) →   λ(Get_ : (./Nat → IO) →  →   λ(Put_ : ./Nat → IO →  →   λ(Pure_ : ./Prod0 → I →   Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Pure_ ./Prod0/Make ))))))))))

Let's try a more complicated program, that reads and writes integers 10 times:

 $ annah | morte
 let io : ./IO ./Prod0 = ./IO/Monad ./Prod0 (do ./IO {
     n : ./Nat   <- ./IO/get  ;
     _ : ./Prod0 <- ./IO/put n;
 })
 in  ./IO/Monad ./Prod0 (./Monad/replicateM_ ./IO 10 io)
 <Ctrl-D>
 ∀(IO : *) → ∀(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO) → IO) → ∀(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO → IO) → ∀(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → 
 λ(IO : *) → λ(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO) → IO) → λ(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO → IO) → λ(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → IO) → Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : N

... which if we simplify we get:

     λ(IO : *) →   λ(Get_ : (./Nat → IO) →  →   λ(Put_ : ./Nat → IO →  →   λ(Pure_ : ./Prod0 → I →   Get_ (λ(r : ./Nat )       Put_ r (
         Get_ (λ(r : ./Nat )            Put_ r (
             Get_ (λ(r : ./Nat )                Put_ r (
                 Get_ (λ(r : ./Nat )                    Put_ r (
                     Get_ (λ(r : ./Nat )                        Put_ r (
                         Get_ (λ(r : ./Nat )                            Put_ r (
                             Get_ (λ(r : ./Nat )                                Put_ r (
                                 Get_ (λ(r : ./Nat )                                    Put_ r (
                                     Get_ (λ(r : ./Nat )                                        Put_ r (
                                         Get_ (λ(r : ./Nat )                                            Put_ r (
                                             Pure_ ./Prod0/Make))))))))))))))))))))

In other words, we've built an abstract syntax tree representing ten Get_ and Put_ nodes where each Get_ node threads its result to the next Put_ node.

Annah cannot run this abstract syntax tree since Annah does not have a backend to interpret this tree. The most Annah can do is model effects without running them.

Paths

Annah provides support for the Category type class, too, using an approach very similar to the support for Monoid and Monad:

Provide a placeholder type named ./Path (which is a "free category") * Provide syntactic support for building ./Paths * Define a .Category@ to be something that folds @.Paths

 $ cat Category.annah
 let Category (cat : * -> * -> *) : * =
     forall (a : *) -> forall (b : *) -> ./Path cat a b -> cat a b
 in  Category

Here is an example of composing several functions using the ./Category instance for functions:

 $ annah | morte
 let even (n : ./Nat ) : ./Bool = n ./Bool ./Bool/not ./Bool/True

 in  let f : ./List ./Nat -> ./Bool =
     ./(->)/Category (./List ./Nat ) ./Bool
         [id ./(->) { ./List ./Nat } ./Nat/sum { ./Nat } even { ./Bool } ./Bool/not { ./Bool }]

     in  f [nil ./Nat , 1, 2, 3, 4
 <Ctrl-D>
 ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bo 
 λ(Bool : *) → λ(True : Bool) → λ(False : Bool) →

The above code creates a composition chain of three functions, reading from left to right:

./Natsum@, which has type @.\List ./Nat -> ./Nat * even, which has type ./Nat -> ./Bool * ./Bool/not, which has type ./Bool -> ./Bool

Annah's path notation requires you to annotate the types along the way as you compose each component. In the above example, you can find each function's input type immediately to the left of that function and the output type immediately to the right of each function. Types are surrounded by braces to separate them from the things you compose.

Annah's path notation differs from lists in a couple of ways:

You replace nil with id * The id is followed by the type constructor that you are chaining * You replace commas with intermediate types

You may find the notation easier to read if you put each composable component on a separate line preceded by the corresponding input type:

 let even (n : ./Nat ) : ./Bool = n ./Bool ./Bool/not ./Bool/True

 in  let f : ./List ./Nat -> ./Bool =
     ./(->)/Category (./List ./Nat ) ./Bool [id ./(->)
         { ./List ./Nat } ./Nat/sum
         { ./Nat        } even
         { ./Bool       } ./Bool/not
         { ./Bool       }
     ]

     in  f [nil ./Nat , 1, 2, 3, 4]

Annah's Prelude only provides support for one ./Category instance for functions named .(->)Category, so in practice the ./Category support is not that handy out-of-the box and is mainly provided for completeness.

Conclusion

Those are all the features that Annah supports! Annah is a very tiny language and library that illustrates and implements basic idioms for translating functional programming concepts into pure lambda calculus.

Hopefully you can use Annah to learn how to encode a subset of Haskell in a completely total programming language. If you translate any Haskell functions to Annah you can contribute them upstream to the Annah prelude by submitting a pull request against the Annah repository:

https://github.com/Gabriel439/Haskell-Annah-Library/tree/master/Prelude