Limit the number to a range (Haskell)

Question

I am exposing a function that takes two parameters, one of which is minimal, and the other is maximum. How can I ensure, using types, that, for example, the minimum border is not greater than the maximum?

I want to avoid creating an intelligent constructor and returning Maybe because this will make all use more cumbersome.

thanks

Answer 1

This doesn't exactly answer your question, but one approach that sometimes works is to change your interpretation of your type. For example, instead of

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

you can use

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

Therefore, it is not possible to imagine an invalid range.

Answer 2

This solution uses dependent types (and may be too heavy, check if dfeuer answer is enough for your needs).

The solution uses the GHC.TypeLits module from the database, as well as the typelits-witnesses package.

Here is a difference function that takes two integer arguments (known statically) and complains at compile time when the first number is greater than the second:

 {-# 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 

We can check this from 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 ** 

But what if we want to use a function with values ​​defined at runtime? Say the values ​​we read from the console or from a file?

 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" 

In this case, we use functions such as someNatVal and isLE . These functions may fail with Nothing . However, if they succeed, they return a value that "testifies" to some kind of limitation. And by comparing the patterns with the witness, we bring this restriction into scope (this works because the witness is GADT).

In this example, pattern matching Just (SomeNat proxyn,SomeNat proxym) brings KnownNat constraints for the two arguments to the scope. And matching the Just Refl brings the n <= m constraint into scope. Only then can we call our function difference .

So, in a sense, we have shifted all efforts so that the arguments satisfy the required preconditions from the function itself.

Answer 3

What you request are dependent types. It has a good tutorial https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

Although I do not know how friendly it will be. Please note that dependent typing has been improved in GHC 8.0, but I have no experience in this area. I would make sure that you are comfortable using the Haskell template if you do not want it to be cumbersome.

Answer 4

You do not need to call the Maybe type to use smart constructors. If you want, you can take constructors of any form (min,max) or (max,min) and still create a data type that correctly interprets what is.

For example, you can create a small module:

 module RangeMinMax ( Range, makeRange ) where data Range = Range (Integer,Integer) deriving Show makeRange ab = Range (min ab, max ab) 

And now, when you create a Range using makeRange , the 2-tuple will be automatically organized so that it is in the form (min,max) . Note that the constructor for Range not exported, so the module user cannot create an invalid Range - you just need to make sure that you are creating valid ones in this module.