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

Anthony Clayden anthony_clayden at clear.net.nz
Mon Sep 14 01:00:40 UTC 2020

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
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.

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

More information about the Haskell-Cafe mailing list