Hi all, I have a few replies to Andres' comments:
Extensibility: - Data types are non-extensible, however we can try to combine the approach with type classes to get some form of extensibility (RepLib proposes one solution like this).
I think I prefer the term "Specializability" (even though it is more of a mouthful.) Generic functions can be specialized at particular datatypes to specific operations. (LIGD does not support this behavior, but could be extended to do so by pushing RepLib through the GADT translation.)
The phrase "specialization" makes sense if you consider generic functions that in principle work on all data types, and now are trying to assign a new, specific behaviour to the function for one data type. But what if we have defined a function in the style of a generic programmign approach such as LIGD that does not have a catch-all case and does only work for a limited number of data types. That'd correspond to an ad-hoc overloaded functions. You might still want to extend such functions to new data types. And in this case, I think it's better to call the function "extensible" or "open".
I disagree here. Generic functions are not the same as ad-hoc overloaded functions because of datatype-genericity. This allows them to be defined by the structure of the datatype instead of its name, and is (I would argue) the key difference between generic programming and ad-hoc overloading, such as with type classes. Even though datatype genericity may not extend to all datatypes (Such as those that contain functions, or those that haven't been represented, there is a large class of common types that it does apply to.) Part of the confusion is that it is often the same mechanism solving two different problems. (a) Generic functions apply *uniformly* based on type structure. (b) Generic functions apply to many *but not all* types. Sometimes we would like a generic function to behave specially for a particular type in its domain. For example, newtype Set = S [Int] should use set equality not list equality. Sometimes we would like to extend a generic function to a type not in its domain. For example, in newtype Set = S ([Int], Int -> Bool), perhaps the function doesn't matter and we can define equality just by looking at the integers. In both cases, generic equality for types that contain Set should use the user-specified version of equality. Is there a framework that solves one problem but not the other? Or that solves the two problems with two different mechanisms? Personally, I think problem (a) occurs much more often than (b), which is why I prefer "specializability".
Performance considerations: - Sums of products based and therefore involving considerable performance penalties.
Besides the runtime types and sums-of-products explosion, there is also the issue of applying the identity function type coercions (if they are not optimized away). Those at least would be eliminated by using a GADT.
Isn't "explosion" a bit exaggerated, or am I missing something?
Sorry. That was an obscure analogy :-). In SML, strings are arrays of characters, and the function "explode" converts a string to a list of characters. I was thinking of the sum-of-products view as converting constructor arguments from a packed tuple (that cannot be accessed directly) into an accessible list of components.
I think the main overhead of the sums-of-products representation lies in the fact that it is different from the representation Haskell usually has for a value. So, at least in principle, every value has to actually be converted twice in order to apply a generic function, and optimizing this is tricky, especially if we want to do it in Haskell, without applying special knowledge about the application domain.
When you say "application domain" what do you mean? I think that if we make sure to use special purpose types to store the arguments of the constructor in the view and provide a library of operations for those types, then (perhaps) a smart Haskell compiler could optimize things under the covers.
What do you mean by "local redefinitions"?
Stefan has already given an answer. I think Bruno mentions this here because "local redefinitions" are a bit like having functions of different arities.
Sorry if I'm being dense, but I still don't see the connection between "local redefinitions" and different arities.
I think the case for GADTs in Haskell' would be strengthened if there were other Haskell compilers than GHC that implement GADTs. Does anyone know of any?
I haven't heard of any plans. The next HCAR is going to happen soon, so maybe I'll get a report from one of the implementation teams that tells me they're working on it.
Great! Thanks, Stephanie