This library provides type-level operations for Typelevel Scala with SIP-23.

Simple example:

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

Using singleton-ops

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.

Supported types:

Char with Singleton (aliased as XChar)
Int with Singleton (aliased as XInt)
Long with Singleton (aliased as XLong)
Float with Singleton (aliased as XFloat)
Double with Singleton (aliased as XDouble)
String with Singleton (aliased as XString)
Boolean with Singleton (aliased as XBoolean)
Nat (from Shapeless)

Supported arithmetic operations:

type +[P1, P2]
type -[P1, P2]
type *[P1, P2]
type /[P1, P2]
type %[P1, P2]
type Abs[P1]
type Negate[P1]

Supported relational operations:

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]

Supported logical operations:

type &&[P1, P2]
type ||[P1, P2]
type ![P1]

Supported explicit conversion operations:

type ToNat[P1]
type ToChar[P1]
type ToInt[P1]
type ToLong[P1]
type ToFloat[P1]
type ToDouble[P1]
type ToString[P1]

Supported string operations:

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]

Supported constraints operations:

type Require[P1]

Supported control operations:

type ==>[A, B] (first A then B)
type ITE[I,T,E] (If (I) Then (T) Else (E))

Supported Aux Pattern interface:

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]

Examples

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 and Int 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

Contributors and participation

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.