Universe level of heterogeneous list

Stream: lean4

[Brendan Seamas Murphy]

Say I define a type of heterogeneous lists by

inductive HList.{u} : List (Type u) → Type (u+1)
  | nil  : HList []
  | cons : {τ : Type u} → {τs : List (Type u)} → τ → HList τs → HList (τ :: τs)

Then HList τs lives in the universe u+1 because each node of the list has to store the type of that element. But we can define an equivalence (τs : List (Type u)) → HList τs ≃ List.foldr Prod PUnit.{u + 1} τs, so in fact HList τs is essentially u-small. Is there any clever way of rewriting this definition that's still an inductive type but lives in Type u?

[Kyle Miller]

I'm curious about this too. It seems like the fact that List (Type u) is an index to the inductive type means that {τ : Type u} and {τs : List (Type u)} shouldn't be counted for the universe bump. Maybe there's some subtlety to constructors (like ::) in indices, or maybe this is something that could be supported but isn't? I have heard that there are some inductive types that the elaborator rejects but the kernel wouldn't -- this isn't one of those, is it?

[Jannis Limperg]

Agda also rejects this:

open import Data.List

data HList {u} : List (Set u) → Set u where
  nil : HList []
  cons : ∀ {τ τs}, τ → HList τs → HList (τ ∷ τs)

{-
Set (Agda.Primitive.lsuc u) is not less or equal than Set u
when checking that the type List (Set u) of an argument to the
constructor cons fits in the sort Set u of the datatype.
Note: this argument is forced by the indices of cons, so this
definition would be allowed under --large-indices.
-}

The mentioned large-indices option is apparently known to be inconsistent with the no-UIP version of Agda's type theory, but since Lean has UIP, it could maybe relax its restrictions here.

[Kyle Miller]

Just to check, by writing an implementation for the type by hand, this inductive type should be OK in Lean:

universe u

def HList (τs : List (Type u)) : Type u := τs.foldr Prod PUnit

@[match_pattern] def HList.nil : HList [] := PUnit.unit

@[match_pattern] def HList.cons {τ : Type u} {τs : List (Type u)} (x : τ) (xs : HList τs) :
    HList (τ :: τs) := (x, xs)

def HList.rec {motive : (τs : List (Type u)) → HList τs → Sort u}
    (nil : motive [] HList.nil)
    (cons : {τ : Type u} → {τs : List (Type u)} → (x : τ) → (xs : HList τs) →
              motive τs xs → motive (τ :: τs) (HList.cons x xs))
    {τs : List (Type u)} (xs : HList τs) : motive τs xs :=
  match τs, xs with
  | [], PUnit.unit => nil
  | _ :: _, (x, xs) => cons x xs (HList.rec nil cons xs)

[Kyle Miller]

I wonder if it's worth filing a Lean 4 issue for this feature?

Are there other cases where large indices would be useful?

[Brendan Seamas Murphy]

Side note, in what ways does the manual construction differ from an inductive type like List? Like, is the runtime representation any larger? My understanding is that it should be the same, but I'm not sure. Does the positivity checker recognize that α is positive in HList (α::τ) for either/both definitions?

[Kyle Miller]

I think the runtime representation should be exactly the same between the List.foldr one and HList (if it worked)

[Kyle Miller]

Actually, the List.foldr seems to be more efficient. I'm seeing that the inductive type stores the list of types (but the elements of the list are cleared, since types have no runtime representation)

[Brendan Seamas Murphy]

Huh! I would've thought List X got erased if X did

[Brendan Seamas Murphy]

Kyle Miller said:

I wonder if it's worth filing a Lean 4 issue for this feature?

Are there other cases where large indices would be useful?

I'd like to get a better understanding of the tradeoffs or how it works in other languages first, but it would be nice to have this definition accepted! I'm kind of shocked that heterogenous lists and arrays aren't in Std

[Brendan Seamas Murphy]

(my use case is for defining morphisms in a version of the TypeVec category based on vectors as a subtype of lists, because it would be useful in a formalization of multicategories based on lists I'm writing)

[François G. Dorais]

IIRC, "indices don't matter" forces any Eq-like inductive definition to live in the lowest universe (Prop) and therefore implies UIP. I don't immediately recall the details.

[Mario Carneiro]

Kyle Miller said:

I'm curious about this too. It seems like the fact that List (Type u) is an index to the inductive type means that {τ : Type u} and {τs : List (Type u)} shouldn't be counted for the universe bump.

It's the opposite: having them as indices rather than as parameters is what leads to the problem

[Kyle Miller]

Sure, parameters don't have this issue, but I mean that it seems like in principle constructor arguments that are constrained by the indices shouldn't necessarily lead to a universe bump

[Mario Carneiro]

This is also known as "non-uniform parameters"

[Mario Carneiro]

it's a kernel extension which I don't think buys too much and increases the trust base so I'm not inclined toward it

[Mario Carneiro]

you can define such types by recursion so I don't see the point

[Mario Carneiro]

that is, the List (Type u) argument is not quite an index but also not quite a parameter

[Kyle Miller]

Mario Carneiro said:

you can define such types by recursion so I don't see the point

Just to check -- you mean like my code block implementing HList, right?

[Mario Carneiro]

yes

[Mario Carneiro]

you don't want it to be a proper index because then you need "too many constructors"

[Kyle Miller]

Do you think the inductive command could set up this recursion and implement the type?

[Mario Carneiro]

Another classic example of non-uniform parameters is:

inductive BalancedTree : Type u → Type u
  | leaf : α → BalancedTree α
  | pair : BalancedTree (α × α) → BalancedTree α

[Brendan Seamas Murphy]

(another fun encoding of HList τs, although it's still in universe u+1, is as { xs : List (Σ τ, τ) // xs.map Sigma.fst = τs }. This requires way too much casting to use though)

[Mario Carneiro]

Kyle Miller said:

Do you think the inductive command could set up this recursion and implement the type?

The lean 4 inductive command doesn't do inductive simulation anymore, so that seems possibly contentious

[Mario Carneiro]

I think we need a better story for doing simulations in inductive and coinductive but I don't think it's a year 1 goal

[Mario Carneiro]

I've never really seen the point of an HList type, you can just use iterated products because the arity is fixed

[Kyle Miller]

I guess a motivated individual could write inductive! to try hard to compile a type to inductive and then wire it up to look like the inductive you think it is...

[Mario Carneiro]

There are two issues with that strategy:

1. We really want to guarantee inductive-like ABI and compiler handling, most encodings have difficulty with this without special compiler support
2. All the tactics need to not peek through the abstraction and treat it like an inductive type, necessitating many changes to the metaprogramming API

[Max Nowak 🐉]

You also wouldn’t get nice pattern matching and would have to call your defined recursor yourself. Although, I do wonder how hard it would be to make the match compiler support custom recursors