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: 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. |
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. |
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. |
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. |
In reply to this post by AntC
On Fri, Sep 11, 2020 at 11:22 PM Anthony Clayden <[hidden email]> wrote:
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.
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. |
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. |
In reply to this post by AntC
On Fri, Sep 11, 2020 at 6:19 PM Anthony Clayden <[hidden email]> wrote:
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. |
Free forum by Nabble | Edit this page |