3

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在 Morte 上重写 Haskell，这样：

enumFromTo 0 2

归一化为：

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

那可能吗？

4

1 回答 1

5

在 Morte 中，自然数被编码为类型的值：

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

因此，例如，0Morte中的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
        )

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

于 2015-02-21T00:21:35.500 回答