How to limit the Int field to a number of values?

Question

In my data

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

I want, for example, to limit the uRanklist of values ​​[-1, 1, 3].

How to do it?

Answer 1

Defining a small amount type is the best answer to this particular question. You can also use newtypewith smart designers to achieve this effect.

newtype Rank = UnsafeMkRank { unRank :: Int }

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

Now, if you use only the safe constructor mkRank, you can assume that your values Rankhave the values Intyou want.

Answer 2

For something so small, you have to define the exact type:

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

Haskell does not force you to encode everything as a subset of integers; use it!

, , , ( ?) 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 }
  @-}

This is similar to your definition, but with a restriction type instead Int. We could include a constraint instead of having a type alias, but then your data type Userwould be pretty unreadable.

You can determine good values ​​and the tool liquidwill not complain:

goodValue :: User
goodValue = User 1 12

But bad values ​​lead to an error:

badValue :: User
badValue = User 10 12

$ liquid so.hs (or your integration with the editor, if you have this setting):

**** 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)}