Jak ograniczyć pole Int do zakresu wartości?

Question

moim danych

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

że chcemy ograniczać uRank z listy wartości [1, 1, 3], na przykład.

Jak to zrobić?

Answer 1

Określenie typu małej sumy jest najlepszą odpowiedzią na to konkretne pytanie. Możesz również użyć newtype z inteligentnymi konstruktorami, aby osiągnąć ten efekt.

newtype Rank = UnsafeMkRank { unRank :: Int } 

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

Teraz, pod warunkiem korzystania tylko bezpieczne mkRank konstruktora, można przyjąć, że wartości Rank mają wartości Int chcesz.

Answer 2

Na coś tak małe, należy określić dokładny typ:

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

Haskell nie zmusza cię do kodowania wszystko jako podzbiór liczb całkowitych; wykorzystaj to!

Dla większych podzbiorów gdzie byłoby to trudne, szukasz utrzymaniu typu, które (jeszcze do niedawna?) Nie jest obsługiwany przez Haskell bezpośrednio.

Answer 3

Ciecz Haskell, który dodaje typy udoskonalania na górze Haskell, może to zrobić. Zobacz odpowiednią sekcję samouczka: here.

Najpierw określ typ danych jako normalny.

module User where 

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

Następnie definiujemy twoje ograniczenie jako typ udoskonalenia. Użytkownicy Liquid Haskell komentują adnotacje o składni {-@ blah @-}. Będziemy zdefiniować dziwne ograniczenie -1, 1, 3 pierwszy z typem RestrictedInt:

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

Oznacza to, że RestrictedInt jest Int że jest albo -1, 1 lub 3. Zauważ, że możesz łatwo pisać zakresy i inne ograniczenia, nie musi to być bezmyślne wyliczanie prawowitych wartości.

Teraz ponownie określić typ danych w naszym języku wyrafinowanie przy użyciu tego typu int ograniczony:

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

ta jest podobna do definicji ale z typem restrykcyjnym, a nie tylko Int. Moglibyśmy wprowadzić ograniczenie zamiast mieć alias typu, ale wtedy twój typ danych byłby całkiem nieczytelny.

Można zdefiniować dobre wartości i narzędzie liquid nie będzie narzekać:

goodValue :: User 
goodValue = User 1 12 

Ale złe wartości powodują błąd:

badValue :: User 
badValue = User 10 12 

$ liquid so.hs (lub integracja edytora, o ile trzeba, że setup) produkuje:

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