1

让我们定义列表类型

list = forall 'a, 'x. ('a -> 'x -> 'x) -> 'x -> 'x

例如在哪里

nil = Λ'a . Λ'x . λ(c : 'a -> 'x -> 'x) . λ(e : 'x) . e
cons = Λ'a . Λ'x . λ(head : 'a) . λ(tail : list 'a 'x) . λ(c : 'a -> 'x -> 'x) . λ(e : 'x) . c head (tail c e)

我正在尝试定义zip类型的函数

zip : forall 'a, 'b, 'c, 'x. ('a -> 'b -> 'c) -> list 'a 'x -> list 'b 'x -> list 'c 'x

直观地做到了

zip (+) [1,2,3] [4,5,6] = [5,7,9]
zip (λa . λb . a) [1,2] [2,3,4] = [1,2]
zip (λa . λb . a) [2,3,4] [1,2] = [2,3]

请注意，它会截断较长的列表以适应较短的列表。

我在这里遇到的主要问题是我不能一次“迭代”两个列表。如何在系统F中实现这样的功能？甚至可能吗？

4

1 回答 1

0

好的，我设法为它编写了解决方案。首先让我们定义辅助option类型：

option = forall 'a, 'x. ('a -> 'x) -> 'x -> 'x

其中有两个构造函数：

none = Λ'a . Λ'x . λ (onsome : 'a -> 'x) . λ (onnone : 'x) . onnone
some = Λ'a . Λ'x . λ (elem : 'a) . λ (onsome : 'a -> 'x) . λ (onnone : 'x) . onsome elem

下一步是将提取列表head的函数。将返回处理空列表情况，但只会在空列表上返回空列表（与 Church 数字上的前置函数类似）tailheadoption 'elemtypetail

head = Λ 'a . λ (l : list 'a) . l (λ (elem : 'a) . λ (p : option 'a) . some elem) none
tail = Λ 'a . λ (l : list 'a) .
    pair_first 
       ( l (λ (elem : 'a) . λ (p : pair (list 'a) (list 'a)) .
               make_pair (list 'a) (list 'a) 
                  (pair_second (list 'a) (list 'a) p) 
                  (cons 'a elem (pair_second (list 'a) (list 'a) p))) 
           (make_pair (list 'a) (list 'a) (nil 'a) (nil 'a)))

的想法head是，我们从空列表开始聚合我们的列表none，对于从左侧开始的每个新元素，我们将此元素设置为我们的结果，some以保留输入。 tail另一方面，不需要option很好地定义，因为在空列表的情况下，我们可能只返回一个空列表。它看起来很丑陋，但使用的技术与自然数的前身相同。我假设pair接口是已知的。

接下来，让我们定义listmatch将在给定列表上进行模式匹配的函数

listmatch = Λ 'a . Λ 'x . λ (l : list 'a) . λ (oncons : 'a -> list 'a -> 'x) . λ (onnil : 'x) .
    (head 'a l)
      (λ (hd : 'a) . oncons hd (tail 'a l))
      onnil

这个函数帮助我们区分空列表和非空列表，并在销毁后执行一些操作。

几乎最后，我们希望有foldl2一个给定 function f、空 caseem和两个列表的函数，[a,b,c]并[x,y]返回如下内容：（f(f(em a x) b y)将列表缩小到较短的一个，切断尾部）。

它可以定义为

foldl2 =
  Λ 'a . Λ 'b . Λ 'c .
  λ (f : 'c -> 'a -> 'b -> 'c) . λ (em : 'c) . λ (la : list 'a) . λ (lb : list 'b) .
  pair_first 'c (list 'b)
    ((reverse 'a la)
      ( λ (el : 'a) . λ (p : pair 'c (list 'b)) . 
        listmatch 'a (pair 'c (list 'b)) (pair_second 'c (list 'b) p)
          (λ (hd : 'a) . λ (tl : list 'a) .
            make_pair 'c (list 'b) 
              (f (pair_first 'c (list 'b) p) el hd)
              tl)
          (make_pair 'c (list 'b) (pair_first 'c (list 'b) p) (nil 'a))
      )
      (make_pair 'c (list 'b) em lb))

在此之后，zip就在我们手中：

zip = 
  Λ 'a . Λ 'b . Λ 'c .
  λ (f : 'a -> 'b -> 'c) . λ (la : list 'a) . λ (lb : list 'b) .
  reverse 'c
    (foldl2 'a 'b 'c
      (λ (lt : 'c) . λ (a : 'a) . λ (b : 'b) . cons 'c (f a b) lt)
      (nil 'c) la lb)
于 2019-05-28T13:22:06.877 回答