=> Option[Nat]？

Question

Int => Option[Nat]函数是否以无形形式存在？

其类型签名：

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

示例：

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

Answer 1

我认为您要寻找的是一个函数，它将把一个Int转换成相应的Nat子类型，这将是某种形式的_0、Succ[_0]、Succ[Succ[_0]]等等。

因为我们通常希望在后续的类型级别计算中利用得到的Nat子类型的结构，所以需要在编译时静态地知道这一点。因此Int类型不够精确.我们需要一个Int单例类型代替。这些(现在还没有)不能在Scala中直接表示，尽管无形状提供了基于宏的隐式转换，用于从Int文本计算Nat，

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

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

由于这是静态计算的，所以不需要将结果类型包装在Option中.如果参数文字没有Nat表示，它将是编译时错误，

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