7 ms·

How are type families worse than fundeps? That's a pretty ridiculous assertion; the things you can do with fundeps are strictly fewer than the things you can do

by wyager 10y ago

How are type families worse than fundeps? That's a pretty ridiculous assertion; the things you can do with fundeps are strictly fewer than the things you can do with type families. > The principled approach You're dead wrong. The principled approach here is dependent types and full-featured type-level functions. Fundeps are a hack that let you implement a small subset of such functions (while type families gets us a bit closer to the ideal). > they have unacceptable limitations as a large-scale program structuring construct. Such as? > And instead use an ML-style module system for that purpose. How about we just use C macros for parametricity? ML-style modules have their uses, but they aren't nearly as elegant as a clean type-level solution.

catnaroek 10y ago
> How are type families worse than fundeps? That's a pretty ridiculous assertion; the things you can do with fundeps are strictly fewer than the things you can do with type families. It's not about how much you can do (otherwise, just use a dynamic language, you can do everything, even shoot yourself in the foot!), it's about whether the result makes sense, and how much effort it takes to make sense of it. > You're dead wrong. The principled approach here is dependent types and full-featured type-level functions. Fundeps are a hack that let you implement a small subset of such functions (while type families gets us a bit closer to the ideal). You wanna play the dependent type theory card? Type families as provided in Haskell are incompatible with univalence. type instance Foo Bool = Int type instance Foo YesNo = String Please kindly provide the isomorphism between `Int` and `String`. Case analysis only makes sense when performed on the cases of an inductive type, which the kind of all types is not. > Such as? The insistence on globally unique instances? > How about we just use C macros for parametricity? What does this even mean? > ML-style modules have their uses, but they aren't nearly as elegant as a clean type-level solution. See here for how modular type classes, as proposed for ML, would actually prevent the issues caused by Haskell-style type classes: http://blog.ezyang.com/2014/09/open-type-families-are-not-modular/#comment-20939 http://blog.ezyang.com/2014/09/open-type-families-are-not-mo...
- wyager 10y ago
  > otherwise, just use a dynamic language, you can do everything, even shoot yourself in the foot! Type classes allow huge flexibility while maintaining type safety, to a much greater degree than fundeps allow. > it's about whether the result makes sense Which they do. Perhaps you have some examples of when type families confused you or made you perform an error? > Type families as provided in Haskell are incompatible with univalence. TFs aren't dependent types. However, they are on the right track. Fundeps are farther away from the right idea. Could you explain to me what's wrong with your example? I'm not up to date on HoTT, but it seems like there's nothing in principle wrong with pattern matching on elements of *. That seems like an important feature of type-level functions. >The insistence on global unique instances? 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"), and it's very easy to use newtype wrappers to create new instances if needed. > What does this even mean? ML modules are flexible, but backwards from a theoretical perspective. Parametricity is something that should be embedded in the type system, not the module system. > See here 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.
  - catnaroek 10y ago
    > 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 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/ 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.

by wyager 10y ago

catnaroek 10y ago

> How are type families worse than fundeps? That's a pretty ridiculous assertion; the things you can do with fundeps are strictly fewer than the things you can do with type families. It's not about how much you can do (otherwise, just use a dynamic language, you can do everything, even shoot yourself in the foot!), it's about whether the result makes sense, and how much effort it takes to make sense of it. > You're dead wrong. The principled approach here is dependent types and full-featured type-level functions. Fundeps are a hack that let you implement a small subset of such functions (while type families gets us a bit closer to the ideal). You wanna play the dependent type theory card? Type families as provided in Haskell are incompatible with univalence. type instance Foo Bool = Int type instance Foo YesNo = String Please kindly provide the isomorphism between `Int` and `String`. Case analysis only makes sense when performed on the cases of an inductive type, which the kind of all types is not. > Such as? The insistence on globally unique instances? > How about we just use C macros for parametricity? What does this even mean? > ML-style modules have their uses, but they aren't nearly as elegant as a clean type-level solution. See here for how modular type classes, as proposed for ML, would actually prevent the issues caused by Haskell-style type classes: http://blog.ezyang.com/2014/09/open-type-families-are-not-modular/#comment-20939 http://blog.ezyang.com/2014/09/open-type-families-are-not-mo...

wyager 10y ago
> otherwise, just use a dynamic language, you can do everything, even shoot yourself in the foot! Type classes allow huge flexibility while maintaining type safety, to a much greater degree than fundeps allow. > it's about whether the result makes sense Which they do. Perhaps you have some examples of when type families confused you or made you perform an error? > Type families as provided in Haskell are incompatible with univalence. TFs aren't dependent types. However, they are on the right track. Fundeps are farther away from the right idea. Could you explain to me what's wrong with your example? I'm not up to date on HoTT, but it seems like there's nothing in principle wrong with pattern matching on elements of *. That seems like an important feature of type-level functions. >The insistence on global unique instances? 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"), and it's very easy to use newtype wrappers to create new instances if needed. > What does this even mean? ML modules are flexible, but backwards from a theoretical perspective. Parametricity is something that should be embedded in the type system, not the module system. > See here 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.
- catnaroek 10y ago
  > 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 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/ 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.