GADT is not great - sometimes: can be almost as stupid as stupid theta
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
On Fri, Sep 11, 2020 at 06:19:27PM +1200, Anthony Clayden wrote:
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
This, as I am sure you're aware, is correct, but I'd also say unsurprising. The function indeed works for all `a`, it is just that for many `a` (those without an 'Eq' instance) the type `SetG a` is uninhabited, so the function is correct vacuously. I wouldn't describe this situation as there being something "stupid" with GADTs. The function is defined for all `a` and `SetG a`, even when `SetG a` is uninhabited. Once all the constructors imply the requisite constraints, the functions are automatically safe for all, possibly uninhabited, `SetG a` types. 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, ... And the constraints can be imposed on individual functions that actually test equality. Yes, with the deprecated `DatatypeContexts` the constraint does propagate to the use site (though one still needs to specify it explicitly, as with "unFoo" below), but there are still some anomalies: λ> :set -XFlexibleContexts λ> :set -XDatatypeContexts <no location info>: warning: -XDatatypeContexts is deprecated: ... λ> data (Eq a) => Foo a = Foo a deriving Show λ> unFoo :: Eq a => Foo a -> a; unFoo (Foo a) = a λ> let x = Foo id λ> unFoo x (1 :: Int) <interactive>:12:1: error: • No instance for (Eq (Int -> Int)) ... So, even with the constraint in place, we still got to define a (largely) uninhabited "x" term: x :: Eq (a -> a) => Foo (a -> a) x = Foo id Though of course one can arrange for a few special cases: instance Eq (() -> ()) where f == g = f () == g () instance Eq (Bool -> Bool) where f == g = f False == g False && f True == g True Which then allow: λ> unFoo x True True The same naturally extends to the GADT case: λ> let x = ConsSetG id NilSetG λ> elemSG (id :: Bool -> Bool) x -- Given above instance True λ> elemSG (id :: String -> String) x <interactive>:39:33: error: • No instance for (Eq (String -> String)) arising from a use of ‘x’ ... -- Viktor.
On Fri, Sep 11, 2020 at 6:19 PM Anthony Clayden < anthony_clayden@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... 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
participants (2)
-
Anthony Clayden -
Viktor Dukhovni