How in shapeless do you say that a proof is the empty type (i.e. false)

Question

I want to write a function that take a Nat as parameter, and return this nat ONLY if this nat isn't divisible by three.

for example :

def myFunction[N <: Nat](n :N)(implicit ev: /* what do I put here that say not divible by 3 ? */): N = n

To do that, I have to write something that say "N is not divisible by _3", or "Mod.Aux[N, _3,_0] is the empty type"

how can I do that in shapeless ?

Answer 1

The easiest way in this particular case is probably just to use =:!= (although note that you need a new type parameter):

import shapeless._, nat._, ops.nat.Mod

def myFunction[N <: Nat, R <: Nat](n: N)
  (implicit mod: Mod.Aux[N, _3, R], neq: R =:!= _0) = n

More generally, it's not too hard to express this kind of constraint as a type class:

trait NotDivBy3[N <: Nat]

object NotDivBy3 {
  implicit def notDivBy3[N <: Nat]: NotDivBy3[N] = new NotDivBy3[N] {}

  implicit def notDivBy3Ambig[N <: Nat]
    (implicit ev: Mod.Aux[N, _3, _0]): NotDivBy3[N] = unexpected
}

def myFunction[N <: Nat: NotDivBy3](n: N) = n

Or even more generally:

trait DoesntHave[N <: Nat, Prop[_ <: Nat]]

object DoesntHave {
  implicit def doesntHave[N <: Nat, Prop[_ <: Nat]]: DoesntHave[N, Prop] =
    new DoesntHave[N, Prop] {}

  implicit def doesntHaveAmbig[N <: Nat, Prop[_ <: Nat]]
    (implicit ev: Prop[N]): DoesntHave[N, Prop] = unexpected
}

type Mod3Is0[N <: Nat] = Mod.Aux[N, _3, _0]
type NotDivBy3[N <: Nat] = DoesntHave[N, Mod3Is0]

def myFunction[N <: Nat: NotDivBy3](n: N) = n

Both of these solutions use the same machinery as =:!= (i.e. they rely on the fact that the Scala compiler will fail to find an implicit value if it has two candidates that it can't prioritize).

I'd probably tend to go with the second approach, unless I found I needed a lot of constraints like this for the same type, in which case the third might be cleaner.