System F 中的 Zip 功能

Question

让我们定义列表类型

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中实现这样的功能？有没有可能？

Answer 1

好的，我设法为它编写了解决方案。首先让我们定义 helper 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 和tail 的函数。 head 将返回 option 'elemtype 以处理空列表情况，但 tail 将仅在空列表上返回空列表（与 Church 数字上的前置函数类似）

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 函数，它给定函数f，空壳em 和两个列表[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)