could open type families be deprecated?
And associated types?
(Open) TypeFamilies have the important feature of distributed logic (same with typeclasses): in your own module, you declare your own type or data, and can then give an instance for it. But yet keep the overall TF logic coherent. (That is, no overlaps, and a type-despatch mechanism.)
I’ve not seen any DH proposal yet for how that’ll work with ‘ordinary’ function definitions. I guess we’re still some way off that, as @jaror says.
Then no, not yet.
3 Likes
Perhaps a type level function would not be directly extensible in dependent haskell. But wouldn’t there extensible alternatives? Like a typeclass with type level instances?
Idris2 does not need need open type level functions ( or type families ) presumably because you can do the above
I’m thinking now about Existential types. And they something in common with DH.
@int-index you describe foreach as “unerasible”. And it is Ok if we need just 1-5 such types per executapable program.
But what if we neet 1-10 millions of them?
Sure, we must utilize such types after we no longer need them.
How do you decide if unerasible type is still saved or it is already deleted?
I’m not sure what you mean (e.g., “we must utilize such types after we no longer need them” does not make sense to me), but types can be garbage collected just like almost all other things at run time. It would work very similarly to how Typeable works today.