How to create the `enumFromTo` function on Morte?

coinduction, data-structures, functional-programming, haskell, induction

Solution

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.

Problem

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?

Original source