Heterogeneous list whose types "depend on itself"

Stream: lean4

[André Muricy Santos]

Hey all,

I'm trying to define a "dependent input" type that is basically a heterogeneous list whose elements' types
depend on the value of the previous element. So in a sense, the list's type "depends on itself". The desired
usage is something like this: imagine you want to construct a list of elements that are either strings or integers.

The first element is a string, but! If it's the string "a", then next element is an integer, otherwise a string.
If the integer is 1, then the next element is a string, otherwise an integer, and so on. The following value is
of this imagined dependent list:

["a", 1, "b", "c", "a", 2, 3, 5]

The normal way of defining heterogeneous lists is merely indexed by a list of a defined type, which means
the order in which the values of different types appear is determined by the list it's indexed by. The value
above is of the following HList type:

inductive HList {α : Type} (β : α → Type) : List α → Type
  | nil  : HList β []
  | cons : β i → HList β is → HList β (i::is)

infixr:67 " ::: " => HList.cons

example : HList intOrString [true, false, true, true, true, false, false, false] :=
  "a" ::: Int.ofNat 1 ::: "b" ::: "c" ::: "a" ::: Int.ofNat 2 ::: Int.ofNat 3 ::: Int.ofNat 5 ::: HList.nil

But this is determined by the list of booleans provided "ahead of time". I want the type of the list to be
programmatically determined by its own elements. Is this even possible?

[Mario Carneiro]

inductive Kind | string | int

abbrev Kind.toType : Kind → Type
  | .string => String
  | .int => Int

abbrev Kind.next : {k : Kind} → k.toType → Kind
  | .string, "a" => .int
  | .string, _ => .string
  | .int, 1 => .string
  | .int, _ => .int

inductive SList : Kind → Type
  | nil {k}  : SList k
  | cons {k} (a : k.toType) : SList (k.next a) → SList k

infixr:67 " ::: " => SList.cons
notation  "ι" x:max => (x : Int)

example : SList .string :=
  "a" ::: ι 1 ::: "b" ::: "c" ::: "a" ::: ι 2 ::: ι 3 ::: ι 5 ::: .nil

[Tom]

wow, impressive.

I believe that with enough trial and error I would be able to cobble something like that together. However, I don’t quite understand why ‘abbrev’ is used. Is it just needed to “force the evaluation” of the term?

in general, is there guidance/best practices on this? Like use ‘def’ and switch to ‘abbrev’ as needed?

[François G. Dorais]

For all practical purposes, abbrev is the same as @[inline, reducible]. The inline part tells the compiler to see through the def and inline it. The reducible part tells the kernel to see through the def and reduce it. Basically, the user is the only one that get's to see the abbrev, the compiler and the kernel both look right through it to the definition.

[Mario Carneiro]

The usage of abbrev in this example is unusual, and used so that the typeclass system will reduce these functions. Even so it doesn't quite work, otherwise I wouldn't have needed the ι 1 notations

[François G. Dorais]

But that's actually the match not working, right?

[Mario Carneiro]

I think? I'm not really sure where it's getting stuck

[André Muricy Santos]

beautiful, guys! Thanks for the help. I managed to generalize it to fit my purposes:

inductive SList {α : Type} {β : α → Type} {γ : (a : α) → (β a) → α} : α → Type
  | nil {s : α}  : SList s
  | cons {s : α} (a : β s) : SList (γ s a) → SList s

I still get confused by what appears to the left and right of a colon in an inductive definition. What we're saying here is that for ALL α, β and γ, give me a value of type α and I will give you back a type. So the nil constructor, as a function, by taking no arguments "claims" to be a value of all indexed types (no matter if the value is 1, "hello", IO FilePath etc.

The cons constructor takes an element that is the result of applying β to any given s : α, AND an SList indexed over the result of applying γ to that particular s and that particular a in the fiber over that particular s. Then it gives a value of SList indexed over the original s.

It's almost like whatever appears to the right of the colon in the inductive definition is what the constructors get to say the elements they build are a part of, and whatever's to the left is universal, i.e. they "can't touch it". I keep thinking of analogies to hashmaps where the thing to the right of a colon is a key k whose value is "the universal type keyed by k".

Is this a proper intuition?

[Tom]

François G. Dorais said:

For all practical purposes, abbrev is the same as @[inline, reducible]. The inline part tells the compiler to see through the def and inline it. The reducible part tells the kernel to see through the def and reduce it. Basically, the user is the only one that get's to see the abbrev, the compiler and the kernel both look right through it to the definition.

Thanks for the explanation!

In this case, when you say the compiler will inline it, what is there to inline? Isn't the above just a type-level computation? Or are there parts of the above that will need to be reified to run time?

[Tom]

@André Muricy Santos

I still get confused by what appears to the left and right of a colon in an inductive definition.

Until someone more knowledgeable than me can answer your question, perhaps the beginning of this chapter in FPiL can help? Indexed Families

[Tom]

As an aside, in my (meager) understanding of Lean, in the case of cons

cons {s : α} (a : β s) : SList (γ s a) → SList s

is just syntax sugar for

cons {s : α} : (a : β s) -> SList (γ s a) -> SList s

or even

cons : {s : α} -> (a : β s) → SList (γ s a) → SList s

so the ":" here doesn't have the same semantic meaning as in the type definition itself. Maybe it could be considered good style to syntactically/visually separate your indexed and non-indexed parameters to the constructor? I am not sure but perhaps that's what Mario was going for here.

[Tom]

I am not sure if this code example will help clarify (or cause more confusion :grinning_face_with_smiling_eyes: ):

inductive Plus (n : Nat) where
  | base
  | plus (m : Nat)
deriving Repr

inductive Plus' : n -> Type where
  | base (k: Nat) : Plus' k
  | plus (m : Nat) : Plus' n -> Plus' (m + n)
deriving Repr

def eval : Plus n -> Nat
  | .base => n
  | .plus m => m + n

def eval' : (Plus' n) -> Nat
  | .base k => k
  | .plus m p => m + eval' p

def plus := (.plus 4 : Plus 8)
def plus' := (Plus'.plus 4 (.base 8 : Plus' 8))

#eval eval plus
#eval eval' plus'

[Mario Carneiro]

Tom said:

As an aside, in my (meager) understanding of Lean, in the case of cons

cons {s : α} (a : β s) : SList (γ s a) → SList s

is just syntax sugar for

cons {s : α} : (a : β s) -> SList (γ s a) -> SList s

or even

cons : {s : α} -> (a : β s) → SList (γ s a) → SList s

so the ":" here doesn't have the same semantic meaning as in the type definition itself. Maybe it could be considered good style to syntactically/visually separate your indexed and non-indexed parameters to the constructor? I am not sure but perhaps that's what Mario was going for here.

This is correct. I just prefer to put dependent arrows before the colon when possible since it's a bit shorter that way (but you might also want to put other arguments before the colon if you want to give them meaningful names)

[Yuyang Zhao]

François G. Dorais said:

For all practical purposes, abbrev is the same as @[inline, reducible]. The inline part tells the compiler to see through the def and inline it. The reducible part tells the kernel to see through the def and reduce it. Basically, the user is the only one that get's to see the abbrev, the compiler and the kernel both look right through it to the definition.

I think the kernel doesn't knows @[reducible]. Elaborator knows @[reducible], the kernel only knows docs#Lean.ReducibilityHints. And docs#Lean.ReducibilityHints makes abbrev and @[reducible, inline] def not the same, there are several PRs in mathlib that change @[reducible] def to abbrev to improve performance.

[François G. Dorais]

That's correct. This is why I said "for all practical purposes" at the outset. (I probably should have mentioned the elaborator though.)