[Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta
Anthony Clayden
anthony_clayden at clear.net.nz
Fri Sep 11 06:19:27 UTC 2020
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>
More information about the Haskell-Cafe
mailing list