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.