module Positive (toPositive, getPositive, Positive) where

newtype Positive = Positive { unPositive :: Int }

toPositive :: Int -> Maybe Positive
toPositive n = if (n <= 0) then Nothing else Just (Positive n)

-- We can't export unPositive, because unPositive can be used
-- to update the field.  Trivially renaming it to getPositive
-- ensures that getPositive can only be used to access the field
getPositive :: Positive -> Int
getPositive = unPositive

上面的模块没有导出构造函数，因此构建Positive类型的值的唯一方法是为toPositive提供一个正整数，然后可以使用getPositive展开该正整数以访问实际值。
然后，您可以使用以下语句编写一个只接受正整数的函数：

positiveInputsOnly :: Positive -> ...

Haskell可以在编译时执行一些其他语言在运行时执行的检查。你的问题似乎暗示你希望将任意检查提升到编译时，如果没有很大的潜在证明义务（这可能意味着你，程序员，需要证明该属性在所有用途下都是真的），这是不可能的。
在下面的内容中，我并不觉得我说的比pigworker提到的听起来很酷的Inch工具更多。希望每个主题上的附加词能为你澄清一些解决方案空间。

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

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

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

Gabriel的解决方案是创建一个类型Positive，它只能是正数。构建正数仍然需要在运行时进行检查，但是一旦得到了正数，就不需要在使用函数时进行检查了--静态（编译时）类型检查可以从这里开始使用。
这是一个很好的解决很多问题的方法。我在讨论黄金数字的时候也推荐了同样的方法。但是，我不认为这是你想要的。

精确表示

dflemstr评论说，您可以使用Word类型，它不能表示负数（这与表示正数的问题略有不同）。这样，您实际上不需要使用受保护的构造函数（如上所述），因为该类型中没有违反不变量的成员。
一个更常见的使用正确表示的例子是非空列表。如果你想要一个永远不能为空的类型，那么你可以直接创建一个非空列表类型：

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

这与使用Nil而不是Single a的传统列表定义形成对比。
回到正例，你可以使用皮亚诺数的一种形式：

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合作的研究社区非常棒。虽然对于一般用途来说还太不成熟，但人们已经开发了一些工具来做静态检查function partiality和contracts之类的事情。如果你环顾四周，你会发现这是一个丰富的领域。

如果我不能插入Adam Gundry的Inch预处理器，那我就没有尽到作为他的主管的责任。
智能构造函数和抽象障碍都很好，但是它们将太多的测试推到了运行时，并且不允许您以静态 checkout 的方式实际知道自己在做什么，而不需要Maybe填充。另一个答案的作者似乎暗示0是正的，有些人可能会认为这是有争议的。当然，事实上，我们有很多下界的用法，0和1都经常出现，我们也有一些上界的用法。
在Xi的DML的传统中，Adam的预处理器在Haskell本机提供的基础上增加了一层额外的精确度，但产生的代码会被Haskell擦除。如果他所做的可以更好地与GHC集成，与Iavor Diatchki一直在做的类型级自然数的工作相协调，那就太好了。我们渴望弄清楚什么是可能的。
回到一般的观点，Haskell目前没有足够的依赖类型化，不允许通过理解来构造子类型（例如，大于0的Integer元素），但您通常可以将类型重构为允许静态约束的索引更多的版本。目前，singleton 类型构造是实现这一点的最简洁的方法。您需要一种“静态”整数，那么Integer -> *类型的居民不仅捕获了诸如“具有动态表示”之类的特定整数的属性（这是单例构造，为每个静态事物赋予唯一的动态对应物），而且还捕获了诸如“为正”之类的更具体的事物。
Inch代表了一种想象，如果你不需要为单例构造而烦恼，就可以处理一些行为相当良好的整数子集。依赖类型编程在Haskell中经常是可能的，但目前比必要的复杂。对这种情况的适当看法是尴尬，我个人对此感受最深。

我知道这一问题很久以前就得到了回答，我也已经提供了我自己的答案，但我想提请大家注意在此期间出现的一个新的解决办法：Liquid Haskell，您可以阅读here的介绍。
在这种情况下，您可以指定给定的值必须为正数，方法是写入：

{-@ 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的定义。

GHC 7.6.1计划使用类型级自然数：https://ghc.haskell.org/trac/ghc/ticket/4385
使用这个特性，编写一个“自然数”类型是很简单的，并且提供了一个你永远无法达到的性能（例如，使用手动编写的Peano数字类型）。