You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
classForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) where
forIn {β} [Monad m] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
Note in particular that the class depends on ρ (the collection type) but not (x : ρ) (the particular collection being iterated over). This means that it is impossible to implement an iterator where the yielded element type depends on the value:
for x in (g : MyGraph) do-- x : VertexOf g
The current workaround for this is to define a wrapper type structure ElementOf (g : MyGraph) but this requires some boilerplate to set up, complicates usage code, and is also not very discoverable.
The way this situation can be improved is to move the (x : ρ) argument to a parameter, so that it can participate in typeclass inference such that α can depend on x:
classForIn (m : Type u₁ → Type u₂) {ρ : Sort u} (x : ρ) (α : outParam (Sort v)) where
forIn {β} [Monad m] (b : β) (f : α → β → m (ForInStep β)) : m β
(Note, I've also changed Type to Sort in two places here. I believe the use of Type in this position is not necessary, but this can be considered separately if desired.)
This impacts mainly users of the ForIn typeclass, namely libraries for programming such as Batteries, as well as users that have set up their own iterable collection types.
Proposal
Currently,
ForIn
has the following type:Note in particular that the class depends on
ρ
(the collection type) but not(x : ρ)
(the particular collection being iterated over). This means that it is impossible to implement an iterator where the yielded element type depends on the value:The current workaround for this is to define a wrapper type
structure ElementOf (g : MyGraph)
but this requires some boilerplate to set up, complicates usage code, and is also not very discoverable.The way this situation can be improved is to move the
(x : ρ)
argument to a parameter, so that it can participate in typeclass inference such thatα
can depend onx
:(Note, I've also changed
Type
toSort
in two places here. I believe the use ofType
in this position is not necessary, but this can be considered separately if desired.)This impacts mainly users of the
ForIn
typeclass, namely libraries for programming such as Batteries, as well as users that have set up their own iterable collection types.Community Feedback
This was recently discussed on Zulip.
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: