Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Let the type system do it for you

Let the type system do it for you

Presentation at Functional Media, ITV, London.
http://www.meetup.com/Functional-Media/events/137916712/

Richard Dallaway

September 24, 2013
Tweet

More Decks by Richard Dallaway

Other Decks in Programming

Transcript

  1. def csv[N <: Nat]( hdrs: Seq[String], rows: List[Seq[String]]) : String

    = ... import shapeless._ import syntax.sized._
  2. def csv[N <: Nat]( hdrs: Sized[Seq[String], N], rows: List[Seq[String]]) :

    String = ... import shapeless._ import syntax.sized._
  3. def csv[N <: Nat]( hdrs: Sized[Seq[String], N], rows: List[Sized[Seq[String], N]])

    : String = ... import shapeless._ import syntax.sized._
  4. csv( Sized("Date" ), Sized("Mon","6") :: Sized("Tue","-2") :: Nil ) Type

    mismatch at compile time found: Sized[IndexedSeq[String],shapeless.nat._1] required: Sized[Seq[String],Succ[_ >: shapeless.nat._1 ...] Oops
  5. class SizedOps[A, Repr, N <: Nat] ... { def head(implicit

    ev : _0 < N) : A = r.head def tail(implicit pred : Pred[N]) = wrap[Repr, pred.Out](r.tail) ... }