Quick annah walkthrough

gistfile1.txt

-- Example Annah programs and their reductions
-- I'll start with simple non-recursive data types so that you can get a feel for the syntax and then work up to recursive data
-- types followed by mutually recursive types

-- Example #1: Bool, the type
$ annah
type Bool
data True
data False
in Bool
<Ctrl-D>
*

∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

-- Explanation of Example #1:
-- All Annah source code is just one big expression (like Morte).  There is not concept of multiple top-level expression or
-- modules.  These are actually unnecessary, for reasons I'll go into below.
--
-- When you compile an Annah program it does these steps:
--
-- * Translate the Annah expression to a Morte expression
-- * Normalize the Morte expression (i.e. beta-/eta- reduction)
-- * Translate the Morte expression back to Annah (which is a super-set of Morte)
--
-- Then the compiler will print out the type of the normalized expression and the value of the normalized expression.
--
-- In this case you read the above program as a data type definition scoping over another expression:
--
-- type Bool  -- Define a `Bool` type
-- data True  -- with two constructors
-- data False
-- in Bool    -- The data type is only in scope for everything after the `in`.  You can think of this as analogous to a `let`
--            -- expression except replace the `let` with a data type definition that scopes over the body of the `in`
--            -- expression
--
-- So what `annah` is returning is the value and type of the final `Bool` in the body of the `in`.  The type is the first line
-- of the output:
--
-- *
--
-- The value is the second line of the output:
-- 
-- ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
--
-- Notice that when introducing Pi- or Lambda-bound variables, you will see me reuse the names of data or type constructors.
-- This is not a coincidence, but it can be confusing at first, since the variables are not the same as the values they are
-- supposed to represent.
--
-- Now let's ask Annah to encode the `False` constructor.  We reuse the same data type definition, but this time change the
-- body of the `in`:
$ annah
type Bool
data True
data False
in True
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True

-- Notice how the inferred type of this Boehm-Berarducci-encoded `True` matches the value of the Boehm-Berarducci `Bool`.  The
-- nice property that Boehm-Berarducci encoding has is "representability": you can replace the System-F encodings with the
-- terms of types they are supposed to represent and everything remains consistent.
--
-- The value of the Church-encoded Bool is the typical lamba encoding of boolean values, with types explicitly elaborated.
-- Notice how we are again using type and data constructor names for the lambda-bound variables.
--
-- Also note how the right-hand side of types or terms greatly resembles the values they encode.  This is not a coincidence.
-- THis is basically how Boehm-Berarducci encoding works: for every data or type constructor you just "assume" it by binding it
-- using "Lambda" or "Pi" and then build up your type.
--
-- Let's move on to recursive data types:
$ annah
type Nat
data Succ (n : Nat)
data Zero
in Nat
*

∀(Nat : *) → ∀(Succ : ∀(n : Nat) → Nat) → ∀(Zero : Nat) → Nat

-- Again, we will just "assume" that we have the `Nat` type and its constructors and use them to build our values of type
-- `Nat`
type Nat
data Succ (n : Nat)
data Zero
in Zero
<Ctrl-D>
∀(Nat : *) → ∀(Succ : ∀(n : Nat) → Nat) → ∀(Zero : Nat) → Nat

λ(Nat : *) → λ(Succ : ∀(n : Nat) → Nat) → λ(Zero : Nat) → Zero

-- Zero is straight-forward, but `Succ` is slightly more tricky:

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

λ(n : ∀(Nat : *) → ∀(Succ : ∀(n : Nat) → Nat) → ∀(Zero : Nat) → Nat) → λ(Nat : *) → λ(Succ : ∀(n : Nat) → Nat) → λ(Zero : Nat) → Succ (n Nat Succ Zero)

-- For any recursive invocation we forward the constructors.  If you understand Church encoding you probably already
-- understand this trick
--
-- Note that the representation of `Succ` is non-recursive.  This is what I mean when I say that Boehm-Berarducci encoding
-- lets you encode recursive data types in a non-recursive System-F.
--
-- Now, here's the part that is really interesting.  Annah lets you import expressions by simplify referencing a file
-- containing an expression.  To do this you just do `#file` to import the contents of `file`
--
-- So what I can do is save the `Nat` type, and the `Zero` and `Succ` constructors to three files of the same name:
--
$ annah > Nat
type Nat
data Succ (n : Nat)
data Zero
in Nat
$ annah > Zero
type Nat
data Succ (n : Nat)
data Zero
in Zero
$ annah > Succ
type Nat
data Succ (n : Nat)
data Zero
in Succ

-- and once I do that, I can reference those files like this:

$ annah
#Succ (#Succ (#Succ #Zero))
<Ctrl-D>
∀(Nat : *) → ∀(Succ : ∀(n : Nat) → Nat) → ∀(Zero : Nat) → Nat

λ(Nat : *) → λ(Succ : ∀(n : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))

-- The right-hand side is a lambda-encoded three.  The inferred type is "Nat"
--
-- However, annah is actually extremely smart.  Not only can Annah encode things in Morte, but Annah can actually
-- intelligently resugar things as imported expressions.
--
-- For example, suppose that we save `Bool`, `True`, and `False` to three separate files:
--
$ annah > Bool
type Bool
data True
data False
in Bool
$ annah > True
type Bool
data True
data False
in True
$ annah > False
type Bool
data True
data False
in False

-- We will also save `and` to its own file:
$ annah > and
\(b1 : #Bool) -> \(b2 : #Bool) -> b1 #Bool b2 #False

-- Now we can ask annah boolean logic:
$ annah
#and #True #False
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False

-- But wait!  There's more!  We can ask Annah: "Does this look like any expression we have defined so far?" by just supplying
-- the `-d` flag.  Then you get:
$ annah -d
#and #True #False
<Ctrl-D>
#Bool

#False

-- Annah notices that the expressions can be replaced with imports and resugars the type to an import of the `Bool` file and
-- the value to an import of the `False` file
--
-- It's like we're not even using lambda calculus any more, even though it's used as an intermediate.  We can think
-- completely in terms of the higher-level types and constructors we defined.
--
-- Note that this trick of resugaring imports does not work for recursive types.  Annah instead hard-codes support for
-- specific recursive types (i.e. lists, free monads, and free categories, strings, and binary numbers)
--
-- I mentioned that you can do mutually recursive types, too, so HERE WE GO:
$ annah
type Even
data Zero
data SuccE (n : Odd)

type Odd
data SuccO (n : Even)

in Even
<Ctrl-D>
*

∀(Even : *) → ∀(Odd : *) → ∀(Zero : Even) → ∀(SuccE : ∀(n : Odd) → Even) → ∀(SuccO : ∀(n : Even) → Odd) → Even

-- The trick for mutually recursive types is no different than recursive types.  We just "assume" one value for every type or
-- data constructor and then build the tree
--
-- If I were to repeat this exercise for all the type and data constructors in the above `Odd` and `Even` example and save
-- them to their respective files, I could then do:
--
$ annah
#SuccE (#SuccO #Zero)
<Ctrl-D>
∀(Even : *) → ∀(Odd : *) → ∀(Zero : Even) → ∀(SuccE : ∀(n : Odd) → Even) → ∀(SuccO : ∀(n : Even) → Odd) → Even

λ(Even : *) → λ(Odd : *) → λ(Zero : Even) → λ(SuccE : ∀(n : Odd) → Even) → λ(SuccO : ∀(n : Even) → Odd) → SuccE (SuccO Zero)

-- and it does exactly what you expect.
--
-- Anyway, all of this is extremely in flux (some of Annah's functionality will be migrated into Morte and instead of using
-- files Annah will eventually use network endpoints that you can download expressions from), but that gives you a high-level
-- view of what is going on.