Как создать функцию enumFromTo на Morte?

Question

Morte был разработан, чтобы служить промежуточным языком для супероптимизирующих функциональных программ. Чтобы сохранить строгую нормализацию, она не имеет прямой рекурсии, поэтому индуктивные типы, такие как списки, представлены в виде складок, а проводящие типы, такие как бесконечные списки, представлены в виде потоков:

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

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

Я хочу переписать Хаскелла enumFromTo на морте, так что:

enumFromTo 0 2

нормализуется до:

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

Это возможно?

Answer 1

В Morte натуральное число кодируется как значение типа:

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

Так, например, 0, 1, а также 2 в Morte будет представлен как:

(   \(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)

С этой кодировкой вы можете начать писать простые вещи, такие как 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)

дела enumFromTo будет немного сложнее, но все равно будет возможно. Вы все еще будете использовать foldNat, но ваш аккумулятор будет сложнее, чем List Nat, Было бы больше похоже (Nat, List Nat) и затем вы извлечете второй элемент кортежа в конце сгиба. Это, конечно, потребовало бы также кодирования кортежей в Morte.

Это превосходит мою способность писать код Morte на лету, поэтому я опущу это. Тем не менее, сейчас я работаю над языком среднего уровня, который компилируется в Morte, пока мы говорим, и это всего лишь несколько строк кода от поддержки рекурсивных типов (и нерекурсивные типы готовы). Вы можете проверить это здесь:

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

Как только этот код будет готов, вы сможете написать:

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

Это средний уровень в том смысле, что вам все еще придется иметь дело с явным выписыванием сгиба и определением правильного промежуточного состояния для использования в качестве аккумулятора, но одна из вещей, которые он упрощает, это let и объявления типов данных. Он также в конечном итоге будет поддерживать встроенный десятичный синтаксис для Nat, но я еще не начал это.

Изменить: сейчас annah поддерживает рекурсивные типы и выше annah код нормализуется до:

$ 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)

... который я отформатирую, чтобы сделать его немного более читабельным:

    λ(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
        )

Если вы посмотрите внимательно, он создал список с двумя элементами, каждый из которых представляет собой закодированное в церковь число три.