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?
-
6Why you need 2 parameters then?kennytm– kennytm2010-07-10 17:52:23 +00:00Commented Jul 10, 2010 at 17:52
-
2Can't you have the function take one argument, and assume the other number is 1.618 times greater?Michał Trybus– Michał Trybus2010-07-10 17:52:52 +00:00Commented Jul 10, 2010 at 17:52
-
1You can't enforce that at compile time (with two parameters) -- and, as you point out, would be no guard against user input. Here is a counter-challenge given two numbers, x and y, write a function to return true iff they form the golden ratio. Now, alter it to return some golden ratio or nothing, as appropriate.user166390– user1663902010-07-10 17:59:22 +00:00Commented Jul 10, 2010 at 17:59
-
2Don't get too caught up in a bad example. If it helps imagine x and y are a message and salted hash. I only want to execute myfun if the salted hash of x matches y. Lets say I have 10 more functions that need this invariant also, can the type system guarantee it?Jason Christa– Jason Christa2010-07-10 18:09:20 +00:00Commented Jul 10, 2010 at 18:09
-
3Here is a functional design pattern that probably has the trade-off you are looking for: lukepalmer.wordpress.com/2009/03/24/certificate-design-pattern You can go fully into type verification with a dependently-typed total language like Agda or Coq, but in their current state of the art they are still very hard to program in.luqui– luqui2010-07-10 18:54:05 +00:00Commented Jul 10, 2010 at 18:54
3 Answers
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 ???.
10 Comments
data Gold = G Double Double if you want to use a fixed type; you'll never find two Integers that satisfy the golden ratio.Gold was exported without its constructors so unless you want an unnecessarily explicit (), I'm not sure what you want. Kenny: Obviously this doesn't run as there are omitted functions for the asker to fill in along with myfun not actually being in a module or importing anything. The concept of ADTs is what's important.a/b == golden and instead need some sort of approximate equality or boolean test which I called 'isGolden'.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.
1 Comment
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 -> Maybe 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.
8 Comments
myfun.inputA <- getLine; inputB <- getLine; let [numA, numB] = map read [inputA, inputB] :: [Double]; magicRatioFunction numA numB