リストタイプを定義しましょう
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]
短いリストに合わせて長いリストを切り捨てることに注意してください。
ここで遭遇する主な問題は、一度に 2 つのリストを「反復」できないことです。システム F でそのような機能をどのように実装できますか? それは可能ですか？