Gab*_*lez 39
module Positive (toPositive, Positive(unPositive)) where
newtype Positive = Positive { unPositive :: Int }
toPositive :: Int -> Maybe Positive
toPositive n = if (n < 0) then Nothing else Just (Positive n)
上面的模块不会导出构造函数,因此构建类型值的唯一方法Positive是提供toPositive一个正整数,然后可以使用它unPositive来解包实际值.
然后,您可以编写一个只接受正整数的函数:
positiveInputsOnly :: Positive -> ...
Tho*_*son 34
Haskell可以在编译时执行一些其他语言在运行时执行的检查.您的问题似乎意味着您希望将任意检查提升到编译时间,如果没有很大的证明义务潜力,这是不可能的(这可能意味着您,程序员,需要证明该属性适用于所有用途) ).
在下面,我并不觉得我在说一个非常酷的发声Inch工具,而不是说什么是染工.希望每个主题的附加词语将为您阐明一些解决方案空间.
人们的意思(谈到Haskell的静态保证时)
通常当我听到人们谈论Haskell提供的静态保证时,他们谈论的是Hindley Milner风格的静态类型检查.这意味着一种类型不能与另一种类型混淆 - 任何此类滥用都会在编译时捕获(例如:let x = "5" in x + 1无效).显然,这只是触及表面,我们可以讨论Haskell中静态检查的更多方面.
智能构造器:在运行时检查一次,通过类型确保安全性
加布里埃尔的解决方案是拥有一种Positive只能是积极的类型.构建正值仍然需要在运行时进行检查,但是一旦得到肯定,就不需要使用函数进行检查 - 可以从此处利用静态(编译时)类型检查.
对于许多问题,这是一个很好的解决方案.在讨论黄金数字时我推荐了同样的东西.从来没有,我不认为这是你钓鱼的.
确切的陈述
dflemstr评论说你可以使用一个类型,Word它不能代表负数(与表示正数的问题略有不同).通过这种方式,您实际上不需要使用受保护的构造函数(如上所述),因为没有类型的居民违反您的不变量.
使用适当表示的更常见示例是非空列表.如果你想要一个永远不会为空的类型,那么你可以只创建一个非空的列表类型:
data NonEmptyList a = Single a | Cons a (NonEmptyList a)
这与使用Nil而不是传统的列表定义形成对比Single a.
回到正面的例子,你可以使用Peano数字的形式:
data NonNegative = One | S NonNegative
或者用户GADT构建无符号二进制数(并且您可以添加Num,以及其他实例,允许这样的函数+):
{-# LANGUAGE GADTs #-}
data Zero
data NonZero
data Binary a where
I :: Binary a -> Binary NonZero
O :: Binary a -> Binary a
Z :: Binary Zero
N :: Binary NonZero
instance Show (Binary a) where
show (I x) = "1" ++ show x
show (O x) = "0" ++ show x
show (Z) = "0"
show (N) = "1"
外部证明
虽然不是Haskell世界的一部分,但可以使用备用系统(例如Coq)生成Haskell,从而可以声明和证明更丰富的属性.以这种方式,Haskell代码可以简单地省略检查,x > 0但x总是大于0的事实将是静态保证(再次:安全性不是由于Haskell).
从Pigworker所说的,我将Inch在这个类别中进行分类.Haskell还没有足够的增长来执行你想要的任务,但生成Haskell的工具(在这种情况下,Haskell上的非常薄的层)继续取得进展.
更具描述性静态属性的研究
与Haskell合作的研究社区非常精彩.虽然对于一般用途来说太不成熟,但人们已经开发了一些工具来执行诸如静态检查功能偏好和合同之类的事情.如果你环顾四周,你会发现它是一个丰富的领域.
pig*_*ker 30
如果我没有插入Adam Gundry的Inch 预处理器来管理Haskell的整数约束,那么作为他的主管,我将失败.
智能构造函数和抽象障碍都非常好,但它们会对运行时进行太多测试,并且不允许您以静态检出的方式实际知道自己在做什么,而不需要Maybe填充.(一个学究写道.另一个答案的作者似乎暗示0是正面的,有些人可能会认为是有争议的.当然,事实是我们有各种下限的用途,0和1都经常发生.我们也有一些用于上限.)
在Xi的DML传统中,Adam的预处理器在Haskell原生提供的基础上增加了额外的精度层,但生成的代码按原样擦除了Haskell.如果他所做的事情可以更好地与GHC整合,那将是很好的,与Iavor Diatchki一直在做的类型级自然数的工作相协调.我们很想知道什么是可能的.
回到一般的观点,Haskell目前还没有充分依赖地键入以允许通过理解构造子类型(例如,Integer的元素大于0),但是您通常可以将类型重构为更接近静态约束的索引版本.目前,单一类型结构是实现这一目标的最不可思议的方法.你需要一种 "静态"整数,然后种类的居民Integer -> *捕获特定整数的属性,如"有一个动态表示"(这是单身结构,给每个静态的东西一个独特的动态对应物),但也有更具体的东西,如"积极".
Inch代表了如果你不需要为单例构造而烦恼的想象,以便与整数的一些表现良好的子集一起工作.在Haskell中通常可以进行依赖类型编程,但目前比必要的更复杂.对这种情况的适当情绪是尴尬,我最为敏锐地感受到它.
Gab*_*lez 13
我知道很久以前就已经回答了这个问题,我已经提供了自己的答案,但是我想提请注意一个新的解决方案,这个解决方案可以在过渡期间使用:Liquid Haskell,你可以在这里阅读介绍.
在这种情况下,您可以通过编写指定给定值必须为正数:
{-@ myValue :: {v: Int | v > 0} #-}
myValue = 5
同样,您可以指定函数f只需要像这样的正参数:
{-@ f :: {v: Int | v > 0 } -> Int @-}
Liquid Haskell将在编译时验证是否满足给定的约束.
这或者实际上,对一类自然数(包括0)的类似需求实际上是关于Haskell的数字类层次结构的常见抱怨,这使得无法为此提供真正干净的解决方案.
为什么？看看定义Num:
class (Eq a, Show a) => Num a where
(+) :: a -> a -> a
(*) :: a -> a -> a
(-) :: a -> a -> a
negate :: a -> a
abs :: a -> a
signum :: a -> a
fromInteger :: Integer -> a
除非您恢复使用error(这是一个不好的做法),有没有办法可以提供的定义(-),negate和fromInteger.