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

[Iavor Diatchki]

Hello,

I just re-read the proposal and I am a bit unclear:  are we proposing that
we make this change only in type signatures or in all places where we bind
type variables?  At first I thought we are talking only about type
signatures, but I noticed that the proposal seems to mention type classes,
but not `data` declarations or type families.  I find the "implicit" hidden
parameters in those to be one of the most confusing features of GHC, so
having a way to write those would certainly be useful.  I do have some
clarifying questions illustrated by the examples below (assuming that this
extension should work on `data`):

-- 1) The "normal" case.  I've written the types of the introduces names
underneath, are they correct?
data T1 {k} (a :: k) = C1
-- T1 :: forall {k::Type}. k -> Type
-- C1 :: forall {k::Type} (a :: k). T1 {k} a
-- Am I correct in assuming that while GHC could print the types like that,
but users are not allowed to actually write those types (i.e., `T1 {k}
(a::k)` is not a valid type).

-- 2) Can GHC add extra inferred parameters? (This examples assumes
`PolyKinds`)
data T2 {k} a = C2
-- C2 :: forall {k1::Type} {k::Type} (a :: k1). T2 {k1} {k} a   (ambiguous?)

-- 3) Can we infer non-kind types?
data T3 {a} = C3 a
-- C3 :: forall {a::Type}. a -> T3 {a}

-- 4) If `T3` is OK, how does "inferring" work in signatures? To make
things concrete, would the following be accepted?
f :: T3
f = C3 True
-- A): not, because the signature is really: `forall {a}. T3 {a}`.
-- B): yes, because we are going to infer that the missing type is `Bool`,
so the signature becomes `T3 {Bool}`.

-- 5) The proposal has a class, something like this:
class C a {b} where
  meth1 :: a -> b

-- How do I write an instance for this class?
-- A)
instance C Int where
    meth1 x = x

-- B)
instance C Int {Int} where
    meth1 x = x

I imagine the answer is A) is I see nothing about writing types like
`{Int}`.  If so, here are a couple of follow up questions about instances:

-- Valid?
instance C Int where
    meth1 x = []
-- instance is really `forall {a::Type}. C Int {[a]}` ?

instance C Int where
    meth1 x = return x
--- error, instance is `C Int {m Int}`, but no `Monad` constraint.
-- There doesn't seem to be a way to write the instance with the constraint?

Sorry for the long e-mail, but I hope that these examples might bring some
clarity to users of the proposed feature.

-Iavor



On Tue, May 1, 2018 at 3:55 AM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> [Redirecting to the steering committee]
>
>
>
> I argue for acceptance.
>
>
>
>    - For me a compelling motivation is this: at the moment *we can infer
>    types and kinds that we cannot write down with an explicitly-quantified
>    type signature*.  That seems all wrong to me: we should be able to
>    write down any type you can infer.
>    - The proposal adds *notation*.  It does *not* add semantics.  We
>    already have the distinction between “inferred” and “specified” type
>    variables.  You might not like it, but it’s there in GHC.
>       - If it wasn’t there already, I’d be happy to debate not adding
>       it.
>       - If you want to argue for removing the distinction, that would
>       certainly render the current proposal moot.  But that would take a GHC
>       proposal – and there are good reasons for the status quo!
>       - What is bad is to maintain the semantic distinction, but be
>       unable to express it.  That’s what we have right now, and it’s a bad thing.
>
>
>
> What is the distinction between “specified” and “inferred”?
>
>    - *Specified.   f :: forall a. blah, or   f :: a -> a.*
>
> You may give a visible type argument at a call of f, but you do not have
> to.  Thus  (f x) or (f @type x).
>
>
>
>    - *Inferred*.  *f :: t a -> t a.*  The type of f is really
>
> g :: forall {k} (t :: k -> *) (a :: k). t a -> t a
>
> Note that k does not appear at all in the signature; that’s why it is
> “inferred”.  In GHC today you cannot supply an explicit kind argument for
> g, but you can supply explicit argument for t and a.
>
>
>
> So by all means make the case for abolishing the distinction, to render
> the present proposal moot.  But I think it’s unreasonably simply to reject
> on the grounds of “please think of something better”.
>
>
>
> Simon
>
>
>
> *From:* ghc-devs <ghc-devs-bounces at haskell.org> *On Behalf Of *Iavor
> Diatchki
> *Sent:* 30 April 2018 17:12
> *To:* ghc-devs at haskell.org
> *Subject:* Discussion on proposal #99: forall {k}
>
>
>
> Hello,
>
>
>
> As a shepherd for proposal #99, I'd like to kick off the discussion.  The
> full proposal is available here:
> https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/proposals/0000-explicit-specificity.rst
>
>
>
> Summary: allows programmers to write `forall {x}` instead of `forall x` in
> type signatures.  The meaning of the braces is that this parameter cannot
> be instantiated with an explicit type application and will always be
> inferred.  The motivation is to shorten explicit type applications by
> skipping parameters that are known to be inferable, the common example
> being omitting the kinds in signatures with poly kinds.
>
>
>
> As I understand it, the main motivation for this proposals is to give
> programmers more flexibility when instantiating type variables, with a less
> noisy syntax.   While the proposed solution might work in some situations,
> I am unconvinced that it is the best way to address the issue in general,
> for the following reasons:
>
>
>
>   1. It requires that programmers commit at declaration time about which
> arguments will be inferred, and which may be inferred or specified.   While
> in some cases this may be an easy decision to make, in many cases this
> really is a decision which should be made at the use site of a function
> (e.g., I'd like to provide argument X, but would like GHC to infer argument
> Y).
>
>
>
>   2. It still requires that programmers instantiate arguments in a fixed
> order,  which is sometimes dictated by the structure of the type itslef.
> Here is, for example, what the proposal suggests to do if you want to
> provide type before a kind:
>
>
>
>     typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a
>
>
>
>     While technically this is not wrong, it is not exactly elegant.
>
>
>
> I think that we should reject this proposal, and try to come up with a
> more comprehensive solution to the problem.
>
>
>
> One alternative design is to allow programmers to instantiate type
> variables by name.  This is much more flexible as it allows programmers to
> instantiate whichever variables they want, and in whatever order.  We've
> been doing this in Cryptol for a long time, and it seems to work really
> well.
>
>
>
> -Iavor
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180501/d9a2be6f/attachment.html>