[Haskell-cafe] 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.