search

JamesGallicchio / LeanColls

WIP collections library for Lean 4
https://jamesgallicchio.github.io/LeanColls/docs/
Apache License 2.0
30 stars 7 forks source link

Dependently typed `Indexed` #2

Open lecopivo opened 10 months ago

lecopivo commented 10 months ago

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 commented 10 months ago

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 commented 10 months ago

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.