Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Unit-safe square roots

I just wondered how it is possible to write a user-defined square root function (sqrt) in a way that it interacts properly with F#'s unit system.

What it should be like:

let sqrt (x : float<'u ^ 2>) =
    let x' = x / 1.0<'u ^ 2> // Delete unit
    (x ** 0.5) * 1.0<'u>     // Reassign unit

But this is disallowed due to nonzero constants not being allowed to have generic units.

Is there a way to write this function? With the builtin sqrt it works fine, so what magic does it perform?

like image 630
Dario Avatar asked Feb 03 '23 09:02

Dario


2 Answers

Allowing nonzero generic constants would make it very easy to break the safety of the type system for units (see Andrew Kennedy's papers). I believe that the answer to your last question is that sqrt is indeed magic in some sense in that it shouldn't be possible to define a parametric function with that type signature through normal means. However, it is possible to do what you want (at least in the current version of F#) by taking advantage of boxing and casting:

let sqrt (x : float<'u^2>) =
  let x' = (float x) ** 0.5 (* delete unit and calculate sqrt *)
  ((box x') :?> float<'u>)
like image 168
kvb Avatar answered Feb 08 '23 03:02

kvb


@kvb is right, more generally:

If you have a non-unit aware algorithm (e.g. say you write 'cube root'), and you want to put units on it, you can wrap the algorithm in a function with the right type signature and use e.g. "float" to 'cast away' the units as they come in and the box-and-downcast approach to 'add back' the appropriate units on the way out.

In the RTM release (after Beta2), F# will have primitive library functions for the 'add back units', since the box-and-downcast approach is a currently bit of a hack to overcome the lack of these primitives in the language/library.

like image 40
Brian Avatar answered Feb 08 '23 02:02

Brian