如何在 Morte 上创建 `enumFromTo` 函数？

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

我想在 Morte 上重写 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 代码的能力，所以我将省略它。然而，现在我正在研究一种中级语言，它可以像我们所说的那样编译成 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
        )

如果仔细观察，它会生成一个包含两个元素的列表，每个元素都是一个教堂编码的数字三。

如何在 Morte 上创建 `enumFromTo` 函数？

How to create the `enumFromTo` function on Morte?

haskell

functional-programming

data-structures

induction

coinduction