Open weihsiu opened 4 years ago
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]]
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 -
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
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))
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
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
Compiler Output
Expectation
Compiles successfully