This library provides type-level operations for Typelevel Scala with SIP-23.
import singleton.ops._
class MyVec[L] {
def doubleSize = new MyVec[2 * L]
def nSize[N] = new MyVec[N * L]
def getLength(implicit length : SafeInt[L]) : Int = length
}
object MyVec {
implicit def apply[L](implicit check : Require[L > 0]) : MyVec[L] = new MyVec[L]()
}
val myVec : MyVec[10] = MyVec[4 + 1].doubleSize
val myBadVec = MyVec[-1] //fails compilation, as required
The latest version of the library is 0.5.0, which is available for Scala versions 2.11.12, 2.12.8, and 2.13.1.
If you're using sbt, add the following to your build:
libraryDependencies ++= Seq(
"eu.timepit" %% "singleton-ops" % "0.5.0"
)
If you're using scala.js use %%%
instead
libraryDependencies ++= Seq(
"eu.timepit" %%% "singleton-ops" % "0.5.0"
)
Be sure to follow Typelevel Scala instructions, to be able to use literal types in your code.
Char with Singleton
(aliased asXChar
)Int with Singleton
(aliased asXInt
)Long with Singleton
(aliased asXLong
)Float with Singleton
(aliased asXFloat
)Double with Singleton
(aliased asXDouble
)String with Singleton
(aliased asXString
)Boolean with Singleton
(aliased asXBoolean
)Nat
(from Shapeless)
type +[P1, P2]
type -[P1, P2]
type *[P1, P2]
type /[P1, P2]
type %[P1, P2]
type Abs[P1]
type Negate[P1]
type ==[P1, P2]
type !=[P1, P2]
type >[P1, P2]
type <[P1, P2]
type >=[P1, P2]
type <=[P1, P2]
type Min[P1, P2]
type Max[P1, P2]
type &&[P1, P2]
type ||[P1, P2]
type ![P1]
type ToNat[P1]
type ToChar[P1]
type ToInt[P1]
type ToLong[P1]
type ToFloat[P1]
type ToDouble[P1]
type ToString[P1]
type Length[S]
type +[S1, S2]
(concat)type Reverse[S]
type CharAt[S, I]
type Substring[S, I]
type SubSequence[S, IBeg, IEnd]
type StartsWith[S, Prefix]
type EndsWith[S, Suffix]
type Head[S]
type Tail[S]
type Matches[S, Regex]
type FirstMatch[S, Regex]
type PrefixMatch[S, Regex]
type ReplaceFirstMatch[S, Regex, R]
type ReplaceAllMatches[S, Regex, R]
type Require[P1]
type ==>[A, B]
(first A then B
)type ITE[I,T,E]
(If (I) Then (T) Else (E)
)
type OpAuxNat[O <: Op, Ret_Out <: Nat]
type OpAuxChar[O <: Op, Ret_Out <: XChar]
type OpAuxInt[O <: Op, Ret_Out <: XInt]
type OpAuxLong[O <: Op, Ret_Out <: XLong]
type OpAuxFloat[O <: Op, Ret_Out <: XFloat]
type OpAuxDouble[O <: Op, Ret_Out <: XDouble]
type OpAuxString[O <: Op, Ret_Out <: XString]
type OpAuxBoolean[O <: Op, Ret_Out <: XBoolean]
Int
type operations:
import singleton.ops._
def demo[L <: XInt](implicit p : L*L + L) : p.Out = p.value
val b : 30 = demo[5]
Long
type operations:
import singleton.ops._
def demoLong[L1 <: XLong, L2 <: XLong](implicit p : Min[L1*L1, L2+L2]) : p.Out = p.value
val bLong1 : 1L = demoLong[1L, 5L]
val bLong2 : 6L = demoLong[3L, 3L]
Double
type operations:
import singleton.ops._
def demoDouble[L1 <: XDouble, L2 <: XDouble](implicit p : L1 / L2 + 1.0) : p.Out = p.value
val bDouble : 1.2 = demoDouble[1.0, 5.0]
- Combined
Long
andInt
type operations:
import singleton.ops._
def demoSumLongInt[L1 <: XLong, L2 <: XInt](implicit p : L1 + L2) : p.Out = p.value
val bSumLongInt : 16L = demoSumLongInt[8L, 8]
String
type operations:
import singleton.ops._
def demoString[P1 <: XString](implicit op : Reverse[P1] + P1) : op.Out = op.value
val bString : "cbaabc" = demoString["abc"]
Boolean
type operations:
import singleton.ops._
def demoBoolean[P1 <: XInt](implicit op : P1 < 0) : op.Out = op.value
val bBoolean1 : true = demoBoolean[-5]
val bBoolean2 : false = demoBoolean[5]
val bBoolean3 : false = demoBoolean[0]
Boolean
type constraints:
import singleton.ops._
def demoRequire[P1 <: XInt](implicit op : Require[P1 < 0]) : op.Out = op.value
scala> demoRequire[-1]
demoRequire[-1]
res0: Boolean(true) = true
scala> demoRequire[1]
<console>:16: error: could not find implicit Out for parameter op: singleton.ops.Require[singleton.ops.<[1,0]]
demoRequire[1]
- Shapeless'
Nat
type operations:
import singleton.ops._
import shapeless._
val n = Nat(5)
//Converting Nat to Int singleton occurs implicitly
def demoNatToSing[L <: Nat](implicit p : L+L) : p.Out = p.value
val bSing10 : 10 = demoNatToSing[n.N]
//Converting Int singleton to Nat requires explicit `ToNat`
def demoSingToNat[L <: XInt](implicit op : ToNat[L+L]) : op.Out = op.value
val bNat10 : shapeless.nat._10 = demoSingToNat[5]
- Working with large numbers doesn't slay the compiler:
import singleton.ops._
def bigMul[L1 <: XLong, L2 <: XLong](implicit p : L1 * L2) : p.Out = p.value
scala> bigMul[32000L, 6400000L]
res2: Long = 204800000000
The singleton-ops project supports the Typelevel code of conduct and wants all of its channels (Gitter, GitHub, etc.) to be welcoming environments for everyone.