No. We can't use visible type application with Visible arguments. If they're 
Visible, then you don't need the @.

Ah yes.

How about
 * Required
 * Specified
 * Inferred

A Required argument is just that: it must be provided at all call sites. A 
Specified argument is one whose order we know about and can be given by visible 
type application. An Inferred argument is invented by GHC and cannot be 
affected by the user. With this phrasing, no word is an antonym of another.

I like that. Much more self-explanatory.   Shall we go for it?

Simon

From: Richard Eisenberg [mailto:[email protected]]
Sent: 23 June 2016 14:08
To: Simon Peyton Jones <[email protected]>
Cc: [email protected]
Subject: Re: isInvisible


On Jun 23, 2016, at 8:59 AM, Simon Peyton Jones 
<[email protected]<mailto:[email protected]>> wrote:


Richard
I have just spent an hour plumbing the torrid swamp of binder visibility.  
There is bad naming confusion.
We have

•         Visible

•         Specified

•         Invisible
The function isVisible returns True for Visible and False otherwise.  But 
isInvisible returns True for Invisible and Specified.  And partitionInvisibles, 
filterOutInvisibleTyVars, filterOutInvisibleTypes etc all treat Invisible and 
Specified the same.  That is, it’s really filterOutInvisibleOrSpecifiedTypes 
which is terribly clumsy.

Here is another design I considered:

> data VisibilityFlag
>   = Visible
>   | Invisible SpecifiedFlag
>
> data SpecifiedFlag = Specified | Inferred

That might make this all a bit clearer. I avoided this extra layer of 
indirection, though, as overly ornate. Perhaps I was wrong.

isVisible and isInvisible (the functions) are indeed opposites of each other. 
That's good, in my book. But it is confusing that Specified is lumped in with 
Invisible here.



Sometimes we need to pick up just the Inivisble args, and we don’t have a 
predicate for that (since isInvisible is taken), so you’ll see in 
Inst.top_instantiate we are reduced to saying (binderVisibility bndr == 
Invisible).
It’s all very smelly.  The trouble is that

•         In displayed types like (T a b), we display args that are Visible, 
but not Specified or Invisible

True.



•         In visible type application like (f @t1 @t2) we can specify type args 
that are Visible or Specified but not Invisible.

No. We can't use visible type application with Visible arguments. If they're 
Visible, then you don't need the @.



Urgh. The trouble is that “invisible” is not the negation of “visible”, which 
leads to all kinds of confusion.
I wonder about changing to

•         Explicit

•         Specified

•         Implicit
Then for display we display Explicit args only; for VTA we can specify Explicit 
or Specified args.
So “not Explicit” doesn’t sound structurally like “Implicit” in the way that 
“not Visible” does sound like “Invisible”.

I don't see the improvement here. "Invisible" and "visible" are antonyms, just 
like "implicit" and "explicit". Yes, it's true that "implicit" isn't just a 
prefix put on "explicit", but I hardly think that matters.

How about
 * Required
 * Specified
 * Inferred

A Required argument is just that: it must be provided at all call sites. A 
Specified argument is one whose order we know about and can be given by visible 
type application. An Inferred argument is invented by GHC and cannot be 
affected by the user. With this phrasing, no word is an antonym of another.

Richard


Simon

_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Reply via email to