GADT is not great - sometimes: can be almost as stupid as stupid theta

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

GADT is not great - sometimes: can be almost as stupid as stupid theta

AntC
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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: GADT is not great - sometimes: can be almost as stupid as stupid theta

Viktor Dukhovni
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.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: GADT is not great - sometimes: can be almost as stupid as stupid theta

AntC
In reply to this post by AntC
> On  Fri Sep 11 08:08:54 UTC 2020,  Viktor Dukhovni wrote:
This, as I am sure you're aware, is correct,

Hmm. If you mean 'working as per spec' (the OutsideIn paper), then OK.

> 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.

On the basis that 'well-typed programs can't go wrong'; it allows a well-typed program that crashes. That's not correct. And it's not vacuous: `elemSG` matches on constructor; the only value of `sillySG`'s type is bottom -- i.e. no constructor. I can compile

sillyElem = elemSG (id :: Int -> Int) sillySetG      -- inferred type Bool

Why is that not ill-typed, in the absence of an instance `Eq (Int -> Int)` ?

Running that crashes *** Exception: Prelude.undefined. Whereas `elemSh (id :: Int -> Int) sillySetG` is not well-typed. I could of course specify a signature for `elemSG` with explicit `Eq a =>`, but needing to do that is exactly what people complain of with DatatypeContexts.

I wouldn't describe this situation as there being something "stupid" with GADTs.

To be clear: I'm not saying there's something as stupid as with DatatypeContexts. I am saying there's a family of use-cases for which GADTs are not a good fit.

The example you show using DatatypeContexts fails to compile `No instance for (Eq (Int -> Int))`, which is entirely reasonable; it does compile if supplied an instance, as you go on to show.

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, ...

No. Missing out the constraints is a craven surrender to the limitations in Haskell. Signatures/constraints should give maximum help to the compiler to accept only well-behaved programs.

That limitation is because Functor, Applicative, etc are trying to keep backwards compatibility with H98 Prelude. One approach would be for their methods to have a signature with a type family defined constraint.

Or the 'Partial Type Constructors' paper shows a possible approach -- which is really orthogonal to its main topic.

AntC

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: GADT is not great - sometimes: can be almost as stupid as stupid theta

Viktor Dukhovni
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
>
>     sillySetG = undefined :: SetG (Int -> Int)  -- accepted, but useless
> --  sillySetG = NilSetG :: SetG (Int -> Int)    -- rejected no Eq instance

But is it any surprise that placing bottom in an uninhabited type, and
then later using it runs into a runtime crash?  That seems a rather
contrived problem.


On Fri, Sep 11, 2020 at 11:22:26PM +1200, Anthony Clayden wrote:

> > 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.
>
> On the basis that 'well-typed programs can't go wrong'; it allows a
> well-typed program that crashes. That's not correct. And it's not
> vacuous: `elemSG` matches on constructor; the only value of
> `sillySG`'s type is bottom -- i.e. no constructor. I can compile

Well, but well typed programs do go wrong when you use `undefined`,
`error`, `absurd`, 1 `div` 0, ...  How is this case different?

> sillyElem = elemSG (id :: Int -> Int) sillySetG      -- inferred type Bool

Bit sillySetG is bottom.  Sure you did not get a type error, but the
same thing would compile and crash even if the type were `Int`
rather than `Int -> Int`, and the constraints were enforced.

> Why is that not ill-typed, in the absence of an instance `Eq (Int -> Int)` ?

Because the functions in question are defined for all types!  Vacuously
for those `a` where `SetG a` is uninhabited (by anything other than
bottom.  The type of `sillySetG` is only inhabited when the constraint
`Eq (Int -> Int)` holds.  Going outside to sound part of the type system
by using bottom makes the logic unsound.  Is that really a problem?

> Running that crashes *** Exception: Prelude.undefined. Whereas `elemSh (id
> :: Int -> Int) sillySetG` is not well-typed.

But it is manifestly well-typed!  We have a proof of this fact in the
form of a total function definition mapping the input type to the output
type for all (non-bottom) inputs.  (Total functions are under no
obligation to not crash on bottom).

> To be clear: I'm not saying there's something as stupid as with
> DatatypeContexts. I am saying there's a family of use-cases for which GADTs
> are not a good fit.

I don't think that Haskell offers type safety that survives placing
bottom in otherwise uninhabited types and then evaluating them strictly.
Non-strict evaluation works fine.  The below well-typed program

    {-# LANGUAGE NoStrictData #-}
    {-# LANGUAGE GADTs #-}
    module Main (main) where

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

        sillySetG = undefined :: SetG (a -> a)

        data Y a = Y { y :: a } deriving Show

        lazyUpdate :: Y (SetG (Int -> Int)) -> a -> Y a
        lazyUpdate r a = r { y = a }

        defaultY :: Y (SetG (a -> a))
        defaultY = Y { y = sillySetG }

        main :: IO ()
        main = print $ lazyUpdate defaultY "c"

prints: Y {y = "c"}.  The fact that it runs to completion shows it
is well typed.

> The example you show using DatatypeContexts fails to compile `No instance
> for (Eq (Int -> Int))`, which is entirely reasonable; it does compile if
> supplied an instance, as you go on to show.

Yes, you can gate the constructors, either with the deprecated
DatatypeContexts, or with GADTs.  But the former does not buy you any
new type safety.  Ill-typed programs don't compile either way.

> > 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, ...
>
> No. Missing out the constraints is a craven surrender to the limitations in
> Haskell. Signatures/constraints should give maximum help to the compiler to
> accept only well-behaved programs.

I don't agree that your example is ill-typed.  The only misbehaving term
you are able to introduce is bottom, and its use surely rules out all
expectations of safe behaviour.

> That limitation is because Functor, Applicative, etc are trying to keep
> backwards compatibility with H98 Prelude. One approach would be for their
> methods to have a signature with a type family defined constraint.
>
> Or the 'Partial Type Constructors' paper shows a possible approach -- which
> is really orthogonal to its main topic.

Ah, an fmap that respects value constraints by limiting the co-domain of
allowed functions is an interesting proposition.  And in that
(non-Haskell) case indeed the constraints would have less of a downside.

Meanwhile, the GADT program *is* well typed, it just allows more
uninhabited types than would be the case DatatypeContexts, but in the
end the exposure to runtime errors with bottom is I think the same,
(or I've not yet seen the compelling counter-example).

--
    Viktor.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: GADT is not great - sometimes: can be almost as stupid as stupid theta

AntC
In reply to this post by AntC

On Fri, Sep 11, 2020 at 11:22 PM Anthony Clayden <[hidden email]> wrote:
> On  Fri Sep 11 08:08:54 UTC 2020,  Viktor Dukhovni wrote:

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, ...


No that isn't going to work. As Phil Wadler says here
what's really going on is that we want some invariant to hold over the data structure. A set's elements must be unique; so we need `Eq` to be able to test that; but `Eq` alone doesn't capture the whole invariant.

So take an instance for Functor Set: `fmap` is to apply some arbitrary function to the elements of the set; there's no guarantee that the values returned will still be unique after applying the function. (Indeed there's no guarantee the function's return type is in `Eq`.) Then we need something within the overloading for `fmap` that will check uniqueness; and that'll need an `Eq` constraint.

Or you decorate every call to those constructor classes/methods with post-processing to fix up the mess. Which obfuscates the logic in your elegant pointfree style.
 
Or the 'Partial Type Constructors' paper shows a possible approach -- which is really orthogonal to its main topic.


That paper picks up on a paper from John Hughes 1999, which is tackling exactly the same requirements.
 
AntC

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: GADT is not great - sometimes: can be almost as stupid as stupid theta

Viktor Dukhovni
On Mon, Sep 14, 2020 at 01:00:40PM +1200, Anthony Clayden wrote:

> No that isn't going to work. As Phil Wadler says here
> http://web.archive.org/web/20151001115936/http://code.haskell.org/~dons/haskell-1990-2000/msg04062.html
> what's really going on is that we want some invariant to hold over the data
> structure. A set's elements must be unique; so we need `Eq` to be able to
> test that; but `Eq` alone doesn't capture the whole invariant.

Thanks for that reference.  I guess that puts retroactively on Simon's
side, and perhaps in alignment with:

    http://web.archive.org/web/20151001182427/http://code.haskell.org/~dons/haskell-1990-2000/msg04073.html

from the same thread.

> So take an instance for Functor Set: `fmap` is to apply some arbitrary
> function to the elements of the set; there's no guarantee that the values
> returned will still be unique after applying the function. (Indeed there's
> no guarantee the function's return type is in `Eq`.) Then we need something
> within the overloading for `fmap` that will check uniqueness; and that'll
> need an `Eq` constraint.

Yes, "fmap" is not good fit for Set.  And indeed with the GADT
constructor constraint, there's no way to define it for non-empty sets,
since the constraint cannot be met under general conditions.

A restricted fmap that only allowed maps between types that support
equality, could be defined, but much is lost, since Applicative would
not be available, for lack of equality on arrows.

With the explicit equality operator representation:

    data Set a = MkSet [a] (EqOper a)

a function (Set a) -> (Set b) would have to provide not only a pointwise
mapping, but also an explicit (EqOper b):

    f :: Set SomeA -> Set SomeB
    f (MkSet a eqA) = MkSet (g a) eqB

where sanity also requires (but difficult to check in general)
that: eqA a1 a2 `implies` eqB (g a1) (g a2).

That is, `g` has to respect the `eqA` equivalence classes, something
we'd like to expect from e.g. `Eq` instances, but again cannot in
general check.

--
    Viktor.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: GADT is not great - sometimes: can be almost as stupid as stupid theta

AntC
In reply to this post by AntC

On Fri, Sep 11, 2020 at 6:19 PM Anthony Clayden <[hidden email]> 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:

    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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.