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]

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

我在这里遇到的主要问题是我不能同时 "iterate" 处理两个列表。如何在系统F中实现这样的功能？有可能吗？

Answer 1

好的，我设法为它编写了解决方案。首先让我们定义助手 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 将 return option 'elemtype 处理空列表的情况，但 tail 将只是 return 空列表上的空列表（类似于教堂数字上的前置函数)

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 开始聚合我们的列表，对于从左侧开始的每个新元素，我们将此元素设置为由 [=24 包装的结果=] 以保留输入。另一方面，tail 不需要 option 来明确定义，因为在空列表的情况下我们可能只是 return 一个空列表。它看起来非常丑陋，但使用与自然数的前身相同的技术。我假设 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

这个函数可以帮助我们区分空列表和non-empty列表，并在其销毁后执行一些操作。

几乎最后，我们想要 foldl2 函数给定函数 f、空 case em 和两个列表 [a,b,c] 和 [x,y] returns 是这样的：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)

System F 中的 Zip 功能

Zip function in System F

type-theory

lambda-calculus

system-f