正整数类型 [英] Positive integer type

问题描述

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

解决方案

Haskell可以在编译时执行一些在运行时。你的问题似乎意味着你希望取消任意检查来编译时间，如果没有证明义务的巨大潜力是不可能的（这可能意味着程序员需要证明该属性适用于所有用途）。

在下面，我不觉得我说什么比小猪工作人员提到的东西还多，而提到很酷的声音英制工具。希望每个主题上的附加单词都会为您解释一些解决方案空间。

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

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

智能构造函数：在运行时检查一次，确保通过类型

Gabriel的解决方案是有一个类型 Positive ，它只能是正数。构建正值仍然需要在运行时进行检查，但一旦你有一个积极的消费函数不需要检查 - 静态（编译时）类型检查可以在这里使用。

对许多问题来说，这是一个很好的解决方案。我在讨论黄金数字。从来没有，我不认为这是你正在捕捞。

精确表示

dflemstr评论说您可以使用 Word 类型，它无法表示负数（与表示正数的问题略有不同）。以这种方式，你真的不需要使用保护构造函数（如上所述），因为没有任何类型的居民违反了你的不变量。

更常见的例子使用正确的表示法是非空列表。如果你想要一个永远不能为空的类型，那么你可以创建一个非空的列表类型：

  data NonEmptyList a =单个|缺点（NonEmptyList a）
  

这与使用 Nil 而不是单个a 。

回到正面的例子，你可以使用一种形式的Peano数字：

 数据NonNegative = One | S NonNegative 
  

或者用户GADT来构建无符号二进制数（并且您可以添加 Num 和其他实例，允许像 + ）这样的函数：

  { - ＃LANGUAGE GADTs＃ - } 
 
 data Zero 
 data NonZero 
 data Binary a where 
 I :: Binary a  - >二进制非零
 O ::二进制a  - >二进制a 
 Z ::二进制零
 N ::二进制非零
 
实例显示（二进制a）其中
 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合作的研究团队非常棒。虽然对于一般用途来说太不成熟，但人们已经开发了一些工具来执行诸如静态检查函数偏好性和合同。如果你环顾四周，你会发现它是一个丰富的领域。

In many articles about Haskell they say it allows to make some checks during compile time instead of run time. So, I want to implement the simplest check possible - allow a function to be called only on integers greater than zero. How can I do it?

解决方案

Haskell can perform some checks at compile time that other languages perform at runtime. Your question seems to imply you are hoping for arbitrary checks to be lifted to compile time, which isn't possible without a large potential for proof obligations (which could mean you, the programmer, would need to prove the property is true for all uses).

In the below, I don't feel like I'm saying anything more than what pigworker touched on while mentioning the very cool sounding Inch tool. Hopefully the additional words on each topic will clarify some of the solution space for you.

What People Mean (when speaking of Haskell's static guarantees)

Typically when I hear people talk about the static guarantees provided by Haskell they are talking about the Hindley Milner style static type checking. This means one type can not be confused for another - any such misuse is caught at compile time (ex: let x = "5" in x + 1 is invalid). Obviously, this only scratches the surface and we can discuss some more aspects of static checking in Haskell.

Smart Constructors: Check once at runtime, ensure safety via types

Gabriel's solution is to have a type, Positive, that can only be positive. Building positive values still requires a check at runtime but once you have a positive there are no checks required by consuming functions - the static (compile time) type checking can be leveraged from here.

This is a good solution for many many problems. I recommended the same thing when discussing golden numbers. Never-the-less, I don't think this is what you are fishing for.

Exact Representations

dflemstr commented that you can use a type, Word, which is unable to represent negative numbers (a slightly different issue than representing positives). In this manner you really don't need to use a guarded constructor (as above) because there is no inhabitant of the type that violates your invariant.

A more common example of using proper representations is non-empty lists. If you want a type that can never be empty then you could just make a non-empty list type:

data NonEmptyList a = Single a | Cons a (NonEmptyList a)

This is in contrast to the traditional list definition using Nil instead of Single a.

Going back to the positive example, you could use a form of Peano numbers:

data NonNegative = One | S NonNegative

Or user GADTs to build unsigned binary numbers (and you can add Num, and other instances, allowing functions like +):

{-# 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"

External Proofs

While not part of the Haskell universe, it is possible to generate Haskell using alternate systems (such as Coq) that allow richer properties to be stated and proven. In this manner the Haskell code can simply omit checks like x > 0 but the fact that x will always be greater than 0 will be a static guarantee (again: the safety is not due to Haskell).

From what pigworker said, I would classify Inch in this category. Haskell has not grown sufficiently to perform your desired tasks, but tools to generate Haskell (in this case, very thin layers over Haskell) continue to make progress.

Research on More Descriptive Static Properties

The research community that works with Haskell is wonderful. While too immature for general use, people have developed tools to do things like statically check function partiality and contracts. If you look around you'll find it's a rich field.

这篇关于正整数类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！