Kim-Ee Yeoh writes:

data Foo a where   Foo :: Eq a => a -> Foo a

is equivalent to

data Foo a = Eq a => Foo a

but is different from

data Eq a => Foo a = Foo a

... and nothing in GADTs does what one would naively expect the last declaration to do.

Brandon Allbery writes:

As I understand it, it's because fixing them involves passing around a dictionary along with the data, and you can't do that with a standard declaration (it amounts to an extra chunk of data that's only *sometimes* wanted, and that "sometimes" complicates things). GADTs already have to pass around extra data in order to support their constructors and destructors; and, being new and not part of the standard, they don't have backward compatibility or standards compatibility issues, so they can get away with including the extra dictionary without breaking existing programs.

But you can't do this with GADTs either?

It is not completely backwards compatible, because (for instance) the declaration: newtype C a => Foo a = Foo a was allowed, but: newtype Foo a where Foo :: C a => a -> Foo a is an illegal definition. It can only be translated to a non-newtype data declaration, which changes the semantics. On Thu, Apr 25, 2013 at 10:35 AM, Gábor Lehel wrote:

I've wondered this too. What would have been wrong with a simple source-to-source translation, where a constraint on the datatype itself translates to the same constraint on each of its constructors? Perhaps it would be unintuitive that you would have to pattern match before gaining access to the constraint? On a superficial examination it would have been backwards-compatible, allowing strictly more programs than the previous handling.

On Thu, Apr 25, 2013 at 12:38 PM, harry wrote:

...

If I understand correctly, the problem with datatype contexts is that if we have e.g. data Eq a => Foo a = Foo a the constraint Eq a is thrown away after a Foo is constructed, and any method using Foos must repeat Eq a in its type signature.

Why were these contexts removed from the language, instead of "fixing" them?

PS This is following up on a discussion on haskell-beginners, "How to avoid repeating a type restriction from a data constructor". I'm interested in knowing whether there's a good reason not to allow this, or if it's just a consequence of the way type classes are implemented by compilers.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Your ship was destroyed in a monadic eruption. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I can't think of any at the moment that are still in force. However, one that might have been relevant at the time is: data C a => Foo a = Foo a a foo :: Foo a -> (a, a) foo ~(Foo x y) = (x, y) Irrefutable matches used to be disallowed for GADT-like things, which would break the above if it were translated to GADTs. Now they just don't introduce their constraints. However, another thing to consider is that getting rid of data type contexts was accepted into the language standard. It's not really possible to fix them by translation to GADTs in the report, because GADTs aren't in the report, and probably won't be for some time, if ever. And putting a fixed version natively into the report would require nailing down a lot of details. For instance, are the contexts simply invalid on newtypes, or do they just work the old way? I don't really think they're worth saving in general, though. I haven't missed them, at least. -- Dan On Thu, Apr 25, 2013 at 3:19 PM, Gábor Lehel wrote:

Good point, again. Is that the only problem with it?

On Thu, Apr 25, 2013 at 5:57 PM, Dan Doel wrote:

...

It is not completely backwards compatible, because (for instance) the declaration:

newtype C a => Foo a = Foo a

was allowed, but:

newtype Foo a where Foo :: C a => a -> Foo a

is an illegal definition. It can only be translated to a non-newtype data declaration, which changes the semantics.

On Thu, Apr 25, 2013 at 10:35 AM, Gábor Lehel wrote:

...

I've wondered this too. What would have been wrong with a simple source-to-source translation, where a constraint on the datatype itself translates to the same constraint on each of its constructors? Perhaps it would be unintuitive that you would have to pattern match before gaining access to the constraint? On a superficial examination it would have been backwards-compatible, allowing strictly more programs than the previous handling.

On Thu, Apr 25, 2013 at 12:38 PM, harry wrote:

...

If I understand correctly, the problem with datatype contexts is that if we have e.g. data Eq a => Foo a = Foo a the constraint Eq a is thrown away after a Foo is constructed, and any method using Foos must repeat Eq a in its type signature.

Why were these contexts removed from the language, instead of "fixing" them?

PS This is following up on a discussion on haskell-beginners, "How to avoid repeating a type restriction from a data constructor". I'm interested in knowing whether there's a good reason not to allow this, or if it's just a consequence of the way type classes are implemented by compilers.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Your ship was destroyed in a monadic eruption. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Your ship was destroyed in a monadic eruption.

That is because every other language conflates the notion of a class with a vtable smashed into every inhabitant of the class where everything has to be defined together in one monolithic definition. You also can't write sensible Monads in those languages (Where does return go?) or retroactively define new classes and make existing types instances of it without controlling the source code to every instance. On Fri, Apr 26, 2013 at 4:02 AM, Guy wrote:

Dan Doel wrote:

I don't really think they're worth saving in general, though. I haven't

...

missed them, at least.

Maybe you haven't :-) My code is cluttered with redundant type contexts - I can't think of a similar redundancy in any other language.

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe

On Sun, Apr 28, 2013 at 3:59 AM, harry wrote:

Dan Doel writes:

...

However, another thing to consider is that getting rid of data type contexts was accepted into the language standard.

... which means that implementers should be free to "fix" data type contexts however they like, as they are now complier extensions which won't conflict with standard Haskell.

Except that people do build older programs with newer Haskell compilers, and it's bad to "repurpose" a syntax like that because it leads to strange errors. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

On Sun, Apr 28, 2013 at 10:29 AM, gs wrote:

Brandon Allbery writes:

...

... which means that implementers should be free to "fix" data type contexts however they like, as they are now complier extensions which won't conflict with standard Haskell.

Except that people do build older programs with newer Haskell compilers, and it's bad to "repurpose" a syntax like that because it leads to strange errors.

"Remembering" data type contexts shouldn't break existing code, unless it's semantically broken already. (I'm sure that anyone could come up with a theoretical example of code which would break

These statements are contradictory.

- but would it break any real-world code?)

I do not support that criterion. We use theory to ENSURE that no real-world code will break.

On Sun, Apr 28, 2013 at 10:55 AM, gs wrote:

Alexander Solla writes:

...

I do not support that criterion. We use theory to ENSURE that no real-world code will break.

By theoretical example, I meant something which you would never expect to find in use. Perhaps it was a poor choice of wording in an academically orientated forum :-)

I understood that much. The problem is there is no good way to know what code we should "expect". Real world code might be "unexpected". Your criterion amounts to hoping no real world code breaks.