如何在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))

我想enumFromTo在Morte 上重写Haskell ,所以:

enumFromTo 0 2

归一化为:

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

那可能吗？

Answer 1

在Morte中,自然数被编码为类型的值:

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

因此,例如,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
        )

如果你仔细观察,它会产生一个包含两个元素的列表,每个元素都是一个教会编码的三号.