10

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

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

谢谢

4

4 回答 4

16

这并不能完全回答您的问题，但有时有效的一种方法是改变您对类型的解释。例如，而不是

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

你可以使用

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

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

于 2016-10-01T21:55:40.487 回答
10

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

该解决方案利用了baseGHC.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函数。

因此，在某种程度上，我们已经将确保参数满足所需先决条件的所有繁琐工作从函数本身移出。

于 2016-10-01T22:52:58.707 回答
1

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

虽然不知道会有多友好。请注意，依赖类型在 GHC 8.0 中得到了改进，但我在这方面没有经验。如果您不希望它很麻烦，我会确保您对使用模板 Haskell 感到满意。

于 2016-10-01T21:44:05.377 回答
1

您无需调用该Maybe类型即可利用“智能构造函数”。如果你愿意，你可以接受任何一种形式的构造函数，或者(min,max)仍然(max,min)创建一个data正确解释哪个是哪个的类型。

例如，您可以制作一个小模块：

module RangeMinMax (
               Range,
               makeRange
              )
where

data Range = Range (Integer,Integer)
  deriving Show
makeRange a b = Range (min a b, max a b)

现在，当您创建RangeusingmakeRange时，2 元组将自动排列，因此它的形式为(min,max)。请注意，for 的构造函数Range未导出，因此模块的用户无法创建无效的Range- 您只需要确保在此模块中创建有效的。

于 2016-10-02T06:34:52.043 回答