Kevin Meredith Kevin Meredith - 3 months ago 22
Scala Question

Int => Option[Nat]?

Does a

Int => Option[Nat]
function exist in Shapeless?

Its type signature:

intToOptionNat(a: Int): Option[Nat] = ???


Examples:

intToOptionNat(5) == Some( Nat(5) )
intToOptionNat(-42) == None

Answer

I think that what you're looking for is a function which will convert an Int to the corresponding Nat subtype, which will be something of the form _0, Succ[_0], Succ[Succ[_0]] etc.

Because we typically want to exploit the structure of the resulting Nat subtype in some subsequent type level computation this is something which need to know statically, at compile time. Consequently the type Int isn't sufficiently precise ... we need an Int singleton type instead. These are not (yet) directly expressible in Scala, however shapeless provides a macro-based implicit conversion for computing a Nat from an Int literal,

scala> import shapeless.syntax.nat._
import shapeless.syntax.nat._

scala> def intToNat(n: Nat): n.type = n
intToNat: (n: shapeless.Nat)n.type

Since this is computed statically there's no need for the result type to be wrapped in Option ... if the argument literal doesn't have a Nat representation it will be a compile time error,

scala> intToNat(5)
res0: Succ[Succ[Succ[Succ[Succ[_0]]]]] = Succ()

scala> intToNat(-42)
<console>:19: error: Expression -42 does not evaluate to a non-negative Int literal
       intToNat(-42)
                 ^