Racines carrées sécurisées en unité

Question

Je me demandais simplement comment il est possible d'écrire une fonction racine carrée définie par l'utilisateur (sqrt) de manière à interagir correctement avec les unit system de F #.

Ce qu'il devrait être comme:

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

Mais ce n'est pas autorisée en raison de constantes non nulles ne sont pas autorisés à avoir des unités génériques.

Existe-t-il un moyen d'écrire cette fonction? Avec le sqrt intégré ça fonctionne bien, alors quelle magie fait-il?

Answer 1

En autorisant des constantes génériques non nulles, il serait très facile de rompre la sécurité du système de types pour les unités (voir le document papers d'Andrew Kennedy). Je crois que la réponse à votre dernière question est que sqrt est en effet magique dans un certain sens en ce sens qu'il ne devrait pas être possible de définir une fonction paramétrique avec cette signature de type par des moyens normaux. Cependant, il est possible de faire ce que vous voulez (au moins dans la version actuelle de F #) en tirant parti de la boxe et de la coulée:

let sqrt (x : float<'u^2>) = 
    let x' = (float x) ** 0.5 (* delete unit and calculate sqrt *) 
    ((box x') :?> float<'u>) 

Answer 2

@kvb est juste, plus généralement:

Si vous avez un algorithme qui ne soit pas unitaire (par exemple, vous écrivez 'cube root'), et vous voulez y placer des unités, vous pouvez envelopper l'algorithme dans une fonction avec la bonne signature de type et utiliser par exemple "flotter" pour "rejeter" les unités au fur et à mesure qu'elles arrivent et l'approche "boîte-et-downcast" pour "rajouter" les unités appropriées à la sortie. Dans la version RTM (après Bêta2), F # aura des fonctions de bibliothèque primitives pour les 'unités de retour', puisque l'approche de boîte-et-downcast est actuellement un peu un hack pour surmonter l'absence de ces primitives dans la langue/bibliothèque.