Heterogeneous List

Stream: general

[Wojciech Nawrocki]

Are there any attempts at heterogeneous lists in mathlib? These would be lists which admit elements of varying types, presumably with some constraint on the element types, otherwise you couldn't do much with such a thing. The use case I envision is to make using type classes more ergonomic, e.g. when I want to map a typeclass function over values of different types, all of which are in the class. For example, for pretty-printing:

/-- Typeclass-requiring, heterogeneous list. -/
inductive thlist (cl: Sort u → Sort v): Sort max (u+1) v
| nil: thlist
| cons {α: Sort u} [cl α]: α → thlist → thlist
notation `h[` l:(foldr `, ` (h t, thlist.cons h t) thlist.nil _ `]`) := l
open thlist

def map {cl: Sort u → Sort v} {β: Sort*} (f: Π {α: Sort u} [cl α], α → β)
  : thlist cl → list β
| (nil _) := []
| (@cons _ _ h a t) := @f _ h a :: map t

meta def fmt_all (l: thlist has_to_format): list format :=
  l.map @has_to_format.to_format

example : true := begin
  `[tactic.trace $ fmt_all h["abc", 2, (tt, ff)]],
  /- hlist.lean:24:2: information trace output
  [abc, 2, (tt, ff)] -/
end

[Reid Barton]

For this you could just use a list whose element type is a sigma type, right?

[Wojciech Nawrocki]

Hm, that might also work, thanks! Some universe errors appear when I try it with the same definition of cl, but it's probably possible.

[Floris van Doorn]

Maybe d_array is useful? It is a sequence of a fixed length where you can specify the type of the i-th element.

[Mario Carneiro]

I once tried to write heterogeneous lists but they didn't make anything easier. I found the problem was I didn't have an application

[Mario Carneiro]

The example can be done more simply:

meta def fmt_cons {α} [has_to_format α] (h : α) : list format → list format :=
list.cons (has_to_format.to_format h)

notation `fmt_all[` l:(foldr `, ` (h t, fmt_cons h t) [] `]`) := l

example : true := by tactic.trace fmt_all["abc", 2, (tt, ff)]; `[trivial]

[matt rice]

not really heterogeneus list i imagine, but over here I was playing with a qpf datatype like list of sigma,
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/qpf.20and.20type.20class.20instances

if we change that last line from eval to check:
#check list.map (alt.elim (λ l, alt.l (string.length l)) (λ r, alt.r(r + 1))) x

which in my original implicit formulation gives: list alt, and with Simon's recommendation of explicit type variables (and appropriate modifications) gives list (alt ℕ ℕ)

[matt rice]

This can kind of be annoying if you want a list of a bunch of types because you end up with list (alt ℕ (alt bool string)) etc...