Change in terminology for typelevel methods #4927

odersky · 2018-08-10T18:09:38Z

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.

dottybot

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:

Separate subject from body with a blank line

When fixing an issue, start your commit message with Fix #<ISSUE-NBR>:

Limit the subject line to 72 characters

Capitalize the subject line

Do not end the subject line with a period

Use the imperative mood in the subject line ("Add" instead of "Added")

Wrap the body at 80 characters

Use the body to explain what and why vs. how

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

Have an awesome day! ☀️

milessabin · 2018-08-12T19:08:13Z

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 · 2018-08-12T20:24:35Z

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 · 2018-08-13T07:06:11Z

Bit it's sort of equivalent

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

odersky · 2018-08-13T08:23:50Z

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 · 2018-08-13T16:31:15Z

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 · 2018-08-13T22:18:05Z

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 · 2018-08-14T09:05:08Z

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 · 2018-08-14T09:07:31Z

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

odersky · 2018-08-14T09:22:17Z

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 · 2018-08-14T09:28:22Z

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 · 2018-08-14T10:30:22Z

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

Fair enough.

ctongfei · 2018-08-14T23:18:42Z

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 · 2018-08-15T17:15:07Z

@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 · 2018-08-15T20:17:41Z

@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 · 2018-08-17T14:29:56Z

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

nicolasstucki

Otherwise LGTM

nicolasstucki · 2018-08-27T07:44:47Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

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


Should remove these two lines

nicolasstucki · 2018-08-27T07:48:55Z

@odersky this PR needs a rebase

- 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.

...in new code added through rebase

dottybot reviewed Aug 10, 2018

View reviewed changes

odersky mentioned this pull request Aug 10, 2018

Decouple transparent and erased properties #4860

Closed

odersky force-pushed the change-rewrite branch from 327ae1c to f951c6b Compare August 12, 2018 18:27

odersky mentioned this pull request Aug 13, 2018

Add support for generic tuples #4938

Merged

liufengyun assigned nicolasstucki Aug 20, 2018

liufengyun requested a review from nicolasstucki August 20, 2018 14:29

liufengyun assigned OlivierBlanvillain Aug 20, 2018

liufengyun requested a review from OlivierBlanvillain August 20, 2018 14:29

odersky force-pushed the change-rewrite branch from 0480620 to 6a86f99 Compare August 22, 2018 15:57

nicolasstucki approved these changes Aug 27, 2018

View reviewed changes

odersky added 4 commits August 27, 2018 14:23

Change spec, renaming transparent to rewrite.

5e76c82

- 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.

Rename transparent methods -> rewrite methods

ccc7845

Also implements rewrite matches and rewrite ifs. Keeps transparent as a separate modifier with meaning: "inline if called from a rewrite context".

Fix test

f697eb0

Change overriding rule for erased values

e48a9c7

erased can only override erased, non-erased can only override non-erased.

odersky added 2 commits August 27, 2018 14:24

Change test to use non-toplevel rewrite match

aa96f35

Fix transparent -> rewrite

bbe88d1

...in new code added through rebase

odersky force-pushed the change-rewrite branch from 8a13d19 to bbe88d1 Compare August 27, 2018 12:25

odersky added 4 commits August 27, 2018 14:27

Drop debug printlns

df8293a

Fix tests

076a5dd

Fix more tests

739efdb

Fix even more tests

006f9ef

Blaisorblade added the stat:needs rebase label Aug 27, 2018

Fix yet another test

6ab608e

odersky merged commit 973b675 into scala:master Aug 27, 2018

Blaisorblade deleted the change-rewrite branch August 27, 2018 17:05

Blaisorblade removed the stat:needs rebase label Aug 27, 2018

odersky mentioned this pull request Sep 6, 2018

Choose Primitives for Typelevel and Meta Programming in Scala 3.0 #5086

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Change in terminology for typelevel methods #4927

Change in terminology for typelevel methods #4927

odersky commented Aug 10, 2018 •

edited

Loading

dottybot left a comment

milessabin commented Aug 12, 2018

odersky commented Aug 12, 2018

milessabin commented Aug 13, 2018

odersky commented Aug 13, 2018

milessabin commented Aug 13, 2018

milessabin commented Aug 13, 2018

odersky commented Aug 14, 2018

milessabin commented Aug 14, 2018

odersky commented Aug 14, 2018

odersky commented Aug 14, 2018

milessabin commented Aug 14, 2018

ctongfei commented Aug 14, 2018

odersky commented Aug 15, 2018 •

edited

Loading

ctongfei commented Aug 15, 2018

odersky commented Aug 17, 2018

nicolasstucki left a comment

nicolasstucki Aug 27, 2018

nicolasstucki commented Aug 27, 2018

Change in terminology for typelevel methods #4927

Change in terminology for typelevel methods #4927

Conversation

odersky commented Aug 10, 2018 • edited Loading

dottybot left a comment

Choose a reason for hiding this comment

Commit Messages

milessabin commented Aug 12, 2018

odersky commented Aug 12, 2018

milessabin commented Aug 13, 2018

odersky commented Aug 13, 2018

milessabin commented Aug 13, 2018

milessabin commented Aug 13, 2018

odersky commented Aug 14, 2018

milessabin commented Aug 14, 2018

odersky commented Aug 14, 2018

odersky commented Aug 14, 2018

milessabin commented Aug 14, 2018

ctongfei commented Aug 14, 2018

odersky commented Aug 15, 2018 • edited Loading

ctongfei commented Aug 15, 2018

odersky commented Aug 17, 2018

nicolasstucki left a comment

Choose a reason for hiding this comment

nicolasstucki Aug 27, 2018

Choose a reason for hiding this comment

nicolasstucki commented Aug 27, 2018

odersky commented Aug 10, 2018 •

edited

Loading

odersky commented Aug 15, 2018 •

edited

Loading