Typelevel natural numbers

Implemented through a "successor" operation `S`, which is
interpreted when applied to constant numbers.

Author: odersky

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -219,6 +219,7 @@ class Definitions {
     def Sys_error(implicit ctx: Context) = Sys_errorR.symbol
 
   lazy val TypelevelPackageObjectRef = ctx.requiredModuleRef("scala.typelevel.package")
+  lazy val TypelevelPackageObject = TypelevelPackageObjectRef.symbol.moduleClass
     lazy val Typelevel_errorR = TypelevelPackageObjectRef.symbol.requiredMethodRef(nme.error)
     def Typelevel_error(implicit ctx: Context) = Typelevel_errorR.symbol
 
@@ -888,6 +889,9 @@ class Definitions {
     }
   }
 
+  final def isTypelevel_S(sym: Symbol)(implicit ctx: Context) =
+    sym.name == tpnme.S && sym.owner == TypelevelPackageObject
+
   // ----- Symbol sets ---------------------------------------------------
 
   lazy val AbstractFunctionType = mkArityArray("scala.runtime.AbstractFunction", MaxImplementedFunctionArity, 0)

compiler/src/dotty/tools/dotc/core/StdNames.scala

@@ -204,6 +204,7 @@ object StdNames {
     final val Object: N              = "Object"
     final val PartialFunction: N     = "PartialFunction"
     final val PrefixType: N          = "PrefixType"
+    final val S: N                   = "S"
     final val Serializable: N        = "Serializable"
     final val Singleton: N           = "Singleton"
     final val Throwable: N           = "Throwable"

compiler/src/dotty/tools/dotc/core/TypeApplications.scala

@@ -12,6 +12,7 @@ import util.common._
 import Names._
 import NameOps._
 import NameKinds._
+import Constants.Constant
 import Flags._
 import StdNames.tpnme
 import util.Positions.Position
@@ -409,8 +410,15 @@ class TypeApplications(val self: Type) extends AnyVal {
         LazyRef(c => dealiased.ref(c).appliedTo(args))
       case dealiased: WildcardType =>
         WildcardType(dealiased.optBounds.appliedTo(args).bounds)
-      case dealiased: TypeRef if dealiased.symbol == defn.NothingClass =>
-        dealiased
+      case dealiased: TypeRef =>
+        val sym = dealiased.symbol
+        if (sym == defn.NothingClass) return dealiased
+        if (defn.isTypelevel_S(sym) && args.length == 1)
+          args.head.safeDealias match {
+            case ConstantType(Constant(n: Int)) => return ConstantType(Constant(n + 1))
+            case none =>
+          }
+        AppliedType(self, args)
       case dealiased =>
         AppliedType(self, args)
     }

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -11,6 +11,7 @@ import config.Config
 import config.Printers.{typr, constr, subtyping, gadts, noPrinter}
 import TypeErasure.{erasedLub, erasedGlb}
 import TypeApplications._
+import Constants.Constant
 import scala.util.control.NonFatal
 import typer.ProtoTypes.constrained
 import reporting.trace
@@ -288,6 +289,15 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
           case ConstantType(v1) => v1.value == v2.value
           case _ => secondTry
         }
+      case tp2: AnyConstantType =>
+        if (tp2.tpe.exists) recur(tp1, tp2.tpe)
+        else tp1 match {
+          case tp1: ConstantType =>
+            tp2.tpe = tp1
+            true
+          case _ =>
+            secondTry
+        }
       case _: FlexType =>
         true
       case _ =>
@@ -831,7 +841,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
           canConstrain(param2) && canInstantiate(param2) ||
           compareLower(bounds(param2), tyconIsTypeRef = false)
         case tycon2: TypeRef =>
-          isMatchingApply(tp1) || {
+          isMatchingApply(tp1) ||
+          defn.isTypelevel_S(tycon2.symbol) && compareS(tp2, tp1, fromBelow = true) || {
             tycon2.info match {
               case info2: TypeBounds =>
                 compareLower(info2, tyconIsTypeRef = true)
@@ -865,14 +876,39 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
           }
           canConstrain(param1) && canInstantiate ||
             isSubType(bounds(param1).hi.applyIfParameterized(args1), tp2, approx.addLow)
-        case tycon1: TypeRef if tycon1.symbol.isClass =>
-          false
+        case tycon1: TypeRef =>
+          val sym = tycon1.symbol
+          !sym.isClass && (
+            defn.isTypelevel_S(sym) && compareS(tp1, tp2, fromBelow = false) ||
+            recur(tp1.superType, tp2))
         case tycon1: TypeProxy =>
           recur(tp1.superType, tp2)
         case _ =>
           false
       }
 
+    /** Compare `tp` of form `S[arg]` with `other`, via ">:>` if fromBelowis true, "<:<" otherwise.
+     *  If `arg` is a Nat constant `n`, proceed with comparing `n + 1` and `other`.
+     *  Otherwise, if `other` is a Nat constant `n`, proceed with comparing `arg` and `n - 1`.
+     */
+    def compareS(tp: AppliedType, other: Type, fromBelow: Boolean): Boolean = tp.args match {
+      case arg :: Nil =>
+        natValue(arg) match {
+          case Some(n) =>
+            val succ = ConstantType(Constant(n + 1))
+            if (fromBelow) recur(other, succ) else recur(succ, other)
+          case none =>
+            natValue(other) match {
+              case Some(n) if n > 0 =>
+                val pred = ConstantType(Constant(n - 1))
+                if (fromBelow) recur(pred, arg) else recur(arg, pred)
+              case none =>
+                false
+            }
+        }
+      case _ => false
+    }
+
     /** Like tp1 <:< tp2, but returns false immediately if we know that
     *  the case was covered previously during subtyping.
     */
@@ -914,6 +950,17 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
     }
   }
 
+  /** Optionally, the `n` such that `tp <:< ConstantType(Constant(n: Int))` */
+  def natValue(tp: Type): Option[Int] = {
+    val ct = new AnyConstantType
+    if (isSubTypeWhenFrozen(tp, ct))
+      ct.tpe match {
+        case ConstantType(Constant(n: Int)) if n >= 0 => Some(n)
+        case _ => None
+      }
+    else None
+  }
+
   /** Subtype test for corresponding arguments in `args1`, `args2` according to
   *  variances in type parameters `tparams`.
   */
@@ -1713,6 +1760,11 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
 
 object TypeComparer {
 
+  /** Class for unification variables used in `natValue`. */
+  private class AnyConstantType extends UncachedGroundType with ValueType {
+    var tpe: Type = NoType
+  }
+
   private[core] def show(res: Any)(implicit ctx: Context) = res match {
     case res: printing.Showable if !ctx.settings.YexplainLowlevel.value => res.show
     case _ => String.valueOf(res)
@@ -1773,7 +1825,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
     def paramInstances = new TypeAccumulator[Array[Type]] {
       def apply(inst: Array[Type], t: Type) = t match {
         case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
-          inst(n) = instanceType(t, fromBelow = variance >= 0)
+          inst(n) = approximation(t, fromBelow = variance >= 0).simplified
           inst
         case _ =>
           foldOver(inst, t)

library/src-scala3/scala/typelevel/package.scala

@@ -7,4 +7,6 @@ package object typelevel {
   case class Typed[T](val value: T) { type Type = T }
 
   rewrite def error(transparent msg: String): Nothing = ???
+
+  type S[X <: Int] <: Int
 }

tests/pos/matchtype.scala

@@ -5,21 +5,17 @@ object Test {
     case Int => String
   }
 
-  trait Nat {
-    def toInt: Int = ???
-  }
-
-  case object Z extends Nat
-  case class S[N <: Nat] extends Nat
-  type Z = Z.type
-
-  type Len[X] = X match {
-    case Unit => Z
+  type Len[X] <: Int = X match {
+    case Unit => 0
     case x *: xs => S[Len[xs]]
   }
 
   type T2 = Len[(1, 2, 3)]
-  erased val x: S[S[S[Z]]] = erasedValue[T2]
+  erased val x: 3 = erasedValue[T2]
+
+  type T1 = S[0]
+
+  erased val x2: 1 = erasedValue[T1]
 
   rewrite def checkSub[T1, T2] =
     rewrite typelevel.erasedValue[T1] match {
@@ -32,19 +28,39 @@ object Test {
     checkSub[T2, T1]
   }
 
-  checkSame[T2, S[S[S[Z]]]]
+  checkSame[T2, S[S[S[0]]]]
 
   type Head[X <: Tuple] = X match {
     case (x1, _) => x1
   }
 
   checkSame[Head[(Int, String)], Int]
 
-  type Concat[X <: Tuple, Y <: Tuple] = X match {
+  type Concat[X <: Tuple, Y <: Tuple] <: Tuple = X match {
     case Unit => Y
     case x1 *: xs1 => x1 *: Concat[xs1, Y]
   }
 
+  type Elem[X <: Tuple, N] = X match {
+    case x *: xs =>
+      N match {
+        case 0 => x
+        case S[n1] => Elem[xs, n1]
+      }
+  }
+
+  type Elem1[X <: Tuple, N] = (X, N) match {
+    case (x *: xs, 0) => x
+    case (x *: xs, S[n1]) => Elem1[xs, n1]
+  }
+
+  erased val x3: String = erasedValue[Elem[(String, Int), 0]]
+  erased val x4: Int = erasedValue[Elem1[(String, Int), 1]]
+
+  checkSame[Elem[(String, Int, Boolean), 0], String]
+  checkSame[Elem1[(String, Int, Boolean), 1], Int]
+  checkSame[Elem[(String, Int, Boolean), 2], Boolean]
+
   checkSame[Concat[Unit, (String, Int)], (String, Int)]
   checkSame[Concat[(Boolean, Boolean), (String, Int)], Boolean *: Boolean *: (String, Int)]
   checkSub[(Boolean, Boolean, String, Int), Concat[(Boolean, Boolean), String *: Int *: Unit]]