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

[Viktor Dukhovni]

On Mon, Sep 14, 2020 at 01:00:40PM +1200, Anthony Clayden wrote:

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

Thanks for that reference.  I guess that puts retroactively on Simon's
side, and perhaps in alignment with:

    http://web.archive.org/web/20151001182427/http://code.haskell.org/~dons/haskell-1990-2000/msg04073.html

from the same thread.

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

Yes, "fmap" is not good fit for Set.  And indeed with the GADT
constructor constraint, there's no way to define it for non-empty sets,
since the constraint cannot be met under general conditions.

A restricted fmap that only allowed maps between types that support
equality, could be defined, but much is lost, since Applicative would
not be available, for lack of equality on arrows.

With the explicit equality operator representation:

    data Set a = MkSet [a] (EqOper a)

a function (Set a) -> (Set b) would have to provide not only a pointwise
mapping, but also an explicit (EqOper b):

    f :: Set SomeA -> Set SomeB
    f (MkSet a eqA) = MkSet (g a) eqB

where sanity also requires (but difficult to check in general)
that: eqA a1 a2 `implies` eqB (g a1) (g a2).

That is, `g` has to respect the `eqA` equivalence classes, something
we'd like to expect from e.g. `Eq` instances, but again cannot in
general check.

-- 
    Viktor.