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

[Anthony Clayden]

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

>
> 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
>
>
>     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
>
>
>
It seems you can get there with PatternSynonyms, using an explicit
signature with 'required' constraints:
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms

    pattern ConsSetPS x yss = ConsSetG x yss
    -- inferred pattern ConsSetPS :: () => Eq a => a -> SetP a -> SetP a
 -- that is, if no sig given

Using `ConsSetPS` as the pattern in `elemSG` with that default/inferred
signature gives the same typing as using the GADT constructor. But with
explicit signature

    pattern ConsSetPS :: Eq a => a -> SetG a -> SetG a
    --                      longhand :: Eq a => () => a -> SetG a -> SetG a

The 'required' `Eq a` is exposed, so `elemSG` gets the same signature as
`elemSh` above.

After all, if you're trying to maintain an invariant, you'd be using a
PatternSynonym as 'smart constructor' to validate uniqueness; so giving it
a signature (and hiding the GADT constructor) is easy enough.

Would be nice to be able to give pattern-style signatures for GADT
constructors. Unfortunately, the sigs for `ConsSetG` and `ConsSetPS` look
the same but mean the opposite way round.


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