Skip to content
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

Change in terminology for typelevel methods #4927

Merged
merged 11 commits into from Aug 27, 2018

Conversation

@odersky
Copy link
Contributor

odersky commented Aug 10, 2018

This PR changes the typelevel.md spec, renaming transparent to rewrite.

  • also, introduce rewrite as a modifier for match expressions and conditionals.
  • keep transparent for methods that are not erased, and don't inline by themselves, yet can be inlined from rewritten code.

It's hopefully clearer this way. Also, rewrite on conditonals and matches, while being more verbose makes their use more compositional. This PR is based on #4916.

Copy link

dotty-bot left a comment

Hello, and thank you for opening this PR! 🎉

All contributors have signed the CLA, thank you! ❤️

Commit Messages

We want to keep history, but for that to actually be useful we have
some rules on how to format our commit messages (relevant xkcd).

Please stick to these guidelines for commit messages:

  1. Separate subject from body with a blank line
  2. When fixing an issue, start your commit message with Fix #<ISSUE-NBR>:
  3. Limit the subject line to 72 characters
  4. Capitalize the subject line
  5. Do not end the subject line with a period
  6. Use the imperative mood in the subject line ("Add" instead of "Added")
  7. Wrap the body at 80 characters
  8. Use the body to explain what and why vs. how

adapted from https://chris.beams.io/posts/git-commit

Have an awesome day! ☀️

@odersky odersky force-pushed the dotty-staging:change-rewrite branch from 327ae1c to f951c6b Aug 12, 2018
@milessabin

This comment has been minimized.

Copy link
Contributor

milessabin commented Aug 12, 2018

I worry slightly that using rewrite here will be confused with the tactics of the same name you find in Agda, Idris, Coq etc.

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Aug 12, 2018

I worry slightly that using rewrite here will be confused with the tactics of the same name you find in Agda, Idris, Coq etc.

Bit it's sort of equivalent: You tell the compiler to rewrite the source program according to the rules that are specified.

@milessabin

This comment has been minimized.

Copy link
Contributor

milessabin commented Aug 13, 2018

Bit it's sort of equivalent

I think that's the problem ... it's close enough to cause confusion.

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Aug 13, 2018

I think that's the problem ... it's close enough to cause confusion.

Do you have a suggestion for another term to use? We want something that marks both definitions and match and if expressions. rewrite seems to capture the meaning nicely. I was thinking about reduce for a moment but that's not as clear for non-experts.

@milessabin

This comment has been minimized.

Copy link
Contributor

milessabin commented Aug 13, 2018

My understanding of the terminology in Agda/Idris/Coq, etc. is that rewrite is a specific tactic, and that in general tactics are deduction rules for backwards reasoning, from a goal to a set of prior subgoals (see eg. the introduction here: https://coq.inria.fr/refman/proof-engine/tactics.html).

I think that the backwards reasoning aspect fits implicit search extremely well, and I can imagine that if we developed the idea of a tactic language for Scala it would be closely aligned with implicit search. In particular I can imagine putting together a rewrite tactic, similar to the Agda/Idris/Coq rewrite, as one or more transparent implicit methods.

I think that what you're trying to get to here is a label for forwards reasoning, from premises (arguments/scrutinees) to conclusions (result/match RHS).

I think we're definitely in the same sort of area, but I don't think we have the terminology quite right yet.

I'll try and come up with something better.

@milessabin

This comment has been minimized.

Copy link
Contributor

milessabin commented Aug 13, 2018

Chatting with @Blaisorblade about this a little, we're both of the opinion (correct me if I'm misrepresenting you @Blaisorblade) that this is in effect a staging annotation.

If that's the case, then perhaps we should try and relate the syntax here to the metaprogramming syntax? How about reusing ~? That would give us things like,

~ def concat[A, M, N](xs: Vec[A, M], ys: A[A, N])(implicit ev: Add[M, N]): Vec[A, ev.Result]

~ type Add[M <: Nat, N <: Nat] <: Nat = type M match {
  case Z => N
  case S[type M1] => S[Add[M1, N]]
}

It also takes this,

rewrite def m(x: T) = ~mImpl('x)
...
def mImpl(x: Expr[T]) = ...

to this,

~ def m(x: T) = ~mImpl('x)
...
def mImpl(x: Expr[T]) = ...

which I think is quite suggestive ... the compile time nature of the RHS is mirrored on the LHS.

As an added bonus this doesn't require another new keyword, and ~ sort of suggests something a little reduction like, to me at least ... I've seen ~> used to express "reduces to" for instance.

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Aug 14, 2018

There sure are analogies between rewrite and macro splicing, but there are also differences. Splice ~ is of type Expr[T] => T. So if we wanted to use ~ for a rewrite match, we'd have to quote the returned values, like this:

~ def size(xs: Tuple): Int = ~ xs match {
    case _: Empty => '0
    case _: (_ *: xs1) => 'size(erasedValue[xs1]) + 1
}

(That's actually the model I started with 6 months ago). But I now believe using rewrite or inline, or whatever, is clearer.

There's also the difference that ~ does not produce new types, but rewrite can.

Finally, there's the difference that once I splice a function call, like ~mImpl(...) it is assumed that mImpl will run to completion until it returns a value (of type Expr[T]). Under a reduction model this means transitively reducing everything mImpl calls. rewrite does not behave like this. It will inline only other rewrite functions, perform some selected simplifications and return the result (which is still a term in general, not a value).

So I fear merging rewrite and ~ would be more confusing than simplifying.

@milessabin

This comment has been minimized.

Copy link
Contributor

milessabin commented Aug 14, 2018

I wasn't proposing changing the semantics, just using the token ~ in place of transparent/rewrite/inline.

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Aug 14, 2018

I wasn't proposing changing the semantics, just using the token ~ in place of transparent/rewrite/inline.

That's what I assumed. My worry is that using ~ for rewrite will be confusing because the two have really different semantics.

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Aug 14, 2018

Regarding usage of rewrite I am actually not so worried about the specific usage in Coq or Agda. The term "rewrite rules" is used more broadly than that. Rewrite rules also exist in Haskell (where they go forward), and more generally in term rewriting systems. Our rewrite rules are admittedly very simplistic in that they take a single function call as left-hand-side. But they do fit the definition of rewriting from term rewriting systems.

@milessabin

This comment has been minimized.

Copy link
Contributor

milessabin commented Aug 14, 2018

Rewrite rules also exist in Haskell (where they go forward)

Fair enough.

@ctongfei

This comment has been minimized.

Copy link

ctongfei commented Aug 14, 2018

Since rewrite is a verb, it may corrupt some code if it is used as a keyword. Since it mostly supplants inline, I guess that inline is a better choice? (inline is a keyword in a bunch of languages so people don't usually use it for identifiers)

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Aug 15, 2018

@ctongfei I am not against inline but it would bring us back full circle. inline was dropped because people argued that it would be inappropriate for something that could change types. In other words, inline is just an advisory that should neither change types nor semantics.

rewrite makes that aspect fully explicit, but it's true that it will break code (easy to rewrite automatically by inserting backquotes, though).

@ctongfei

This comment has been minimized.

Copy link

ctongfei commented Aug 15, 2018

@odersky OK I got it. Maybe rewriting would be better (an adjective, similar to transparent/inline, and less likely to be used as an identifier)?

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Aug 17, 2018

It's a big commit. Who volunteers for reviewing?

@liufengyun liufengyun requested a review from nicolasstucki Aug 20, 2018
@liufengyun liufengyun requested a review from OlivierBlanvillain Aug 20, 2018
@odersky odersky force-pushed the dotty-staging:change-rewrite branch from 0480620 to 6a86f99 Aug 22, 2018
Copy link
Contributor

nicolasstucki left a comment

Otherwise LGTM

@@ -2519,6 +2543,8 @@ object Parsers {
stats +++= defOrDcl(in.offset, defAnnotsMods(modifierTokens))
else if (!isStatSep) {
exitOnError = mustStartStat
println(in.token)
println(in.next.token)

This comment has been minimized.

Copy link
@nicolasstucki

nicolasstucki Aug 27, 2018

Contributor

Should remove these two lines

@nicolasstucki

This comment has been minimized.

Copy link
Contributor

nicolasstucki commented Aug 27, 2018

@odersky this PR needs a rebase

odersky added 4 commits Aug 10, 2018
 - also, introduce `rewrite` as a modifier for match expressions
   and conditionals.
 - keep `transparent` for methods that are not erased, and don't inline
   by themselves, yet can be inlined from rewritten code.
Also implements rewrite matches and rewrite ifs. Keeps transparent as a separate
modifier with meaning: "inline if called from a rewrite context".
erased can only override erased, non-erased can only override non-erased.
odersky added 2 commits Aug 13, 2018
...in new code added through rebase
@odersky odersky force-pushed the dotty-staging:change-rewrite branch from 8a13d19 to bbe88d1 Aug 27, 2018
odersky added 4 commits Aug 27, 2018
@odersky odersky merged commit 973b675 into lampepfl:master Aug 27, 2018
2 checks passed
2 checks passed
CLA User signed CLA
Details
continuous-integration/drone/pr the build was successful
Details
@Blaisorblade Blaisorblade deleted the dotty-staging:change-rewrite branch Aug 27, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
7 participants
You can’t perform that action at this time.