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

Question

Morte被设计作为 super 优化功能程序的中间语言。为了保持强标准化，它没有直接递归，因此，归纳类型(例如列表)表示为折叠，传导类型(例如无限列表)表示为流:

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

例如，Morte 中的 0、1 和 2 将表示为:

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

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