将一个数字限制在一个范围内(Haskell)

Question

我公开了一个函数，它包含两个参数，一个是最小界，另一个是最大界。如何使用类型确保最小界不大于最大界？

我希望避免创建一个智能构造函数，并返回一个可能会使整个使用变得更加繁琐。

谢谢

Answer 1

这并不能确切地回答你的问题，但有时有效的一种方法是改变你对你的类型的理解。例如，而不是

data Range = {lo :: Integer, hi :: Integer}

你可以用

data Range = {lo :: Integer, size :: Natural}

这样，就无法表示无效的范围。

Answer 2

此解决方案使用依赖类型(可能太重，请检查dfeuer的答案是否足以满足您的需要)。

该解决方案使用了基座上的GHC.TypeLits模块，以及http://hackage.haskell.org/package/typelits-witnesses-0.2.3.0包。

下面是一个差分函数，它接受两个整数参数(静态已知)，并在编译时抱怨第一个数字大于第二个整数：

{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language DataKinds #-}
{-# language ScopedTypeVariables #-}

import GHC.TypeLits
import GHC.TypeLits.Compare
import Data.Type.Equality
import Data.Proxy
import Control.Applicative

difference :: forall n m. (KnownNat n,KnownNat m,n <= m) 
           => Proxy n 
           -> Proxy m 
           -> Integer
difference pn pm = natVal pm - natVal pn

我们可以从GHCi查看它：

ghci> import Data.Proxy
ghci> :set -XTypeApplications
ghci> :set -XDataKinds
ghci> difference (Proxy @2) (Proxy @7)
5
ghci> difference (Proxy @7) (Proxy @2)
** TYPE ERROR **

但是，如果我们想使用在运行时确定的值的函数呢？比如说，我们从控制台或文件中读取的值？

main :: IO ()
main = do
   case (,) <$> someNatVal 2 <*> someNatVal 7 of
       Just (SomeNat proxyn,SomeNat proxym) ->
            case isLE proxyn proxym of
                Just Refl -> print $ difference proxyn proxym 
                Nothing   -> error "first number not less or equal"
       Nothing ->     
            error "could not bring KnownNat into scope"

在本例中，我们使用像someNatVal和isLE这样的函数。这些函数在Nothing中可能会失败。但是，如果他们成功了，他们会返回一个“见证”某种约束的值。通过对证人的模式匹配，我们将该约束带入范围(这是因为证人是一个GADT)。

在本例中，Just (SomeNat proxyn,SomeNat proxym)模式匹配将两个参数的KnownNat约束带入范围。Just Refl模式匹配将n <= m约束带入范围。只有这样，我们才能调用我们的difference函数。

因此，在某种程度上，我们已经转移了所有的工作，以确保论点满足所需的先决条件，而不是功能本身。

Answer 3

你想要的是依赖型。在https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell中有一个很好的教程

虽然我不知道这会有多友好。请注意，在GHC8.0中，依赖类型得到了改进，但我在这方面没有经验。如果您不想让模板Haskell变得繁琐，我会确保您使用模板Haskell很舒服。