On Wednesday 24 April 2013, 16:45:35, gs wrote:
Daniel Fischer
writes: Well, the context is not redundant, that's the crux.
You can specify the type `Source v a` even when there is no `Variable v` instance [whether you use DatatypeContexts - which, again, are pretty useless because they don't do what one would expect - or GADTs]. And such a type is inhabited by bottom, you just can't create non-bottom values of such a type.
Hence the `Variable v` context gives additional information that is needed
for
the instance.
I'm not following - perhaps you could give a practical example? I'm trying to understand the flaw in this:
1) The compiler sees that a Source v a can only be created when v is a variable.
No, that is the catch: undefined :: Source NotAnInstanceOfVariable Int is possible.
2) Whenever Source v a is used, the compiler should understand that v is a variable without me having to remind it.
But when you use the value constructor, foo (Source list var) = ... you know that the `v` parameter of the type must have a Variable instance. When you use a GADT, the compiler knows that too and can use that fact, when you use DatatypeContexts, the compiler can't use that knowledge (even though it has the knowledge). The point is that the type class dictionary is required to use the class methods, and with a GADT, the dictionary is bundled with the constructor, so pattern-matching makes the dictionary available. Not so with DatatypeContexts, hence the dictionary must be explicitly passed with the context on the function. Did I already mention that DatatypeContexts are fairly useless and have therefore been removed from the language?