Using Vect.cons with List.foldr

Stream: new members

[mars0i]

I tried to do this to build a Vect from a List (based on FPIL 8.1):

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

#check List.foldr Vect.cons Vect.nil ["Møllehøj", "Yding Skovhøj", "Ejer Bavnehøj"]

The error is:

▶ 69:19-69:28: error:
application type mismatch
  List.foldr Vect.cons
argument
  Vect.cons
has type
  ?m.3756 → Vect ?m.3756 ?m.3757 → Vect ?m.3756 (?m.3757 + 1) : Type ?u.3755
but is expected to have type
  String → Vect ?m.3804 0 → Vect ?m.3804 0 : Type (max ?u.3803 0)

The error on Vect.cons made me think that I needed to specify its type. So I tried this:

#check List.foldr (Vect.cons : String -> Vect String n -> Vect String (n + 1))
                   Vect.nil
                   ["Møllehøj", "Yding Skovhøj", "Ejer Bavnehøj"]

Then the errors concern the two instances of n:

unknown identifier 'n'

I tried replacing the ns with underscores to see whether Lean would figure out what to do, but that seems to produce an error that's worse.

Now I think that it's not possible to pass Vect.cons to List.foldr because Vect.cons doesn't have a single function type, which is what foldr wants. String -> Vect String 1 -> Vect String 2 is in some sense a different function type from String -> Vect String 2 -> Vect String 3.

Is that more or less correct? (Nothing specific depends on the answer; I was just exploring while doing the section 8.1 exercises.)

I imagine there is something fancy one could do to use Vect.cons with List.foldr, but it wouldn't be worth the trouble--not for me, now.

[Eric Wieser]

You could make foldr work by returning a sigma type containing n

[mars0i]

Thanks @Eric Wieser. OK--I thought something like that might be what was needed.