基于Scala约束的类型和文字

Question

我在想是否可以在Scala中定义类型如NegativeNumber。这种类型将是一个负数，它将由编译器同样进行检查，以整型，字符串等

val x: NegativeNumber = -34 
val y: NegativeNumber = 34 // should not compile 

同样：

val s: ContainsHello = "hello world" 
val s: ContainsHello = "foo bar" // this should not compile either 

我可以使用这些类型，就像其他类型，例如：

def myFunc(x: ContainsHello): Unit = println(s"$x contains hello") 

这些约束类型可以由临时类型（Int，String）支持。

是否可以实现这些类型（可能与宏）？

自定义文字怎么样？

val neg = -34n //neg is of type NegativeNumber because of the suffix 
val pos = 34n // compile error 

Answer 1

不幸的是，这不是你在编译时可以轻易检查的东西。那么 - 至少不是如果你不限制你的类型的操作。如果您的目标仅仅是检查数字文字是否为非零，您可以轻松编写一个检查此属性的宏。但是，我并没有看到证明否定字面确实是否定的任何好处。

问题不在于Scala的限制 - 它具有非常强大的类型系统 - 但事实是（在一个相当复杂的程序中）不能静态地知道每个可能的状态。然而，你可以尝试超越所有可能状态的集合。

让我们考虑引入仅表示负数的类型NegativeNumber的示例。为了简单起见，我们只定义一个操作：plus。假设你只允许增加多个NegativeNumber，那么类型系统可以用来保证每个NegativeNumber确实是一个负数。但是这看起来确实很严格，所以一个有用的例子肯定会让我们至少增加一个NegativeNumber和一个通用的Int。

如果您有一个表达式val z: NegativeNumber = plus(x, y)，那么您不知道静态地（可能是它们由函数返回）的值为x和y。你怎么知道（静态地）z是不合格的负数？

的方法来解决这一问题将是引进Abstract Interpretation必须在你的程序（源代码，抽象语法树，...）的表示来运行。

例如，你可以对数字定义一个格包含下列元素：

• Top：所有数字
• +：所有正数
• 0：数0
• -：全部为负数
• Bottom：不是一个数字 - 只介绍每对元件具有最大下界

与订货Top>（+，0，-）>Bottom。

然后，你需要定义语义您的操作。从我们的例子中以可交换方法plus：

• plus(Bottom, something)总是Bottom，因为你不能使用无效的数字
• plus(Top, x)某种计算，x != Bottom总是Top，因为添加任意数量任意数量始终是一个随心所欲数
• plus(+, +)是+，因为增加了两个正数总是会产生一个正数
• plus(-, -)是因为添加两个负数将总是产生负数
• plus(0, x),x != Bottom是x，因为0是加法的标识。

的问题是，

• plus - +将Top，因为你不知道，如果它是一个正数或负数做。

所以是静态的安全，你必须采取保守方法，并禁止这样的操作。

有more sophisticated numerical domains但最终，它们都遭受同样的问题：它们代表了对实际程序状态的过度验证。

我会说这个问题类似于整数溢出/下溢：一般来说，你不知道静态操作是否表现出溢出 - 你只知道在运行时。

Answer 2

如果实现了SIP-23，可以使用隐式参数作为细化类型的一种形式。然而，这将是有问题的价值，但由于Scala编译器和类型系统并没有很好的配备来证明例如整型的有趣的事情。为此，使用具有依赖类型的语言（Idris等）或SMT解算器（LiquidHaskell等）检查的精化类型会更好。