これは、このフォローアップの質問のフォローアップです。Zipp は、折り畳みを使用した zip の非再帰的、非パターン マッチング実装です。型なしラムダ計算では、次のようになります。
-- foldr for church encoded lists (that is, folds)
foldr cons nil list = list cons nil
zipp_left = foldr (λ x xs cont -> (cont x xs)) (const [])
zipp_right = foldr (λ y ys x cont -> (cons (pair x y) (cont ys))) (const (const []))
zipp = λ a b -> (zipp_left a) (zipp_right b)
Haskell では、@András_Kovács によって証明されているように、この用語を入力することは不可能ですが、Agda は少し複雑ではありますが、それを行うことができます。このプログラムを Idris でエレガントに定義することは可能ですか?