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

[Anthony Clayden]

The sweet spot for GADTs is representing ASTs for EDSLs typefully. The
characteristics of those use cases is that each data constructor: carries
different constraints; returns a more specific type than `T a`; similarly
recursion may be to a more specific type.

There's a different use case (which is I suspect what was in mind for
DatatypeContexts), with characteristics for each data constructor:

* the constraints are the same for all the type's parameters;
* the return type is bare `T a`
* any recursion is also to bare `T a`

So it's the same type `a` all the way down, and therefore the same instance
for the constraint(s). Consider (adapted from the H98 Report for
DatatypeContexts):

    {-# LANGUAGE  GADTs    #-}

    data SetG a  where
      NilSetG  :: Eq a => SetG a
      ConsSetG :: Eq a => a -> SetG a -> SetG a

    sillySetG = undefined :: SetG (Int -> Int)           -- accepted, but
useless
--     sillySetG = NilSetG :: SetG (Int -> Int)            -- rejected no
Eq instance

(DatatypeContext's equiv with NilSet constructor at `(Int -> Int)` is
accepted, so some improvement.)

    elemSG x NilSetG                     = False
    elemSG x (ConsSetG y ys) | x == y    = True
                             | otherwise = elemSG x ys
      -- ===> elemSG :: a -> SetG a -> Bool                           -- no
Eq a inferred

The elem pattern matching test makes use of ConsSetG's Eq instance, but
doesn't expose that in the inferred type. Whereas:

    headS (ConsSetG x _) = x                             -- hide the
pattern match
    tailS (ConsSetG _ xs) = xs

    elemSh x NilSetG                     = False
    elemSh x yss        | x == headS yss = True
                        | otherwise      = elemSG x $ tailS yss
      -- ==> elemSh :: Eq a => a -> SetG a -> Bool                   -- Eq
a inferred

A 'morally equivalent' elem test but with a different inferred type,
exposing the `Eq a` constraint.

If you give an explicit signature for `elemSh`, you must specify `Eq a` --
which is annoying same as with DatatypeContexts; an explicit signature for
elemSG needn't -- which gives a more annoying imprecise type that'll get
reported at some usage site.

I'm concluding that for this use case, a GADT doesn't 'fix' all of the
stupidness with stupid theta.

AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200911/61d792fb/attachment-0001.html>