1
$\begingroup$

I'm working my way through Functional Programming in Lean and there's an exercise to create a zip function for combining two Lists into a single list of Pairs.

My initial implementation fails to type-check because Lean doesn't know what Type to give []. I don't understand why, as it's specified in the function signature. Here was my initial implementation:

def zip : (as: List α) → (bs: List β) → List (α × β)
    | a::arest, b::brest => (a, b) :: (zip arest brest)
    | _ => []

And the error it generated:

type mismatch
  []
has type
  List ?m.16818 : Type ?u.16817
but is expected to have type
  List β → List (α × β) : Type (max ?u.16734 ?u.16738)

I figured that the the right way to fix this would be to use the constructor List.nil with an explicit parameter for the type. The source for List starts with inductive List (α : Type u), so I figured I should set the $\alpha$ parameter like so:

def zip : (as: List α) → (bs: List β) → List (α × β)
    | a::arest, b::brest => (a, b) :: (zip arest brest)
    | _ => List.nil (α := α×β)

However, this fails with another error:

type mismatch
  []
has type
  List (α × β) : Type (max ?u.16738 ?u.16734)
but is expected to have type
  List β → List (α × β) : Type (max ?u.16734 ?u.16738)

This is confusing to me because I expect it to return a List (α × β), and when I check the typing of the first branch Lean tells me that it has this type. So why is Lean expecting a List β → List (α × β) for the second branch? And is there any way to get Lean to figure out the correct type for the more idiomatic [] automatically?

$\endgroup$

1 Answer 1

4
$\begingroup$

You are missing a pattern for the second argument, ie you should have | _, _ => … instead of | _ => … in your second branch. The error that Lean reports stems from the fact that since it is only given a pattern for the argument of type List α, it is still waiting for an argument of type List β in that branch, and so [] does not have the right type.

I guess this is a somewhat non-intuitive part of simultaneous pattern-matching, that you still have to provide a pattern for each matched term, even if this pattern is _. In other words, _ is interpreted as a pattern for the first matched term only, not for all of them.

$\endgroup$
2
  • $\begingroup$ Oh interesting, I still had this idea of simultaneous matches being Pairs in my mind. A single _ would work in Python because no unpacking would be triggered and the entire tuple would be assigned to it. $\endgroup$
    – Nate Glenn
    Commented Sep 1, 2023 at 0:00
  • $\begingroup$ It's also interesting, and didn't even occur to me previously, that each branch of the match can use a different number of simultaneous matches (1 or more; is 0 possible as a base case?). $\endgroup$
    – Nate Glenn
    Commented Sep 1, 2023 at 0:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.