35

在许多关于 Haskell 的文章中，他们说它允许在编译时而不是运行时进行一些检查。所以，我想实现最简单的检查——只允许对大于零的整数调用函数。我该怎么做？

4

6 回答 6

44 
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 -> ...
于 2012-08-10T22:49:52.137 回答
36

Haskell 可以在编译时执行一些其他语言在运行时执行的检查。您的问题似乎暗示您希望在编译时取消任意检查，如果没有很大的证明义务潜力，这是不可能的（这可能意味着您，程序员，需要证明该属性对于所有用途都是正确的）。

在下面，我不觉得我说的只是 pigworker 在提到非常酷的发声Inch工具时所触及的。希望关于每个主题的附加词将为您阐明一些解决方案空间。

人们的意思（当谈到 Haskell 的静态保证时）

通常，当我听到人们谈论 Haskell 提供的静态保证时，他们谈论的是 Hindley Milner 风格的静态类型检查。这意味着不能将一种类型与另一种混淆 - 任何此类滥用都会在编译时被捕获（例如：let x = "5" in x + 1无效）。显然，这只是皮毛，我们可以讨论 Haskell 中静态检查的更多方面。

智能构造器：运行时检查一次，通过类型确保安全

Gabriel 的解决方案是有一个类型，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）。

根据猪工所说，我会归Inch为这一类。Haskell 还没有发展到足以执行您想要的任务，但是生成 Haskell 的工具（在这种情况下，是 Haskell 上的非常薄的层）继续取得进展。

更具描述性的静态属性研究

与 Haskell 合作的研究社区非常棒。虽然对于一般用途来说还太不成熟，但人们已经开发出一些工具来执行诸如静态检查函数偏向性和合同之类的事情。如果你环顾四周，你会发现这是一个丰富的领域。

于 2012-08-11T05:57:43.437 回答
32

如果我未能插入 Adam Gundry 的Inch 预处理器，该预处理器管理 Haskell 的整数约束，我将无法履行作为他的主管的职责。

智能构造函数和抽象障碍都非常好，但是它们将过多的测试推向运行时间，并且不允许您实际上以静态检查的方式知道自己在做什么，而无需Maybe填充. （一位学究写道。另一个答案的作者似乎暗示 0 是肯定的，有些人可能会认为这是有争议的。当然，事实是我们使用了各种下限，0 和 1 都经常出现。我们也对上限有一些用处。）

按照 Xi 的 DML 的传统，Adam 的预处理器在 Haskell 原生提供的基础上增加了一层额外的精度，但生成的代码会按原样擦除到 Haskell。如果他所做的工作能够更好地与 GHC 集成，与 Iavor Diatchki 一直在做的类型级自然数的工作相协调，那就太好了。我们很想弄清楚什么是可能的。

回到一般的观点，Haskell 目前没有足够的依赖类型来允许通过理解来构造子类型（例如，大于 0 的 Integer 元素），但您通常可以将类型重构为允许静态约束的更多索引版本。目前，单例类型的构造是实现这一目标的可用方法中最干净的。您需要一种“静态”整数，然后同类居民Integer -> *捕获特定整数的属性，例如“具有动态表示”（这是单例构造，为每个静态事物提供唯一的动态对应物），但还需要更具体的事物，例如“积极”。

英寸代表了一种想象，如果您不需要为单例构造而烦恼，以便使用一些表现良好的整数子集，那会是什么样子。在 Haskell 中，依赖类型编程通常是可能的，但目前比必要的要复杂得多。对这种情况的恰当情绪是尴尬，而我对此感受最为强烈。

于 2012-08-10T23:52:51.257 回答
15

我知道很久以前就已经回答了这个问题，并且我已经提供了自己的答案，但我想提请注意在此期间可用的新解决方案：Liquid Haskell，您可以在此处阅读介绍。

在这种情况下，您可以通过以下方式指定给定值必须为正：

{-@ myValue :: {v: Int | v > 0} #-}
myValue = 5

同样，您可以指定一个函数f只需要这样的正参数：

{-@ f :: {v: Int | v > 0 } -> Int @-}

Liquid Haskell 将在编译时验证给定的约束是否得到满足。

于 2013-06-28T23:02:00.487 回答
5

这——或者实际上，对自然数类型（包括 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。

于 2012-08-11T00:34:39.820 回答
4

GHC 7.6.1 计划使用类型级自然数：https ://ghc.haskell.org/trac/ghc/ticket/4385

使用此功能，编写“自然数”类型很简单，并提供您永远无法实现的性能（例如，使用手动编写的 Peano 数类型）。

于 2012-08-13T06:45:41.567 回答