novembre
2010
Hello everyone,
Yesterday, a pretty young woman told me that writing about programming languages really need to be done in English. Now that I know she reads my humble texts, I have to follow its advice. So now… let’s be a bit more serious.
As you probably know, polymorphic variants are often seen as a light and elegant alternative to OCaml constructors. Yet these two concepts are not completely interchangeable : that is why they coexist in OCaml. Here I describe a possible use of polymorphic variants to refine some function signatures from the OCaml standard library by adding type constraints.
Too simple to be safe ?
To make things clearer, let’s consider the example of floating-point numbers (or simply floats) and their corresponding OCaml type. The core module defines many functions which deal with floats, such as square root (sqrt
) and exponential (exp
). Both have the same signature :
val sqrt : float -> float val exp : float -> float
This short signature means that the function receives a floating-point number as argument and returns a floating-point number as result. Now try to remember your math lessons. You should probably know that exponential is defined from R to R+, whereas square root is defined from R+ to R+. In other words, there is no way to compute the square root of strictly negative numbers. As a consequence, we expect the sqrt
function to raise an exception when the input value is negative. Actually, instead of raising an exception, the IEEE 754 standard introduces a special float value called NaN
(not a number) to handle these cases.
# let x = -3.5;; val x : float = -3.5 # exp x;; - : float = 0.0301973834223185 # sqrt x;; - : float = nan
Due to its special status, NaN
is only able to spread again and again through successive computations, so that the final value is always NaN
. This is a convenient solution… but we can also try to get more explicit signatures. This can be achieved with polymorphic variants (this is false suspense before true headache).
The strange world of polymorphic variants
Polymorphic variants are quite subtle stuff that I cannot explain in one short sentence. Therefore, people who are not familiar with this concept should refer to the OCaml manual (politeness for RTFM). For the others, the only thing I really expect you to know by heart is that [> `Foo]
means « at least `Foo, but maybe something else », whereas [< `Foo | `Bar]
means « nothing more than `Foo
and `Bar
». This is the key of what we are going to do in this short article. So first, let’s define a new type :
type ‘a t = ‘a * float
The polymorphic parameter will be used to add some flags to the float value. These flags are polymorphic variants. Of course, the whole definition will be left abstract in the module signature. Then we need two functions for building positive and negative numbers floats, and a specialized value for zero :
let zero = (‘Nil, 0.0) let positive flo = if flo > 0. then (‘Pos, flo) else invalid_arg "positive" let negative flo = if flo < 0. then (‘Neg, flo) else invalid_arg "negative"
These functions have quite clear signatures :
val zero : [> ‘Nil] t val positive : float -> [> ‘Pos] t val negative : float -> [> ‘Neg] t
Note the use of >
in the above signatures and try to understand its aim. Then let’s write another function to convert a given t
value to floating-point number :
let to_float = snd
And that’s all ! We are now able to make things a bit safer. One example :
let sqrt = function ‘Nil, _ -> zero | ‘Pos, x -> (‘Pos, sqrt x)
This new sqrt
function has a fairly explicit (maybe also cryptic) signature :
val sqrt : [< ‘Nil | ‘Pos] t -> [> ‘Nil | ‘Pos] t
It just means that sqrt expects a non-negative float (either `Nil
or `Pos
) and returns a non-negative float. Wonderful ! Now we can write many more float-related functions :
let exp t = (‘Pos, exp (to_float t)) let log (‘Pos, x) = let r = log x in if r = 0. then zero else if r < 0. then (‘Neg, x) else (‘Pos, x) let abs t = let flo = abs_float (to_float t) in if flo = 0. then zero else (‘Pos, flo)
and their signatures :
val exp : [< ‘Neg| ‘Nil | ‘Pos] t -> [> ‘Pos] t val log : [‘Pos] t -> [> ‘Neg| ‘Nil | ‘Pos] t val abs : ‘a t -> [> ‘Nil | ‘Pos] t
We cannot do unsafe computations by composing functions anymore. For instance, the following code is rejected at compile time :
let sqrt_log x = sqrt (log x) ^^^^^^^ Error: This expression has type ([> `Neg | `Nil | `Pos ] as 'a) t = 'a * float but an expression was expected of type ([< `Nil | `Pos ] as 'b) t = 'b * float The second variant type does not allow tag(s) `Neg
The compiler is complaining because log
can return negative values, and sqrt
cannot handle them. We should thus write something like this :
type nonneg = [`Nil | `Pos] let sqrt_log x = match log x with | `Neg, _ -> None | #nonneg, _ as y -> Some (sqrt y)
and we get the following signature :
val sqrt_log : [ `Pos ] t -> [> `Nil | `Pos ] t option
That’s all folks !
Cacophrène
The resulting types seem to be a bit more precise than the option monad alone, but you are right, this is just a tricky toy. I don’t expect to use it in real life. However, it was so fun to think about it.
It does not scale well to encode constraints in numeric types.
Soon nearly all operations will return an option type.
That basically mean you are using the option monad.
And the option monad is just a replacement for disciplined exception.