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.