[Haskell-cafe] Why were datatype contexts removed instead of "fixing them"?

[harry]

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
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Joe Quinn]

From what I have heard, they are completely subsumed by GADTs, which is
a stable enough extension that it was considered unimportant to save.

Your Foo would be something like this:

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

[Kim-Ee Yeoh]

On Thu, Apr 25, 2013 at 6:36 PM, Joe Quinn <headprogr...@gmail.com> wrote:

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

(Yup, tripped up a few of us already!)

-- Kim-Ee

[harry]

Kim-Ee Yeoh <ky3 <at> atamo.com> 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]

On Thu, Apr 25, 2013 at 6:38 AM, harry <volde...@hotmail.com> 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?

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.

--

brandon s allbery kf8nh                               sine nomine associates

allb...@gmail.com                                  ball...@sinenomine.net

unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

[Gábor Lehel]

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.

--
Your ship was destroyed in a monadic eruption.

[harry]

Brandon Allbery <allbery.b <at> gmail.com> 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?

[Dan Doel]

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.

[Gábor Lehel]

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

[Dan Doel]

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

[wren ng thornton]

On 4/25/13 9:49 PM, Dan Doel wrote:
> I don't really think they're worth saving in general, though. I haven't
> missed them, at least.

The thing I've missed them for (and what I believe they were originally
designed for) is adding constraints to derived instances. That is, if I
have:

data Bar a => Foo a = ... deriving Baz

Then this is equivalent to:

data Foo a = ...
instance Bar a => Baz (Foo a) where ...

where the second ellipsis is filled in by the compiler. Now that these
constraints have been removed from the language, I've had to either (a)
allow instances of derived classes which do not enforce sanity
constraints, or (b) implement the instances by hand even though they're
entirely boilerplate.

The behavior of these constraints is certainly unintuitive for beginners,
but the constraints themselves are very helpful when programming with
phantom types and type-level functions for constraints.

--
Live well,
~wren

[Emil Axelsson]

2013-04-26 04:31, wren ng thornton skrev:
> On 4/25/13 9:49 PM, Dan Doel wrote:
>> I don't really think they're worth saving in general, though. I haven't
>> missed them, at least.
>
> The thing I've missed them for (and what I believe they were originally
> designed for) is adding constraints to derived instances. That is, if I
> have:
>
> data Bar a => Foo a = ... deriving Baz
>
> Then this is equivalent to:
>
> data Foo a = ...
> instance Bar a => Baz (Foo a) where ...
>
> where the second ellipsis is filled in by the compiler. Now that these
> constraints have been removed from the language, I've had to either (a)
> allow instances of derived classes which do not enforce sanity
> constraints, or (b) implement the instances by hand even though they're
> entirely boilerplate.

I think standalone deriving solves this:

deriving instance Bar a => Baz (Foo a)

/ Emil

[Guy]

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.

[Edward Kmett]

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.

[harry]

Dan Doel <dan.doel <at> gmail.com> 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.

[Brandon Allbery]

On Sun, Apr 28, 2013 at 3:59 AM, harry <volde...@hotmail.com> wrote:

Dan Doel <dan.doel <at> gmail.com> 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.

[gs]

Brandon Allbery <allbery.b <at> gmail.com> 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 - but would it break any
real-world code?)

[Alexander Solla]

On Sun, Apr 28, 2013 at 10:29 AM, gs <volde...@hotmail.com> wrote:

Brandon Allbery <allbery.b <at> gmail.com> 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.

[gs]

Alexander Solla <alex.solla <at> gmail.com> 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 :-)

[Alexander Solla]

On Sun, Apr 28, 2013 at 10:55 AM, gs <volde...@hotmail.com> wrote:

Alexander Solla <alex.solla <at> gmail.com> 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.