New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TypeApplications for Overloaded Literals #129

Closed
wants to merge 12 commits into
base: master
from

Conversation

Projects
None yet
@isovector

isovector commented Apr 30, 2018

Rendered

Reddit discussion

Currently, types are unable to be applied to overloaded literals via TypeApplications. This proposal slightly changes the behavior of applied types in the presence of overloaded literals allowing us to do so.

@tathougies

This comment has been minimized.

tathougies commented Apr 30, 2018

How does (1 @a) differ from (1 :: a)?

@danidiaz

This comment has been minimized.

danidiaz commented Apr 30, 2018

One can also write something like id @Int 1 as a workaround.

@isovector

This comment has been minimized.

isovector commented Apr 30, 2018

@tathougies it doesn't, unless RebindableSyntax is on.

@ElvishJerricco

This comment has been minimized.

ElvishJerricco commented Apr 30, 2018

@tathougies Mainly precedence. @ binds at the precedence of function application IIRC, whereas :: must come after a complete expression. Doesn't seem hugely relevant for literals though, barring crazy instances like 1 @(Foo -> Bar) foo.

@tomjaguarpaw

This comment has been minimized.

Contributor

tomjaguarpaw commented Apr 30, 2018

Ouch, what a painfully subtle interaction between desugaring and type applications (in the status quo).

@shaylew

This comment has been minimized.

shaylew commented Apr 30, 2018

Some thoughts on fleshing out the integerLit :: Integer -> forall a. Num a => a alternative from Section 5 to work in the RebindableSyntax case:

What about continuing to use integerLit as long as the Prelude fromInteger is the one in scope? This keeps type applications to literals from breaking just because you turned on RebindableSyntax. Code that does rebind fromInteger would work as it does now -- which is to say, its fromInteger can be made to play nice with type applications to literals by putting the type parameter in the appropriate place just like integerLit does.

The upsides: this works in the (5) @Int case, and no existing code breaks. The downside: making your fromInteger work with type applications to literals wouldn't be automatic -- it would require changing its type signature slightly, which is usually simple but might be painful if the rebound fromInteger is a class method.

(Also possibly of note: the code that the main proposal breaks is precisely code that uses this fromInteger :: Integer -> forall a. whatever style.)

@simonpj

This comment has been minimized.

Contributor

simonpj commented Apr 30, 2018

Extending visible type application (e @type) to cover overloaded literals seems like a Good Thing to me.

I don't feel strongly about the details. I very much doubt that there is a single library that would be broken by any variant of the proposal. To break, it would have to

  • Use -XRebindableSyntax
  • Have an in-scope fromIntegral with a type like Integer -> forall a. blah
  • Use visible type application on a literal 4 @Int

So I'm not too bothered about breakage.

I can see the advantage of using parens to control how many type arguments are sucked into the fromInteger application. It cleverly uses a seldom-used facility (left-parenthesising an application) to exert control in a rare situation (when fromInteger has a forall to the right of the arrow. But it is a New Thing: usually left-parenthesising an application makes no difference.

@treeowl

This comment has been minimized.

Contributor

treeowl commented Apr 30, 2018

I very much prefer the integerLit alternative, with RebindableSyntax using integerLit if it's in scope and fromInteger otherwise. This seems to have the smallest impact on the language while still offering full flexibility.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Apr 30, 2018

I am mainly on board with

1 @a          desugars to   fromInteger @a        (1 :: Integer)

but I am less sure about the other, more complex examples and rules. Is this usecase of RebindableSyntax with a fromInteger function with more than one type variable where the user really has to instantiate further ones relevant?

Would this work: This proposal only adds

1 @a          desugars to   fromInteger @a        (1 :: Integer)

and users of RebindableSyntax are encouraged to write their

fromInteger :: forall a, Integer -> forall b c … 

i.e. follow the convention that there is exactly one type variable before the value parameter. This allows the user to write

1 @Ty1 @Ty2 @Ty3

and get

fromInteger @Ty1 (1::Integer) @Ty2 @Ty3
@treeowl

This comment has been minimized.

Contributor

treeowl commented Apr 30, 2018

Joachim's version looks pretty reasonable to me too.

@treeowl

This comment has been minimized.

Contributor

treeowl commented Apr 30, 2018

I thought of a point that might be worth considering in relation to this proposal (although it certainly would not be part of it). In heavily "dependent" code, I might actually want something very different from numeric literals. For example, I may want 2 on the RHS to be sing @2, using sing from singletons, and in a pattern to provide type evidence when matched, so I could write

f :: Sing n -> Maybe (n :~: 3)
f 3 = Just Refl
f _ = Nothing

Of course, it's possible that this notion will be subsumed by something much better when DependentHaskell is finished.

2 @a @b desugars to fromInteger @a @b (2 :: Integer)
3 @a ... @z desugars to fromInteger @a ... @z (3 :: Integer)
(3) @a desugars to fromInteger (4 :: Integer) @a
(4 @a) @b desugars to fromInteger @a (5 :: Integer) @b

This comment has been minimized.

@joehillen

joehillen May 1, 2018

The numbers are out of sync.

@cdsmith

This comment has been minimized.

cdsmith commented May 1, 2018

This seems like it shouldn't be controversial in general.

I'm curious whether anyone actually cares about the subtleties around RebindableSyntax? If not, and the strange behavior for (1) @a versus 1 @a weren't necessary, that would resolve what seems to be the biggest (if, perhaps, purely aesthetic) wart in the current proposal.

@isovector

This comment has been minimized.

isovector commented May 1, 2018

@nomeata @treeowl:

I'm somewhat opposed to desugaring only 1 @a. Relying on Integer -> forall a. ... for the RebindableSyntax case is annoying in that it requires workarounds to actually bind a as a ScopedTypeVariable. Also it feels rather ad-hoc to me -- why is only one type app privileged?

@treeowl

This comment has been minimized.

Contributor

treeowl commented May 1, 2018

@isovector, I prefer the integerLit approach myself, but mostly I want something conservative. Rearranging type variables based on parentheses doesn't really sit well with me.

@isovector

This comment has been minimized.

isovector commented May 1, 2018

@shaylew: Is your primary concern here the weird semantics around (5) @Int? There's nothing preventing us from entering brackets when performing the type-app desugaring, other than egregious backtracking in the case of adversarial syntax trees.

The primary driving factor behind the desugaring cases of 5 @Int vs (5) @Int was to support existing use cases of TypeApplications+RebindableSyntax+fromInteger :: Integer -> forall a. .... But if Simon isn't concerned about breaking these use cases (and, as best as I can tell, there are no actual use cases in existence), I'm not either.

Would you be happier with the current proposal implementation if ((((((((((5))) @Int))))))) @Double = 5 @Int @Double = fromInteger @Int @Double (5 :: Integer)?

@isovector

This comment has been minimized.

isovector commented May 1, 2018

@treeowl:

I very much prefer the integerLit alternative, with RebindableSyntax using integerLit if it's in scope and fromInteger otherwise. This seems to have the smallest impact on the language while still offering full flexibility.

Is the suggestion that RebindableSyntax desugar 5 as integerLit (5 :: Integer) iff integerLit is in scope, otherwise as fromInteger (5 :: Integer)? That strikes me as piling more on workarounds to work around the existing workarounds, but maybe you're seeing something I'm not.

@simonpj

This comment has been minimized.

Contributor

simonpj commented May 1, 2018

Is the suggestion that RebindableSyntax desugar 5 as integerLit (5 :: Integer) iff integerLit is in scope, otherwise as fromInteger (5 :: Integer)?

Yes, if alternatives are to be proposed, it'd be good for them to be well-specified. I agree that the `integerLit solution" isn't very satisfying.

Note too that we could remove the "special treatment for parens" part of the proposal altogether, and still have a very plausible proposal. (Move all the type-arguments to the left.)

@isovector

This comment has been minimized.

isovector commented May 1, 2018

@simonpj I'm in favor of that.

@shaylew

This comment has been minimized.

shaylew commented May 1, 2018

@isovector I was more or less just trying to flesh out the Alternatives section with the simplest possible answer to the "how does this work with RebindableSyntax" question, evaluating things in terms of the proposal's own mentioned benefits/costs/drawbacks which included the parentheses thing. I'm not personally super bothered by any answer to the parentheses question -- the choice is between "why do these extra parentheses break things" and "how do I force a type application to stay at the end", and neither situation seems bad enough to worry much about.

(To be 100% explicit, my "dumbest possible thing that works" concept was slightly dumber than @treeowl's. It would be for integerLit to only be used in place of Prelude.fromInteger -- so, when RebindableSyntax is off or fromInteger isn't being rebound . Nontrivial users of RebindableSyntax would be left to fend for themselves with exactly the existing behavior, on the grounds that unlike the Prelude they have the option to enweirden their fromInteger if they want. But I'm sold now on either the original proposal or the "move all type-arguments left" version, so this is really only here for completeness in case someone more conservative wants to run with it.)

@isovector

This comment has been minimized.

isovector commented May 1, 2018

Updated the proposal to remove the admittedly odd semantics behind parens. As of now, the proposal is to desugar all type applications on an overloaded literal, parens or no.

@treeowl

This comment has been minimized.

Contributor

treeowl commented May 1, 2018

I'm glad to be rid of the parenthesis rule, but I'm still a bit troubled by the proposal as it stands because it adds a little extra complexity where there's already lots of complexity. I'm also a tad concerned about DependentHaskell+RebindableSyntax interactions. Couldn't a foralled type depend on the value of the literal? In that case, couldn't pushing type applications to the left totally hose everything?

The precise alternative I suggest:

Define

integerLit :: Integer -> forall n. Num n => n
integerLit = fromInteger

When RebindableSyntax is not enabled:

Desugar 3 to integerLit 3.

When RebindableSyntax is enabled:

  1. If integerLit is in scope, desugar 3 to integerLit 3.
  2. If integerLit is not in scope, desugar 3 to fromInteger 3 and emit a warning.

Code currently using RebindableSyntax will work exactly the same as it does now. New (or updated) code using RebindableSyntax will define integerLit.

@isovector

This comment has been minimized.

isovector commented May 2, 2018

@treeowl Thanks for your thoughts. The DependentHaskell point is a valid one, but I don't have enough knowledge of the subject to have an informed opinion. @goldfirere -- mind weighing in?

I'm a little hesitant about desugaring to integerLit in that it directly contradicts the report.

It's starting to seem like perhaps the RebindableSyntax stuff isn't worth tackling in this proposal, based on a) nobody actually having complained about it, and b) the desired semantics being unclear. @treeowl would you support only reshuffling a single type variable onto a literal without the intergerLit machinery, so long as NoRebindableSyntax?

@treeowl

This comment has been minimized.

Contributor

treeowl commented May 2, 2018

There's no way to detect the difference from the Report without using non-standard features. So I don't see how it's relevant at all.

@isovector

This comment has been minimized.

isovector commented May 2, 2018

Fair enough. For completeness then, let's hammer out the rest of integerLit. Presumably we get one function per literal variety:

integerLit :: Integer -> forall a. Num a => a
fractionalLit :: Rational -> forall a. Fractional a => a

stringLit :: String -> forall a. IsString a => a
labelLit :: forall s a. IsLabel s => a  -- is this just fromLabel?
listLit :: [i] -> forall a. (IsList a, i ~ Item a) => a

Where should these definitions live? It seems reasonable for the last three to live in GHC.Exts, GHC.OverloadedLabels and GHC.Exts respectively, but the first two I'm less clear on.

Edit: this doesn't really matter if the RebindableSyntax doesn't actually target them.

@isovector

This comment has been minimized.

isovector commented May 2, 2018

I haven't had my coffee yet today, but it's not immediately obvious what we get out of desugaring to integerLit and friends in the case of RebindableSyntax, when the fromInteger in scope is not equal to Prelude.fromInteger.

It seems like we get our cake and can eat it too:

  • if NoRebindableSyntax, desugar 3 to integerLit 3
  • if RebindableSyntax and fromInteger = Prelude.fromInteger, desugar 3 to integerLit 3
  • otherwise desugar 3 to fromInteger 3

This can't break any code because the behavior is identical for people actually using rebindable literals, but gives us literal type apps for everyone else.

@isovector

This comment has been minimized.

isovector commented May 2, 2018

I had a go at implementing the integerLit solution and I must admit, it's significantly nicer than attempting to shuffle the type applications. Color me convinced -- I'll update the proposal with this solution. Thanks for your patience on this, @treeowl.

@shaylew just realized this is what you had proposed all along :) thanks to you too!

@isovector

This comment has been minimized.

isovector commented May 5, 2018

@nomeata ready for committee review!

@nomeata

This comment has been minimized.

Contributor

nomeata commented May 5, 2018

I was about to submit, but I guess there is still one open question. You write

This desugaring rule will only apply when NoRebindableSyntax is enabled, because type applications work as expected when syntax is rebound.

but that sounds like 5 @Int would break if I turn on RebindableSyntax. In your earlier comment you had a more complex rule that addresses it, but it seems it did not make it into the proposal. Was that intentional?

@nomeata

This comment has been minimized.

Contributor

nomeata commented May 6, 2018

Also, Richard points out that an idea that was floated on the steering committee mailing list could be used to give fromInteger the right type directly, without requiring the indirection via integerLit: https://mail.haskell.org/pipermail/ghc-steering-committee/2018-May/000542.html
This would completely avoid the complication of what to do with RebindableSyntax. Maybe this deserves to be discussed at least in the section ”Alternatives”?

@isovector

This comment has been minimized.

isovector commented May 6, 2018

Ah, sorry, this is me mixing implementation details with specification details. In the existing implementation of desugaring overlits, RebindableSyntax is only considered to be on if fromInteger /= Prelude.fromInteger, regardless of the flag being set or not. I'll update the proposal to describe the specification.

Thanks for bringing #99 to my attention. While it would help with the fromInteger case, it (nor the earlier idea of reshuffling type applications into witnesses) doesn't seem to be able to help type-applying NoOverloadedLists lists.

@nomeata

This comment has been minimized.

Contributor

nomeata commented on proposals/0000-type-apply-literals.rst in c3d3894 May 6, 2018

Typo? @Int

This comment has been minimized.

isovector replied May 6, 2018

good catch, thanks!

@cdsmith

This comment has been minimized.

cdsmith commented May 6, 2018

Just to be clear, does this mean that if RebindableSyntax is enabled, and fromInteger resolves to the default implementation, then the integerLit in the current scope is used? Or do you intend to choose one from GHC.Exts, leaving fromInteger as the right way to change integer literal syntax?

If the latter (which seems simpler), then wouldn't it be cleaner to just specify the desired behavior of type application on literals, and leave integerLit as merely an implementation detail?

@isovector

This comment has been minimized.

isovector commented May 6, 2018

The latter. Yes, integerLit and friends should be entirely implementation details.

@nomeata nomeata self-assigned this May 6, 2018

@nomeata

This comment has been minimized.

Contributor

nomeata commented May 14, 2018

Unfortunately, the committee found this proposal unconvincing: The motivation that :t 5 lets one believe that one can use TypeApplications here is not the full picture; only :t +v 5 lets you know if you can use type application: With -fprint-explicit-foralls,

λ> :t +v 5
5 :: forall {p}. Num p => p

The appearance of the braces in the output means that 5 is not available for visible type application (the variable p is inferred). So if there's any unexpected behavior in the current implementation, that's due to ill-informed expectations, not misbehavior.

Also, the the committee found that the proposal had to jump through too many hoops to get the desired effect, and that having to write (5 :: Int) instead of 5 @Int is not painful enough to warrant that.

It was pointed out that this idea might allow us to simply give fromInteger the right, shuffled type, which could be a way foward to having this feature without much ado.

In any case, thanks for your contributions!

@nomeata nomeata closed this May 14, 2018

@AntC2 AntC2 referenced this pull request Jun 21, 2018

Open

Top-level signatures #148

@bravit bravit added the Proposal label Nov 11, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment