How to create the `enumFromTo` function on Morte?

Question

Morte was designed to serve as an intermediate language for super-optimizing functional programs. In order to preserve strong normalization it has no direct recursion, so, inductive types such as lists are represented as folds, and conductive types such as infinite lists are represented as streams:

finiteList :: List Int
finiteList = \cons nil -> cons 0 (cons 1 (cons 2 nil))

infiniteList :: Stream Int
infiniteList = Stream 0 (\n -> (n, n + 1))

I want to rewrite Haskell's enumFromTo on Morte, so that:

enumFromTo 0 2

normalizes to:

\cons nil → cons 0 (cons 1 (cons 2 nil))

Is that possible?

Answer 1

In Morte, a natural number is encoded as a value of type:

forall (Nat : *) -> (Nat -> Nat) -> Nat -> Nat

So, for example, 0, 1, and 2 in Morte would be represented as:

(   \(Nat : *)
->  \(zero : Nat)
->  \(one  : Nat)
->  \(two  : Nat)
->  \(foldNat : Nat -> forall (x : *) -> (x -> x) -> x -> x)
->  ...
)

-- Nat
(forall (Nat : *) -> (Nat -> Nat) -> Nat -> Nat)

-- zero
(\(Nat : *) -> \(Succ : Nat -> Nat) -> \(Zero : Nat) -> Zero)

-- one
(\(Nat : *) -> \(Succ : Nat -> Nat) -> \(Zero : Nat) -> Succ Zero)

-- two
(\(Nat : *) -> \(Succ : Nat -> Nat) -> \(Zero : Nat) -> Succ (Succ Zero))

-- foldNat
(\(n : forall (Nat : *) -> (Nat -> Nat) -> Nat -> Nat) -> n)

With that encoding, then you can start writing simple things like replicate:

-- Assuming you also defined:
-- List : * -> *
-- Cons : forall (a : *) -> a -> List a -> List a
-- Nil  : forall (a : *) -> List a
-- foldList : forall (a : *)
--          -> List a -> forall (x : *) -> (a -> x -> x) -> x -> x

-- replicate : forall (a : *) -> Nat -> a -> List a
replicate =
        \(a : *)
    ->  \(n : Nat)
    ->  \(va : a)
    ->  foldNat n (List a) (\(as : List a) -> Cons a va as) (Nil a)

Doing enumFromTo would be a little more complex but it would still be possible. You will still use foldNat, but your accumulator would be more complex than List Nat. It would be more like (Nat, List Nat) and then you'd extract the second element of the tuple at the end of the fold. That would, of course, require encoding tuples in Morte, too.

That exceeds my ability to hand-write Morte code on the fly, so I will omit that. However, right now I'm working on a medium-level language that compiles to Morte as we speak and it's only a few lines of code away from supporting recursive types (and non-recursive types are ready). You can check it out here:

https://github.com/Gabriel439/Haskell-Annah-Library

Once that code is ready you'd then just be able to write:

type Nat : *
data Succ (pred : Nat) : Nat
data Zero              : Nat
in

type List (a : *) : *
data Cons (head : a) (tail : List a) : List a
data Nil                             : List a
in

let One : Nat = Succ Zero
let Two : Nat = Succ (Succ Zero)
let Three : Nat = Succ (Succ (Succ Zero))
let replicate (a : *) (n : Nat) (va : a) : List a =
        foldNat n (List a) (\(as : List a) -> Cons a va as) (Nil a)
in

replicate Nat Two Three

It's medium-level in the sense that you'd still have to deal with explicitly writing out a fold and figuring out the correct intermediate state to use as the accumulator, but one of the things it simplifies are let and data type declarations. It will also eventually support built-in decimal syntax for Nat, but I haven't started that yet.

Edit: Now annah supports recursive types, and the above annah code normalizes to:

$ annah < replicate.an
∀(List : * → *) → ((∀(Nat : *) → (Nat → Nat) → Nat → Nat) → List (∀(Nat : *) → (Nat → Nat) → Nat → Nat) → List (∀(Nat : *) → (Nat → Nat) → Nat → Nat)) → List (∀(Nat : *) → (Nat → Nat) → Nat → Nat) → List (∀(Nat : *) → (Nat → Nat) → Nat → Nat)

λ(List : * → *) → λ(Cons : (∀(Nat : *) → (Nat → Nat) → Nat → Nat) → List (∀(Nat : *) → (Nat → Nat) → Nat → Nat) → List (∀(Nat : *) → (Nat → Nat) → Nat → Nat)) → λ(Nil : List (∀(Nat : *) → (Nat → Nat) → Nat → Nat)) → Cons (λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))) (Cons (λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))) Nil)

... which I will format to make it slightly more readable:

    λ(List : * → *)
→   λ(  Cons
    :   (∀(Nat : *) → (Nat → Nat) → Nat → Nat)
    →   List (∀(Nat : *) → (Nat → Nat) → Nat → Nat)
    →   List (∀(Nat : *) → (Nat → Nat) → Nat → Nat)
    )
→   λ(Nil : List (∀(Nat : *) → (Nat → Nat) → Nat → Nat))
→   Cons
        (   λ(Nat : *)
        →   λ(Succ : Nat → Nat)
        →   λ(Zero : Nat)
        →   Succ (Succ (Succ Zero))
        )
        (Cons
            (   λ(Nat : *)
            →   λ(Succ : Nat → Nat)
            →   λ(Zero : Nat)
            →   Succ (Succ (Succ Zero))
            )
            Nil
        )

If you look closely, it produced a list with two elements, each of which is a church-encoded number three.