Как создать функцию `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)) 

Я хочу переписать в Haskell 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, когда мы говорим, и это всего лишь несколько строк кода от поддержки рекурсивных типов (и нерекурсивные типы готовы). Вы можете проверить его здесь:

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, но я еще не начал это делать.

Edit: Теперь 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 
     ) 

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