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

[Joachim Breitner]

Hi,

Am Mittwoch, den 02.05.2018, 14:10 -0400 schrieb Richard Eisenberg:
> OK -- I could agree with forbidding braces on `data` (given that the
> GADT-syntax alternative exists), but what about `class`? And then if
> we allow it on `class`, it seems a bit silly not to do the analogous
> thing on `data`. (Note that the proposal currently describes the same
> scheme as I have described in this email thread, but only about
> `class`.)

Indeed, and the Unresolved questions go into some detail here.

It still is a bit weird to have `C {a}` affect _not_ C but _only_ the
methods, but since that is the only place where {a} appears, it is hard
to avoid.

Your solution for C is to say: Write a kind signature, i.e. if I write

   class C {k} (a : k) where meth :: a

and I want the {k} to be also inferred in C’s kind, I have to write

   type C :: forall {k}. k -> Constraint

By a similar reasoning one could expect the user, if they want to
change the specificity of meth, to write out the its full type
signature separately:

   class C k (a : k) where meth :: a
   meth :: forall {k} a. C k a -> k -> Constraint

This would even allow more fine-grained control: You get to choose for
each meth what the specificity is.


In a way, that is similar to Coq’s [Arguments] command, which changes
specificity after-the-fact. And we already have something similar in
Haskell: role annotations. So maybe another alternative is to say

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


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

Cheers,
Joachim
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180502/dc7ecbbf/attachment.sig>