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

Question

我公开了一个带有两个参数的函数,一个是最小边界,另一个是最大边界.如何使用类型确保例如最小边界不大于最大边界？

我想避免创建一个智能构造函数并返回一个Maybe,因为它会使整个使用更麻烦.

谢谢

Answer 1

这并不能完全回答您的问题,但有时可行的一种方法是更改​​您对类型的解释.例如,而不是

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

你可以用

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

这样,就无法表示无效范围.

Answer 2

此解决方案使用依赖类型(并且可能过于重量级,请检查dfeuer的答案是否足以满足您的需求).

该解决方案使用了base的GHC.TypeLits模块,以及typelits-witnesses包的模块.

这是一个差异函数,它接受两个整数参数(静态已知),并在第一个数字大于第二个时在编译时抱怨:

{-# 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功能.

因此,在某种程度上,我们已经转移了所有繁忙的工作,确保参数满足函数本身所需的前提条件.