| > Type classes allow huge flexibility while maintaining type safety, to a much greater degree than fundeps allow. Um, aren't functional dependencies an add-on to multiparameter type classes? I don't see where the opposition is. > Which they do. Perhaps you have some examples of when type families confused you or made you perform an error? I already gave an example above. I defined two type instances that violate the principle of not doing evil: https://ncatlab.org/nlab/show/principle+of+equivalence > TFs aren't dependent types. However, they are on the right track. Dependent types are a good idea. The way Haskell attempts to approximate them is not. Parametricity is too good to give up. With the minor exception of reference cells (`IORef`, `STRef`, etc.), if two types are isomorphic, applying the same type constructor to them should yield isomorphic types. You know what type families actually resemble? What C++ calls “traits”: ad-hoc specialized template classes containing type members. > Fundeps are farther away from the right idea. Functional dependencies are a consistent extension to type classes, which don't introduce a second source of ad-hoc polymorphism, unlike type families. > Why is this a problem? It makes sense from a theoretical perspective (we don't associate multiple ordering properties with the things we call "the integers"), What if I want to order them as Grey-coded numbers? In any case, the integers are far from the only type that can be given an order structure, and many types don't have a clear “bestest” order structure to be preferred over other possible ones. > and it's very easy to use newtype wrappers to create new instances if needed. Creating `newtype` wrappers is easy at the type level, but using them is super cumbersome at the term level. > ML modules are flexible, but backwards from a theoretical perspective. ML modules are plain System F-omega: http://www.mpi-sws.org/~rossberg/1ml/ . Where's the backwardness? > Parametricity is something that should be embedded in the type system, not the module system. It's type families, as done in Haskell, that violate parametricity! Standard ML has parametric polymorphism, uncompromised by questionable type system extensions. > Interesting example. However, I doubt that the syntactic cost of using such a system is less than the syntactic cost of enforcing global instance uniqueness and using newtype wrappers. I can't imagine it being more cumbersome than wrapping lots of terms in newtype wrappers just to satisfy the type class instance resolution system. |
You're right, I meant "type families".
> I defined two type instances that violate the principle of not doing evil:
We're not doing abstract category theory; we're writing computer programs (well, I am). Have you ever run into a problem with type families in that capacity?
>if two types are isomorphic, applying the same type constructor to them should yield isomorphic types.
Agreed, but there's a difference between type functions and type constructors. TFs are (a limited form of) type functions. Value-level constructors admit lots of nice properties that value-level functions do not, and I see no reason to be uncomfortable with this being reflected at the type level.
> What if I want to order them as Grey-coded numbers
Use a newtype wrapper. Even if a language allowed ad-hoc instances, I would consider it messy practice to apply some weird non-intuitive ordering like this without specifically making a new type for it.
> Creating `newtype` wrappers is easy at the type level, but using them is super cumbersome at the term level.
And using ML-style modules is easy at the term level, but cumbersome at the type level.
It's a tradeoff, and I suspect that newtypes are usually the cleaner/easier solution.
> ML modules are plain System F-omega
I hadn't seen the 1ML project. That's pretty cool.
> It's type families, as done in Haskell, that violate parametricity!
How so? I really don't understand your argument here, if you just take TFs to be a limited form of type function.