Using Haskell's types to replace assert statements or if checks in other languages

Question

Sorry if the question is very elementary, I am still very new to Haskell. Lets say I have a function that can only work with two numbers that are in the golden ration (1.618), how do I define the types of myfun x y to take only golden ratio numbers. What happens if I invoke myfun without golden ratio numbers from within my program (a compile error?)? What happens if the call without golden ratio numbers is made at runtime via user input?

Answer 1

The best you can do practically is a run-time check. There could be some type-level calculus I don't know (see luqui's comment), but that's not pratical in Haskell.

You could use an assert, which is what you want to replace,

checker :: a -> b -> Bool
checker x y = x * 1.618 `approxEqual` y

unsafeMyfun :: a -> b -> c
unsafeMyfun x y = assert (checker x y) (doRealThingWith a b)

or return a Maybe a (or Either err a) to avoid exceptions which cannot be caught in pure functions,

myfun :: a -> b -> Just c
myfun x y = do
              guard $ checker x y
              return $ doRealThingWith x y

or use a custom contract type as in Tom's answer etc. In any way, it's not possible to check the constraint in compile time. In fact, due to the IO monad, any compile-time constraint cannot be precise.

Answer 2

You might want an ADT that can only be constructed with golden ratio numbers then write myfun to accept that data type.

I've assumed Integer as a base type, but you could use others (ex: Double or Float) or even be polymorphic.

1) Make the ADT

module Golden (Gold, getGold, buildGold) where

data Gold = G Integer Integer

getGold :: Gold -> (Integer, Integer)
getGold (G x y) = (x, y)

buildGold :: Integer -> Integer -> Maybe Gold
buildGold x y
    | isGolden x y = Just (G x y)
    | otherwise    = Nothing

Notice this module exports the Gold type but not the constructor (namely, not G). So the only way to get a value of type Gold is with buildGold which performs a run-time check - but only one - so the values of Gold can be used and assumed to be a golden ratio by all the consumers without checking.

2) Use the ADT to build myfun

myfun :: Gold -> ???
myfun g = expr
  where (x, y) = getGold g

Now if you try to call myfun with a non-golden number (a value not of type Gold) then you will get a compile time error.

Recap To build golden numbers buildGold function must be used, which forces the number to be checked.

Notice what gets checked when! You have a compile time guarantee that myfun, and all other functions you want to use with Gold, are always provided golden ratios. The program input (from user, network, or where ever) still needs runtime checks and that's what buildGold provides; obviously there's never going to be a program that can promise the human won't type something undesirable.

The alternatives given in the comments to your question are also worthy of consideration. An ADT is slightly heavy weight if all you need is a single function, myfun, that can fail then just have myfun :: (Integer, Integer) -> Maybe ???.

Answer 3

The easiest technique is to use smart constructors, which use a function from Int to GoldenInt, that checks that your values are in the required ratios.

With more effort, you can use type level numbers to ensure that no runtime check is necessary, however, given you're a beginner, I would stick to the smart constructor method.

Tom's answer above is an example of this idiom.