gistfile1.scala

package util

import shapeless._
import shapeless.TypeOperators._
import shapeless.Nat._
import shapeless.LTEq._
import scala.annotation.implicitNotFound

@implicitNotFound("Cannot prove that ${A} is evenly divisble by ${B}")
trait Div[A <: Nat, B <: Nat]

object Div {
  implicit def mod[A <: Nat, B <: Nat, C <: Nat](implicit div: DivAux[A, B, C], ev: C =:= _0): Div[A, B] =
    new Div[A, B] {}
}

trait DivAux[A <: Nat, B <: Nat, C <: Nat]

object DivAux {
  implicit def divAux[A <: Nat, B <: Nat](implicit m: Mod[A, B]): DivAux[A, B, m.Out] =
    new DivAux[A, B, m.Out] {}
}

@implicitNotFound("Cannot prove that ${A} is NOT evenly divisble by ${B}")
trait NDiv[A <: Nat, B <: Nat]

object NDiv {
  implicit def mod[A <: Nat, B <: Nat, C <: Nat](implicit div: DivAux[A, B, C], ev: C =:!= _0): NDiv[A, B] =
    new NDiv[A, B] {}
}

object Foo {


  // H is centuries, L is low years 0 - 99
  trait LeapYear[H <: Nat, L <: Nat]
  object LeapYear {

    // if low is divisible by 4 and is not zero, it's a leap year always
    implicit def leap1[H <: Nat, L <: Nat](implicit div: Div[L, _4], nz: L =:!= _0): LeapYear[H, L] =
      new LeapYear[H, L] {}

    // If low is zero and hi is divisible by 4, it's a leap year
    implicit def leap2[H <: Nat, L <: Nat](implicit div: Div[H, _4], z: L =:= _0): LeapYear[H, L] =
      new LeapYear[H, L] {}

  }

  def ly[H <: Nat, L <: Nat](implicit ev: LeapYear[H, L]) = "\\o/"

  implicitly[Div[_20, _4]]
  implicitly[_0 =:= _0]

  
 ly[_19, _12] // ok; 1913 won't compile
  
}

This is what I have in Idris, so far. Trait LeapYear written out as a GADT, with leap1 as "isLeapYear".

data LeapYear : Nat -> Nat -> Type where
  twoThousandEight : LeapYear 20 8
  isLeapYear : (h: Nat) -> (l: Nat) -> mod l 4 = Z -> Not(l = Z) -> LeapYear h l

Somewhat less glamorous than I was hoping for, so far. Apparently proving (12 = Z) -> _|_ is beyond me at the moment, so I took out the Not(l = Z) part.

Then I can write

ly : {h : Nat} -> {l : Nat} -> {ev : LeapYear h l} -> String
ly = "yippie"

and call it as

ly {ev = isLeapYear 19 12 refl}

(The {}'s mean implicit param a la Scala's [] for type params or something)
Not terribly exciting thus far, I guess.

Though, I could just cheat:
Write a "isLeapYear" function in the "value system":

leapYear : Nat -> Bool
leapYear x = True

(conveniently always agrees, for now)
and toss it in a type sig somewhere:

isItALeapYear : so (leapYear 2013)
isItALeapYear = oh

GADT's seem a lot like Scala. You have them in Haskell as an extension; they're on by default in Idris.

So where in Idris you might have

data Div : Nat -> Nat -> Type where
  divs : (a: Nat) -> (b: Nat) -> {auto ev: mod a b = Z} -> Div a b

In Scala you could have

sealed trait Div[Nat, Nat]

class divs[a <: Nat, b <: Nat, Mod[a,b] =:= Z] extends Div[a, b]

See? Idris is the same as Scala is the same as Ruby... doesn't matter, all the same.