[Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta
Viktor Dukhovni
ietf-dane at dukhovni.org
Fri Sep 11 08:08:54 UTC 2020
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.
More information about the Haskell-Cafe
mailing list