<p>The clever definition of <code>zipWith</code> (which comes from <a href="https://arxiv.org/pdf/1309.5135.pdf" rel="nofollow noreferrer">Launchbury et al.</a>, I believe) doesn't work in Morte, because typing it without negative recursive types (which Morte doesn't have, and which imply <code>fix</code>, as seen in my <a href="https://stackoverflow.com/questions/29885983/infinite-type-error-when-defining-zip-with-foldr-only-can-it-be-fixed/29930561#29930561">mentioned</a> previous answer) requires induction at least on natural numbers. <a href="https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/Hyperfunction.agda" rel="nofollow noreferrer">Here's</a> a simple Agda version of Launchbury's definition without Church encoding; to reproduce this in Morte we'd need functions whose return type depends on natural numbers (the lengths of input lists).</p>

<p>Without induction, the best we can do is an <code>O(N^2)</code> definition that uses <code>O(N)</code> pattern matching on lists, i. e. a <code>List A -&gt; Maybe (A, List A)</code> function. It's <code>O(N)</code> because we can only get the tail of the list by rebuilding it from the end.</p>

<p>In Morte-compliant Agda (to get Morte, we need to desugar <code>let</code> style definitions to applications and function definitions to annotated lambdas):</p>

<pre><code>Pair : Set → Set → Set
Pair A B = ∀ P → (A → B → P) → P

pair : ∀ A B → A → B → Pair A B
pair A B a b P p = p a b

List : Set → Set
List = λ A → ∀ L → (A → L → L) → L → L

Maybe : Set → Set
Maybe A = ∀ M → (A → M) → M → M

just : ∀ A → A → Maybe A
just A a M j n = j a

nothing : ∀ A → Maybe A
nothing A M j n = n

nil : ∀ A → List A
nil A L c n = n

cons : ∀ A → A → List A → List A
cons A a as L c n = c a (as L c n)

match : ∀ A → List A → Maybe (Pair A (List A))
match A as =
  as
    (Maybe (Pair A (List A)))
    (λ a m M j n →
       m M
         (λ p → p M (λ a' as → j (pair A (List A) a (cons A a' as))))
         (j (pair A (List A) a (nil A))))
    (nothing (Pair A (List A)))

zipWith : ∀ A B C → (A → B → C) → List A → List B → List C
zipWith A B C f as = 
  as
    (List B → List C)
    (λ a hyp bs → match B bs (List C)
      (λ p → p (List C) (λ b bs' → cons C (f a b) (hyp bs')))
      (nil C))
    (λ _ → nil C)
</code></pre>
How to type zipWith in Morte?
<p>This is an almost valid <code>zipWith</code> definition in Morte:</p>

<pre><code>zipWith
  =  λ (u : *)
  -&gt; λ (f : (u -&gt; u -&gt; u))
  -&gt; λ (a : (#List u))
  -&gt; λ (b : (#List u))
  -&gt; λ (List : *)
  -&gt; λ (cons : (u -&gt; List -&gt; List))
  -&gt; λ (nil : List)
  -&gt; ((λ (A:*) -&gt; λ (B:*) -&gt;
  (a (B -&gt; List)
    (λ (h:u) -&gt; λ (t : (B -&gt; List) -&gt; λ k : B -&gt; (k h t)))
    (λ (k:B) -&gt; nil)
    (b (u -&gt; A -&gt; List)
      (λ (h:u) -&gt; λ (t:(u -&gt; A -&gt; List)) -&gt; λ (H:u) -&gt; λ (k:A) -&gt; (cons (f h H) (k t)))
      (λ (H:u) -&gt; λ (k:A) -&gt; nil)))
  ) (fix A . ((u -&gt; A -&gt; List) -&gt; List))
    (fix B . (u -&gt; (B -&gt; List) -&gt; List)))
</code></pre>

<p>It isn't actually typeable due to the use of <code>fix</code>, which Morte lacks. <a href="https://stackoverflow.com/a/29930561/477476">András posted this clever Agda solution without <code>fix</code></a> last year. It isn't obvious to me how it translates to Morte, though, because it also lacks inductive types. How to approach this problem? </p>

<p>Edit: seems like my zipWith was incorrect even with <code>fix</code>. <a href="http://lpaste.net/341877" rel="nofollow noreferrer">This one</a> seems to check, though.</p>