如何将一种类型限制为另一种类型的子集?

发布于 2024-10-16 18:51:35 字数 310 浏览 0 评论 0原文

我有一种这是一个愚蠢的问题的感觉,但是这里...我可以定义一个类型,它是另一种类型的元素的子集吗?这是一个简化的示例。

scala> class Even(i: Int) {
     | assert(i % 2 == 0)  
     | }
defined class Even

scala> new Even(3)
java.lang.AssertionError: assertion failed

这是运行时检查。我可以定义一个类型以便在编译时进行检查吗?即,输入参数 i 可以证明总是偶数?

I have that this is a dumb question feeling, but here goes ... Can I define a type that is a subset of the elements of a another type? Here's a simplified example.

scala> class Even(i: Int) {
     | assert(i % 2 == 0)  
     | }
defined class Even

scala> new Even(3)
java.lang.AssertionError: assertion failed

This is a runtime check. Can I define a type such that this is checked at compilation? IE, that the input parameter i is provably always even?

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(1

◇流星雨 2024-10-23 18:51:35

Coq 和 Agda 等语言中的值依赖类型可以做到这一点,但 Scala 不行。

然而,根据具体的用例,在类型系统中对 peano 数字进行编码的方法可能会对您有所帮助。

您可能还想尝试定义 EvenOdd 以及一些密封的抽象超类型(也许是 OddOrEven)以及返回正确值的工厂方法任何给定整数的实例。

另一种可能性是将 Even 定义为提取器。

Value-dependent typing in languages such as Coq and Agda can do this, though not Scala.

Depending on the exact use-case, there are ways of encoding peano numbers in the type system that may, however, help you.

You might also want to try defining both Even and Odd along with some sealed abstract supertype (OddOrEven perhaps) and a factory method that returns the correct instance from any given Integer.

Another possibility is to define Even as an extractor.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文