Функция Zip в системе F

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

Хорошо, мне удалось написать решение для этого. Прежде всего, давайте определимся с помощником 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 просто вернет пустой список в пустой список (аналогично функции-предшественнику на церковных цифрах)

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)