inBounds evidence for GetElem is an outparam

Stream: general

[Quinn]

why is inBounds evidence an outParam?

https://lean-lang.org/functional_programming_in_lean/type-classes/indexing.html#overloading-indexing

[Quinn]

class GetElem (coll : Type) (idx : Type) (item : outParam Type) (inBounds : outParam (coll → idx → Prop)) where
  getElem : (c : coll) → (i : idx) → inBounds c i → item

[Quinn]

The element type and the evidence function are both output parameters. GetElem has a single method, getElem, which takes a collection value, an index value, and evidence that the index is in bounds as arguments, and returns an element:

[Quinn]

I think of the evidence as an input.

[Kim Morrison]

It's the type of the evidence that is an outparam, not the evidence itself (which is the inbounds c i argument to the getElem field).

[Quinn]

So the function that returns the evidence is an output? It's still not clicking for me

[Quinn]

I get how the outParam annotation helps with type inference later

[Kim Morrison]

Notice the value of inBounds c i is a Prop, not data.

[Yury G. Kudryashov]

Given a container and an index type, the following are outputs:

• the type of elements in the container
• the predicate saying that an index is valid

E.g., for List a and Nat the outparams are a and fun l k => k \le l.length.

[Yury G. Kudryashov]

This means that there should be no two instances with the same collection type and the same index type that ask to prove different properties of the index in L[n]'(hn)

[Quinn]

i think i get it, ish. the type of the evidence is an outParam, but the evidence is still an input

[Quinn]

but it doesn't output a tuple (type_of_evidence, elem). it outputs a function type_of_evidence -> elem

[Quinn]

maybe outParam is just "anything that's late enough in left to right evaluation that the metavariable typer might get stuck", and doesn't actually refer to "output"

[Yury G. Kudryashov]

It means that typeclass search will be happy to search for GetElem (List α) Nat ?a ?b with unknown ?a and ?b. Also, it means that instances should be written so that coll and idx uniquely define item and inBounds.