Re: [Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta
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
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.
On Fri, Sep 11, 2020 at 11:22 PM Anthony Clayden < anthony_clayden@clear.net.nz> 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 http://web.archive.org/web/20151001115936/http://code.haskell.org/~dons/hask... 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
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/hask... 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/hask... 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.
participants (2)
-
Anthony Clayden -
Viktor Dukhovni