compiletime ops could interpret non-literal arguments under algebraic laws

[weihsiu]

i did switch matching on 'that' instead of 'this' per @smarter 's suggestion but to no avail. operations that keeps the same list length like map and zip were ok but concat is giving me problems.

Minimized code

enum NList[N <: Int, +A]:
  def concat[M <: Int](that: NList[M, A]): NList[N + M, A] = this match
    case NNil => that
    case NCons(h, t) => NCons(h, t.concat(that))
  case NNil extends NList[0, Nothing]
  case NCons(head: A, tail: NList[N, A]) extends NList[N + 1, A]

Compiler Output

[error] -- [E007] Type Mismatch Error: 
[error] 10 |      case NNil => that
[error]    |                   ^^^^
[error]    |               Found:    (that : tlp.NLists.NList[M, A])
[error]    |               Required: tlp.NLists.NList[N + M, A]
[error]    |
[error]    |               where:    M is a type in method concat with bounds <: Int
[error] -- [E007] Type Mismatch Error:
[error] 11 |      case NCons(h, t) => NCons(h, t.concat(that))
[error]    |                                            ^^^^
[error]    |              Found:    (that : tlp.NLists.NList[M, A])
[error]    |              Required: tlp.NLists.NList[M², A$1]
[error]    |
[error]    |              where:    M  is a type in method concat with bounds <: Int
[error]    |                        M² is a type variable with constraint <: Int

Expectation

Compiles successfully

[weihsiu]

some more tests. the following compiles.

import scala.compiletime.ops.int._
import scala.util.Not

type X <: Int
type N = 2

summon[1 + 2 =:= 2 + 1]
summon[1 + N =:= N + 1]
summon[X + N =:= X + N]

// the following should NOT compile but does
summon[Not[0 + X =:= X]]
summon[Not[X + 0 =:= X]]
summon[Not[X + 1 =:= 1 + X]]
summon[Not[X + N =:= N + X]]

[bishabosha]

I saw this raised as a concern recently, the logic that computes these compiletime operations does not consider mathematical identities such as 0 + x == x, or commutativity, it only looks for two constant arguments, or does not reduce -

https://github.com/lampepfl/dotty/blob/ce684de6ce4ce77c17750c675343d65a5ef24137/compiler/src/dotty/tools/dotc/core/Types.scala#L4047

[bishabosha]

so as M is never a concrete value, it does not matter if N is 0, as M will never equal N + M - but these algebraic laws can be added in

[bishabosha]

Then there are the reductions necessary for the given example

def concat[M <: Int](that: NList[M, A]): NList[N + M, A] = this match
   // (NNil: NList[N, A]) ==> N == 0
   // 0 + M == M
   // M == N + M
   case NNil => that
   // (NCons(h, t): NList[N, A]) ==> N == (N' + 1)
   // (t.concat(that): NList[N' + M, A]) ==> (NCons(h, t.concat(that)): NList[(N' + M) + 1, A])
   // (N' + M) + 1 == (M + N') + 1
   // (M + N') + 1 == M + (N' + 1)
   // M + (N' + 1) == (N' + 1) + M
   // (N' + 1) + M == N + M
   case NCons(h, t) => NCons(h, t.concat(that))

[Adam-Vandervorst]

Because I needed some of these laws, I implemented them user-side, which looks like this:
https://github.com/Adam-Vandervorst/MacroLoop/blob/collection-laws/collection/src/main/scala/be/adamv/macroloop/collection/Laws.scala