[Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta

[Anthony Clayden]

On Fri, Sep 11, 2020 at 11:22 PM Anthony Clayden <
anthony_clayden at clear.net.nz> wrote:

> > On  Fri Sep 11 08:08:54 UTC 2020,  Viktor Dukhovni wrote:
>
> > With this particular type, I'd argue the real problem is adding the constraints
> to the constructors in the first place.
> >  With the constructors unconstrained, one gains the ability to define
> Functor instances, use Applicatives, ...
>
>
No that isn't going to work. As Phil Wadler says here
http://web.archive.org/web/20151001115936/http://code.haskell.org/~dons/haskell-1990-2000/msg04062.html
what's really going on is that we want some invariant to hold over the data
structure. A set's elements must be unique; so we need `Eq` to be able to
test that; but `Eq` alone doesn't capture the whole invariant.

So take an instance for Functor Set: `fmap` is to apply some arbitrary
function to the elements of the set; there's no guarantee that the values
returned will still be unique after applying the function. (Indeed there's
no guarantee the function's return type is in `Eq`.) Then we need something
within the overloading for `fmap` that will check uniqueness; and that'll
need an `Eq` constraint.

Or you decorate every call to those constructor classes/methods with
post-processing to fix up the mess. Which obfuscates the logic in your
elegant pointfree style.


> Or the 'Partial Type Constructors' paper shows a possible approach --
> which is really orthogonal to its main topic.
>
>
That paper picks up on a paper from John Hughes 1999, which is tackling
exactly the same requirements.

AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200914/78512555/attachment.html>