Dependently typed `Indexed`

[lecopivo]

In SciLean, I need an unified interface to deal with functions, arrays(fixed sized) and structs. This can be done with a variant of Indexed which has dependent types. I call it StructType

I'm really not sure if there should be separate dependently typed version of Indexed or not. On one hand, dealing with dependent types is annoying and most of the time not necessary. On the other hand, having variant of Indexed just duplicates code.

A crucial difference of StructType from Indexed is that the index type is not marked outParam. This allows you to index for example the type Nat × ArrayN Nat n with Unit ⊕ Unit or Unit ⊕ Fin n. In SciLean, this is a crucial feature when doing automatic differentiation.

[JamesGallicchio]

I suspect it should be a separate type. I'm happy to maintain this amount of duplicate code, and most of the duplication should be avoidable by making IndexType do the iteration heavy lifting.

BTW, from the StructType file it seems this is not restricted to finite index types, which Indexed explicitly is constrained to?

[lecopivo]

Note the hierarchy

Indexed < StructType < FunLike

I'm tempted to call them Array/Struct/FunLike

FunLike has get and has injection to function type
StructLike has get,set,ofFn and has bijection with function type
ArrayLike has get,set,ofFn,fold and has bije tion with function type

Thinking about these interfaces in terms of this hierarchy might be useful.