1

Let's define list type

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

where for instance

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)

I am trying to define function zip of type

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

That intuitively does

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]

Note that it truncates the longer list to fit the shorter.

The main problem I encounter here is that I cannot "iterate" over two lists at once. How can implement such a function in system F? Is it even possible?

radrow
  • 6,419
  • 4
  • 26
  • 53

1 Answers1

0

Okay, I managed to write solution for it. First of all let's define helper option type:

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

Which has two constructors:

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

Next step are functions that will extract head and tail of the list. head will return option 'elemtype to handle empty list case, but tail will just return empty list on empty list (in similar manner to predecessor function on Church numerals)

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)))

The idea of head is that we start aggregating our list starting with none on empty list and for each new element from the left we set this element as our result wrapped by some to preserve typing. tail on the other hand does not need option to be well defined, because in case of empty list we may just return an empty list. It looks very ugly, but uses same technique as predecessor of natural numbers. I assume pair interface is known.

Next, let's define listmatch function that will pattern match on given list

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

This function helps us distinguish empty list and non-empty list and perform some actions after its destruction.

Almost finally, we would like to have foldl2 function that given function f, empty case em and two lists [a,b,c] and [x,y] returns something like this: f(f(em a x) b y) (shrinks lists to the shorter one cutting off the tail).

It can be defined as

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))

After this the zip is just in our hands:

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)
radrow
  • 6,419
  • 4
  • 26
  • 53
  • how do you run this program? – codeshot Sep 22 '19 at 23:36
  • This is not an actual programming language, but rather a notation of pure lambda calculus with F system. It can be however rewritten to some language that supports type applications and higher rank types such as Agda, Idris, Coq or maybe Haskell. Also, you may perform manual beta reduction if you want to stick to the roots – radrow Sep 23 '19 at 08:03
  • Technically, System F is, and can be used as, an actual programming language. It's just not very ergonomic. I have a written an intrepeter in which you can directly program using System F – crunch Dec 06 '19 at 14:55
  • @crunch can you post a link? – radrow Dec 06 '19 at 15:02
  • @radrow https://github.com/lazear/types-and-programming-languages - It is close to being a port of Benjamin Pierce's typecheckers from the book Types and Programming Languages – crunch Dec 06 '19 at 20:49