[ghc-steering-committee] Discussion on proposal #99: forall {k}

[Richard Eisenberg]

Joachim, you are always a fount of interesting ideas.

> On May 2, 2018, at 2:51 PM, Joachim Breitner <mail at joachim-breitner.de> wrote:
> 
>   class C k (a : k) where meth :: a
>   meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this:

class Num a where
  fromInteger :: Integer -> a

fromInteger :: Integer -> forall a. Num a => a

If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.)

This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it.

And it allows for updated types (including quantified variable ordering, etc.) for record selectors.

And it allows (maybe?) for giving good types to GADT record selectors:

data X a where
  Foo :: { bar :: Int } -> X Int
  Quux :: { bar :: Bool } -> X Bool
bar :: X a -> a

GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy.

GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

>   class C k (a : k) where meth :: a
>   specificity meth inferred specified

This is also quite interesting. Syntax for role annotations started out very terse, and written inline with datatype declarations. Over time, we recognized that it was more ergonomic to separate them from the declarations. One reason for this was to ease the transition period and requisite CPP clutter.

I still prefer your first suggestion here more because it seems to have greater applicability.

> 
> 
> (The rambliness of this mail is an indication that the proposal does
> not immediately resonates as the obvious right and best solution with
> me…)

I agree, and so I'm pleased with this debate.

Richard

> 
> Cheers,
> Joachim
> -- 
> Joachim Breitner
>  mail at joachim-breitner.de
>  http://www.joachim-breitner.de/
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee