Dependent lists?

Stream: Is there code for X?

[Peter LeFanu Lumsdaine]

Does Mathlib have dependent lists? That is, a type family something like

inductive DList {α} (β : α → Type) : List α → Type where
  | nil : DList β []
  | cons {a} (b : β a) {as} (bs : DList β as) : DList β (a::as)

or something reasonably equivalent, e.g. a list-like notation + interface for dependent functions on Fin n that computes roughly like lists?

[Eric Wieser]

I think this is the same as a list of dependent pairs?

[Peter LeFanu Lumsdaine]

Yes, a pair of “a list and a dependent list over it” is equivalent to a list of dependent pairs — and indeed my development currently uses exactly that. But the use-case is where the base list has been given earlier, and a later function is naturally thought of as taking a dependent list as its argument. So using the “list of pairs” approach, I end up giving arguments of the form [⟨_,t1⟩, ⟨_,t2⟩,⟨_,t3⟩], and it would feel cleaner (both notationally and conceptually) if I could give it just as the dependent list [[t1,t2,t3]].

[Mario Carneiro]

a dependent list can be defined as just folding Prod over the list of types

[Mario Carneiro]

at least, that's why I've never seen a use for it being a separate type

[Mario Carneiro]

lean uses this representation of tuples in many places internally

[Peter LeFanu Lumsdaine]

@Mario Carneiro Ah, that sounds good! Can you point me to somewhere that uses this, just to see the kinds of idioms people use with it?

[Mario Carneiro]

well in lean core it's mostly just metaprograms that use docs#PProd or docs#MProd recursively

[Mario Carneiro]

user code would probably just use docs#Prod instead

[Mario Carneiro]

sometimes it's a dependent pair, for example when tupling things up for use in well founded recursion

[Mario Carneiro]

but because it's meta code there is never any abstraction which tries to cover all "product shapes" that would be analogous to your DList. The generated code just has something like (A × B × C × Unit) in it somewhere

[Mario Carneiro]

this is actually more general than you can get with DList as well, because DList has the flaw that even though the types can be different they all have to live in the same universe, because it is parameterized over a List (Type u) or A -> Type u

[Mario Carneiro]

Here's an example where compiler generated code makes use of a tuple type:

def foo : Id Nat := do
  let mut a := 1
  let mut b := 2
  let mut c := 3
  for _ in [0] do
    a := a + 1
    b := 0
    c := a
  return b
#print foo

def foo : Id Nat :=
let a := 1;
let b := 2;
let c := 3;
do
let r ←
  forIn [0] ⟨a, b, c⟩ fun x r ↦ -- note: ⟨a, b, c⟩ : MProd Nat (MProd Nat Nat)
      let a := r.fst;
      let x := r.snd;
      let b := x.fst;
      let c := x.snd;
      let a := a + 1;
      let b := 0;
      let c := a;
      do
      pure PUnit.unit
      pure (ForInStep.yield ⟨a, b, c⟩)
match r with
  | ⟨a, b, c⟩ => pure b

[Peter LeFanu Lumsdaine]

hmm… trying this approach, I’m not quite getting it to work for my use-case, which is to write a function like myFun : {as : List α} (bs : DList β as) -> C as, where C is defined by a fold over as;

[Peter LeFanu Lumsdaine]

with an actual DList, once you give the dependent list argument myFun [[b1,b2,b3]], this forces that the list argument is of the shape [ ?a1 , ?a2 , ?a3 ], and unification then can fill in the entries by looking at the output type, which is something like FC a1 (FC a2 (FC a3 D)))

[Peter LeFanu Lumsdaine]

but if DList is defined as a fold over products, then myFun (b1,b2,b3) doesn’t typecheck, because the shape of the plain list argument can’t be inferred by unification; myFun [_,_,_] (b1,b2,b3) works (with the list argument explicit) but explicitly giving that is what I’m trying to avoid

[Mario Carneiro]

I think most of the time we want to do this kind of thing in mathlib, we use a typeclass with an out-param; this can avoid getting additional gunk in the types that needs reduction after the fact, and allows you to control what gets inferred from what

[Mario Carneiro]

src#Function.HasUncurry might be an example to follow

[Peter LeFanu Lumsdaine]

thanks, I’ll take a look and see if I can imitate that…

[Peter LeFanu Lumsdaine]

I haven’t properly grokked how out-params work, this will be good for me to have to work through :-)

[Peter LeFanu Lumsdaine]

Here is a proper MWE for my use-case of dependent lists — it’s a bit long, but I think keeping it closer to the actual intended use makes the intuition clearer than compressing it more.

inductive DList {α} (β : α → Type) : List α → Type where
  | nil : DList β []
  | cons {a} (b : β a) {as} (bs : DList β as) : DList β (a::as)

/- black-box various background definitions -/
def Ty : Type := sorry
def Cxt : Type := sorry
def cxt_extend : Cxt → Ty → Cxt := sorry
def Tm : Cxt → Ty → Type := sorry
def Telescope : Cxt → Cxt → Type := sorry
def tele_extend : {Δ Γ : Cxt} → (f : Telescope Δ Γ) → {A : Ty} → (Tm Δ A)
                                     → Telescope Δ (cxt_extend Γ A) := sorry

def cxt_extend_list (Γ : Cxt) (As : List Ty) : Cxt :=
  As.foldl cxt_extend Γ

def tele_extend_list {Δ Γ : Cxt} (f : Telescope Δ Γ)
                                (Aas : List (Σ (A : Ty), Tm Δ A)) :
    Telescope Δ (cxt_extend_list Γ (Aas.map Sigma.fst)) :=
  match Aas with
  | .nil => f
  | .cons Aa Aas' => tele_extend_list (tele_extend f Aa.snd) Aas'

/- writing as match requires DList argument before cxt, telescope -/
def tele_extend_dlist'
      {Δ : Cxt} {As : List Ty} (as : DList (Tm Δ) As)
      {Γ} (f : Telescope Δ Γ) :
    Telescope Δ (cxt_extend_list Γ As) :=
  match as with
  | .nil => f
  | .cons a as' => tele_extend_dlist' as' (tele_extend f a)

def tele_extend_dlist
      {Δ Γ : Cxt} (f : Telescope Δ Γ)
      {As : List Ty} (as : DList (Tm Δ) As) :
    Telescope Δ (cxt_extend_list Γ As) :=
  tele_extend_dlist' as f

variable (Δ Γ : Cxt) (f : Telescope Δ Γ)
variable (A1 A2 A3 : Ty) (a1 : Tm Δ A1) (a2 : Tm Δ A2) (a3 : Tm Δ A3)

/- reasonably nice to read + write -/
#check tele_extend_list f [⟨_,a1⟩,⟨_,a2⟩,⟨_,a3⟩]

/- nicer, once a list-like notation set up for DList -/
#check tele_extend_dlist f ((((DList.nil).cons a1).cons a2).cons a3)

[Floris van Doorn]

Is docs#List.TProd what you're looking for? See the module doc for more information.

[Eric Wieser]

Regarding "writing as match requires DList argument before cxt, telescope", a :) fixes it:

def tele_extend_dlist
      {Δ : Cxt} {As : List Ty}
      {Γ : Cxt} (f : Telescope Δ Γ) (as : DList (Tm Δ) As) :
    Telescope Δ (cxt_extend_list Γ As) :=
  match as with
  | .nil => f
  | .cons a as' => (tele_extend_dlist' (tele_extend f a) as' :)