Haskell是不是因为拉姆达演算的许多语言的详细数学,但我认为,域名是不完整的数字:我们有Integer和Float,例如,而不是Positive或Negative,或[1..5]作为域.这有时会使函数不安全,而编译器可能会捕获类型错误.例如:5mod 仅在运行时0输出*** Exception: divide by zero.
mod :: Integral a => a -> a -> a但我们可以有类似的东西mod :: Integral a, a != 0 => a -> a -> a; 像守卫或间隔或其他数据类型的东西......在游戏中,我希望我的角色有一个正数的生命.或者从0到100,不在下,不是上.当他被击中时,我需要称之为丑陋positive x = if x > 0 then x else 0.连C都signed和unsigned.
这是一个弱点还是他们为什么没有"间隔"域名的原因？有没有一个包修复这个？
听起来你正在寻找一种依赖类型的语言,如Agda,Idris或Coq.
你是对的,拥有受限制的数字类型会很好,但你需要考虑如何使用这些类型.假设您的类型mod排除了一个0值.现在你需要在你的程序中调用它.如果数字是文字,大概是编译器"很容易"确定它不是0并让你调用该函数,但是如果数字是在运行时提供的,可能来自用户输入或某些复杂的程序呢？你需要一些方法向编译器解释你知道0在你传入它时它不会是这个数字mod.Haskell并没有真正有能力以任何简单的方式做到这一点(有很多令人讨厌的方法,比如将所有值反映到类型系统中),这就是为什么你看不到更精确的类型.
你可以自由地制作这样的课程,但也许他们没有被包含在Haskell中的原因是因为人们找不到让它们经常有用的方法.
很明显你想要与你的班级相减,但你也希望它被关闭.
这样的事可能吗？
NonNegative x - NonNegative y = NonNegative (max (x - y) 0)
但那时身份x - y + y == x并不成立.
人们为Haskell制作了替代数字层次结构,例如"数字前奏曲".Haskell对自定义非常友好,你甚至可以用自己的定义替换Prelude,但是它们是否有用并且不会导致比它们解决的问题更多的问题是另一回事.