Last active
December 13, 2016 22:43
-
-
Save tomverran/078ce31f6cda852b8f1560b7d689bca9 to your computer and use it in GitHub Desktop.
type level natural numbers + a fixed length list
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import scala.language.higherKinds | |
// trying to understand why shapeless does things it does by reimplementing them | |
/* | |
* scalaVersion := "2.11.8" | |
* resolvers += Resolver.sonatypeRepo("releases") | |
* addCompilerPlugin("org.spire-math" %% "kind-projector" % "0.9.3") | |
*/ | |
sealed trait Nat | |
sealed trait Succ[N <: Nat] extends Nat | |
sealed trait _0 extends Nat | |
type _1 = Succ[_0] | |
type _2 = Succ[_1] | |
type _3 = Succ[_2] | |
type _4 = Succ[_3] | |
type _5 = Succ[_4] | |
trait NatToInt[A <: Nat] { | |
def value: Int | |
} | |
object NatToInt { | |
def value[A <: Nat : NatToInt] = implicitly[NatToInt[A]].value | |
} | |
implicit object NatToZero extends NatToInt[_0] { | |
def value = 0 | |
} | |
implicit def NatToNum[B <: Nat : NatToInt] = new NatToInt[Succ[B]] { | |
def value = 1 + implicitly[NatToInt[B]].value | |
} | |
NatToInt.value[_3] | |
trait FixedList[+A] // a fixed length list where the length is encoded in the type | |
case object FixedNil extends FixedList[Nothing] { | |
override def toString = "nil" | |
} | |
case class FixedCons[A, B <: FixedList[A]](a: A, n: B) extends FixedList[A] { | |
override def toString = s"$a, $n" | |
} | |
implicit class TypeListOps[A](a: A) { | |
def :+[B <: FixedList[A]](b: B) = FixedCons(a, b) | |
} | |
val list = 6 :+ (7 :+ FixedNil) | |
trait ToNat[A] { | |
type Out <: Nat | |
} | |
object ToNat { | |
type Aux[A <: FixedList[Any], O <: Nat] = ToNat[A] { type Out = O } | |
} | |
implicit object NilToNat extends ToNat[FixedNil.type] { | |
type Out = _0 | |
} | |
implicit def ListToNat[A, B <: FixedList[A]](implicit t: ToNat[B]) = new ToNat[FixedCons[A, B]] { | |
type Out = Succ[t.Out] | |
} | |
def length[A <: FixedList[Int], R <: Nat](a: A)(implicit b: ToNat.Aux[A, R], c: NatToInt[R]) = | |
c.value | |
def onlyTwo[A <: FixedList[Int]](a: A)(implicit b: ToNat.Aux[A, _2]): String = | |
s"$a has two items" | |
onlyTwo(list) | |
// onlyTwo(5 +: list) does not compile! | |
/** | |
* Convert a nat F to an FixedList[A] | |
* whose type is exposed in Out | |
* and whose value is in .value | |
* but has some context M attached | |
* | |
* i.e. in a list fill operation given a Nat you should get an Item => List function as the value | |
* in a list to fixed operation given a Nat you should get a List[Item] => Option[List] | |
*/ | |
trait NatToList[N <: Nat, A, M[_]] { | |
type Out <: FixedList[A] | |
def value: M[Out] | |
} | |
/** | |
* instances to convert a _0 and a Nat into a function | |
* that given an A will return a fixed length list of A | |
*/ | |
implicit def ZeroToListFill[A] = new NatToList[_0, A, A => ?] { | |
type Out = FixedNil.type | |
def value: A => Out = _ => FixedNil | |
} | |
implicit def SuccToListFill[N <: Nat, A](implicit tl: NatToList[N, A, A => ?]) = new NatToList[Succ[N], A, A => ?] { | |
override type Out = FixedCons[A, tl.Out] | |
override def value: A => Out = v => FixedCons(v, tl.value(v)) | |
} | |
sealed trait ListError | |
case object TooShort extends ListError | |
case object TooLong extends ListError | |
type ListFunc[A, B] = A => Either[ListError, B] | |
/** | |
* instances to convert a _0 and a Nat into a function | |
* that given a List[A] will return either ListError or a fixed length list of A | |
*/ | |
implicit def ZeroToListConvert[A] = new NatToList[_0, A, ListFunc[List[A], ?]] { | |
type Out = FixedNil.type | |
def value: List[A] => Either[ListError, Out] = { | |
case Nil => Right(FixedNil) | |
case a :: as => Left(TooLong) | |
} | |
} | |
implicit def SuccToListConvert[N <: Nat, A](implicit tl: NatToList[N, A, ListFunc[List[A], ?]]) = new NatToList[Succ[N], A, ListFunc[List[A], ?]] { | |
override type Out = FixedCons[A, tl.Out] | |
def value: List[A] => Either[ListError, Out] = { | |
case a :: as => tl.value.apply(as).right.map(FixedCons(a, _)) | |
case _ => Left(TooShort) | |
} | |
} | |
def fill[N <: Nat, A](implicit tl: NatToList[N, A, A => ?]) = | |
tl.value | |
implicit class FixableList[A](a: List[A]) { | |
def toFixedList[N <: Nat](implicit tl: NatToList[N, A, ListFunc[List[A], ?]]): Either[ListError, tl.Out] = tl.value.apply(a) | |
} | |
implicit class FillableValue[A](a: A) { | |
def fillFixedList[N <: Nat](implicit tl: NatToList[N, A, A => ?]): tl.Out = tl.value.apply(a) | |
} | |
List(1, 2, 3, 4).toFixedList[_3] // too long! | |
List(1, 2).toFixedList[_3] // too short! | |
List(1, 2, 3).toFixedList[_3] // just right | |
"foo".fillFixedList[_1] | |
trait GreaterThan[A <: Nat, B <: Nat] { | |
type Out <: Nat | |
} | |
object GreaterThan { | |
type Aux[A <: Nat, B <: Nat, C] = GreaterThan[A, B] { type Out = C } | |
} | |
implicit def NatGreaterThanZero[A <: Nat] = new GreaterThan[Succ[A], _0] { | |
type Out = Succ[A] | |
} | |
implicit def NatGreaterThanNat[A <: Nat, B <: Nat](implicit g: GreaterThan[A, B]) = new GreaterThan[Succ[A], Succ[B]] { | |
type Out = g.Out | |
} | |
/** | |
* This function won't compile if A is not longer than B | |
* using NatToInt to get the diff though is just me playing about | |
*/ | |
def howMuchLonger[A <: FixedList[Int], B <: FixedList[Int], S <: Nat, X <: Nat, D <: Nat](l1: A, l2: B)( | |
implicit | |
sizeA: ToNat.Aux[A, S], | |
sizeB: ToNat.Aux[B, X], | |
gt: GreaterThan.Aux[S, X, D], | |
toInt: NatToInt[D] | |
): Int = { | |
toInt.value | |
} | |
howMuchLonger( | |
List(1, 2, 3, 4).toFixedList[_4].right.toOption.get, | |
List(1, 2).toFixedList[_2].right.toOption.get | |
) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment