Making connections between types and values

Question

I have implementations of type-level arithmetics capable of doing some compile time arithmetic validation, namely <,>,= in two ways:

• simple implementation
• rigorous implementation

With these, I can have a getFoo function that I can call like this:

getFoo[_2,_3]

With _2 and _3 being the type-level equivalents of integer values 2 and 3. Now Ideally I would like my getFoo function to take integer values as arguments and attempt to infer _2 from the value 2.

My plan was to add the following associatedInt information to the Nat base class:

trait Nat {
  val associatedInt: Int
  type AssociatedInt = associatedInt.type
}

So that the subsequent types would be defined as:

type _1 = Succ[_0] {
  override val associatedInt: Int = 1
}

And then change getFoo's signature so that it takes an integer:

def getFoo(i:Int)(implicit ...)

Based on which, we would do our type level arithmetic assertions with types associated to the AssociatedInt type. Ie, something like:

def getFoo(i: Integer)(implicit ev: Nat{type I = i.type } =:= ExpectedType)

Which is not working. Ie:

trait Nat {
  val i: Integer
  type I = i.type
}

type ExpectedType = _1

trait _1 extends Nat {
  override val i: Integer = 1
}

def getFoo(i: Integer)
          (implicit ev: Nat{type I = i.type } =:= ExpectedType)= ???

getFoo(1) //this fails to prove the =:= implicit.

On reflection, I shouldn't have expected it to. Since if we have:

val x : Integer = 1
val y : Integer = 1
type X = x.type
type Y = y.type
def foo(implicit ev: X =:= Y) = 123
foo //would fail to compile.

I.e. the singleton types of the different "objects" with the same values is different. (I guess the reason is that currently in Scala the singleton types are for objects and are distinct from literal type)

So with this background information, I would like to know if there is any way to achieve what I am trying to do, namely inferring the a type from an associated value, through other methods.

Answer 1

The trick is to realise that values can have type fields and that type information is available at compile time. With this in mind, we can define:

sealed trait NatEnum{
  type Nat_ <:Nat
}

and define enum "values" for these types like:

object __0 extends NatEnum{ override type Nat_ = _0 }
object __1 extends NatEnum{ override type Nat_ = _1 }
object __2 extends NatEnum{ override type Nat_ = _2 }
object __3 extends NatEnum{ override type Nat_ = _3 }

and refactor getFoo as below:

def getFoo(maj: NatEnum, min: NatEnum)(implicit
                     maj_check: FooClient.Major =:= maj.Nat_,
                     min_check: FooClient.Minor <:< min.Nat_
                    ) = FooClient.foo

which we can test with:

getFoo(__2,__2) //compiles
getFoo(__1,__0)// doesn't compile

here is the updated version of the gists: simple and rigorous