如何将Int字段限制为一系列值？

Question

在我的数据中

data User = User { uRank :: Int, uProgress :: Int }

我想限制uRank一个值列表[-1,1,3],例如.

我该怎么做呢？

Answer 1

定义一个小和类型是这个特定问题的最佳答案.您还可以使用newtype智能构造函数来实现此效果.

newtype Rank = UnsafeMkRank { unRank :: Int }

mkRank :: Int -> Maybe Rank
mkRank i 
    | i `elem` [-1, 1, 3] = Just (UnsafeMkRank i)
    | otherwise = Nothing

现在,如果您只使用安全mkRank构造函数,则可以假设您的Rank值具有所需的Int值.

Answer 2

对于这么小的东西,你应该定义一个精确的类型:

data Rank = RankNegOne | RankOne | RankThree  -- There are probably better names
data User = User { uRank :: Rank, uProgress :: Int }

Haskell不会强迫您将所有内容编码为整数的子集; 利用它!

对于较大的子集,这将是一个笨重的,你正在寻找一个依赖类型,直到最近？？Haskell不支持.

Answer 3

Liquid Haskell在Haskell之上添加了细化类型,可以做到这一点.请在此处查看教程的正确部分.

首先,您可以正常定义数据类型.

module User where

data User = User { uRank     :: Int
                 , uProgress :: Int
                 }

接下来,我们将您的限制定义为细化类型.Liquid Haskell用户使用语法注释注释{-@ blah @-}.我们将-1, 1, 3使用RestrictedInt类型定义您的奇怪限制:

{-@ type RestrictedInt = {v : Int | v == -1 || v == 1 || v == 3} @-}

也就是说,RestrictedInt是一个Int要么是-1,1或3.请注意,您可以轻松编写范围和其他限制,它不必是一些无意义的合法值枚举.

现在,我们使用这种受限制的int类型在我们的优化语言中重新定义您的数据类型:

{-@ data User = User { uRank     :: RestrictedInt
                     , uProgress :: Int }
  @-}

这与您的定义类似,但使用限制类型而不仅仅是Int.我们可以内联限制而不是类型别名,但是你的User数据类型将是非常难以理解的.

您可以定义好的值,liquid工具不会抱怨:

goodValue :: User
goodValue = User 1 12

但是错误的值会导致错误:

badValue :: User
badValue = User 10 12

$ liquid so.hs (或者你的编辑器集成,如果你有这个设置)产生:

**** RESULT: UNSAFE ************************************************************


 so.hs:16:12-18: Error: Liquid Type Mismatch

 16 | badValue = User 10 12
                 ^^^^^^^

   Inferred type
     VV : {VV : GHC.Types.Int | VV == ?a}

   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV == (-1)
                                || (VV == 1
                                    || VV == 3)}

   In Context
     ?a := {?a : GHC.Types.Int | ?a == (10 : int)}