CODEWITHSUNDEEP
haskell
McBear Holden
McBear Holden

Reputation: 5901

How to limit a Int field to a range of values?

In my Data

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

I want to limit uRank to a list of values [-1, 1, 3], for example.

How do I do this?

Upvotes: 9

Views: 2866

Answers (3)

Thomas M. DuBuisson
Thomas M. DuBuisson

Reputation: 64740

Liquid Haskell, which adds refinement types on top of Haskell, can do this. See the correct section of the tutorial here.

First you define your data type as normal.

module User where

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

Next we define your restriction as a refinement type. Liquid Haskell users comment annotations with syntax {-@ blah @-}. We'll define your odd restriction of -1, 1, 3 first with the RestrictedInt type:

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

That is, the RestrictedInt is an Int that is either -1, 1, or 3. Notice you could easily write ranges and other restrictions, it doesn't have to be some mindless enumeration of legitimate values.

Now we re-define your data type in our refinement language using this restricted int type:

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

This is similar to your definition but with the restriction type instead of just Int. We could have inlined the restriction instead of having a type alias but then your User data type would be pretty unreadable.

You can define good values and the liquid tool will not complain:

goodValue :: User
goodValue = User 1 12

But bad values result in an error:

badValue :: User
badValue = User 10 12

$ liquid so.hs (or your editor's integration, if you have that setup) produces:

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

Upvotes: 5

ephrion
ephrion

Reputation: 2697

Defining a small sum type is the best answer for this specific question. You can also use newtype with smart constructors 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, provided you only use the safe mkRank constructor, you can assume that your Rank values have the Int values you want.

Upvotes: 10

chepner
chepner

Reputation: 530823

For something so small, you should define a precise type:

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

Haskell doesn't force you to encode everything as a subset of the integers; take advantage of it!

For larger subsets where this would be unwieldy, you are looking for a dependent type, which (until recently?) is not supported by Haskell directly.

Upvotes: 8

Related Questions