Skip to content

Instantly share code, notes, and snippets.

@gigiigig
Last active January 25, 2016 22:55
Show Gist options
  • Save gigiigig/537ae8677d3549fe99a4 to your computer and use it in GitHub Desktop.
Save gigiigig/537ae8677d3549fe99a4 to your computer and use it in GitHub Desktop.
First simple type computation
object console extends App {
trait Nat {
type Plus[That <: Nat] <: Nat
}
trait _0 extends Nat {
type Plus[That <: Nat] = That
}
trait Succ[N <: Nat] extends Nat {
type Plus[That <: Nat] = Succ[N#Plus[That]]
}
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
implicitly[_1#Plus[_2] =:= _3]
// implicitly[_1#Plus[_1] =:= _3]
object phantom {
//trait SList[Size <: Nat] {
// def ::(t: Int): SList[Nat]
//}
//object SNil extends SList[_0] {
// def ::(t: Int): SList[_1] = SCons[_1](t, SNil)
//}
//case class SCons[TailSize <: Nat](head: Int, tail: SList[TailSize]) extends SList[TailSize] {
// def ::(t: Int): SList[Succ[TailSize]] = SCons(t, head :: tail)
//}
}
object implicits {
trait Size[T] {
type V <: Nat
}
trait Size0 {
}
object Size extends Size0 {
implicit def nil[T] = new Size[T] {
type V = _0
}
implicit def cont[F[_], T](implicit s: Size[T]) = new Size[F[T]] {
type V = Succ[s.V]
}
}
def foo[T](t: T)(implicit S: Size[T]): S.V = ???
val count2: _2 = foo(List(Option(3)))
val count1: _1 = foo(Option(3))
val count0: _0 = foo(3)
// val wrongCount1: _1 = foo(List(Option(3)))
}
object Print {
trait Print[T] {
type R
def print: R
}
object Print {
implicit def printT[T] = new Print[T] {
type R = String
def print = s"T"
}
implicit def printF[F[_], T](implicit p: Print[T]) = new Print[F[T]] {
type R = String
def print = s"F[T]: ${p.print}"
}
}
def print[T](t: T)(implicit p: Print[T]): p.R = ??? // p.print
val res = print(List(Option(2)))
println(s"res: ${res}")
}
Print
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment