Функция Zip в системе F - PullRequest
Новая
       30

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

0 голосов
/ 26 мая 2019

Давайте определим тип списка 

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? Это вообще возможно?

1 Ответ

0 голосов
/ 28 мая 2019

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