Kevin Meredith - 1 year ago 120

Scala Question

Does a

`Int => Option[Nat]`

Its type signature:

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

Examples:

`intToOptionNat(5) == Some( Nat(5) )`

intToOptionNat(-42) == None

Answer Source

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)
^
```