Des unités de mesure F # peuvent-elles être implémentées dans OCaml?

Question

F# est une des unités de mesure de capacité (il n'y a plus de détails dans ce document de recherche).

[<Measure>] type unit-name [ = measure ]

Cela permet aux unités d'être définie comme:

type [<Measure>] USD
type [<Measure>] EUR

Et le code pour être écrite comme suit:

let dollars = 25.0<USD>
let euros = 25.0<EUR>

// Results in an error as the units differ
if dollars > euros then printfn "Greater!"

Il gère aussi les conversions (je suppose que les moyens de Mesure a certaines fonctions définies qui permettent des Mesures soient multipliés, divisé et exponentiated):

// Mass, grams.
[<Measure>] type g
// Mass, kilograms.
[<Measure>] type kg

let gramsPerKilogram : float<g kg^-1> = 1000.0<g/kg>

let convertGramsToKilograms (x : float<g>) = x / gramsPerKilogram

Pourrait cette capacité d'être mis en œuvre en OCaml? Quelqu'un a suggéré que je regarde types fantômes, mais ils n'apparaissent pas à composer de la même manière que les unités.

(Divulgation: j'ai posé cette question à propos de Haskell il y a quelques mois, a eu une discussion intéressante à ce sujet mais pas de réponse définitive au-delà de "probablement pas").

Answer 1

Réponse rapide: Non, c'est au-delà des capacités actuelles de l'inférence de type OCaml.

Pour expliquer un peu plus: l'inférence de type, dans la plupart des langages fonctionnels est basé sur un concept appelé à l'unification, qui est vraiment juste une façon particulière de résoudre des équations. Par exemple, déduire le type d'une expression comme

let f l i j =
  (i, j) = List.nth l (i + j)

implique d'abord la création d'un ensemble d'équations (où les types d' l, i et j sont 'a, 'b et 'c respectivement, et List.nth : 'd list -> int -> 'd, (=) : 'e -> 'e -> bool, (+) : int -> int -> int):

'e ~ 'b * 'c
'a ~ 'd list
'b ~ int
'c ~ int
'd ~ 'e

et puis la résolution de ces équations, ce qui donne 'a ~ (int * int) list et f : (int * int) list -> int -> int -> bool. Comme vous pouvez le voir, ces équations ne sont pas très difficiles à résoudre; en fait, la seule théorie de l'unification est syntaxique de l'égalité, c'est à dire si deux choses sont égales si et seulement si elles sont écrites de la même façon (avec une attention particulière pour unbound variables).

Le problème avec les unités de mesures est que les équations qui sont générés ne peuvent pas être résolus d'une manière unique à l'aide syntaxique de l'égalité; la théorie correcte à utiliser est la théorie de la Abéliennes groupes (inverses, de l'identité de l'élément, opération commutative). Par exemple, les unités de mesure m * s * s⁻¹ doit être équivalent à m. Il est une complication de plus quand il s'agit de principaux types et laissez-la généralisation. Par exemple, la suite n'est pas de type case en F#:

fun x -> let y z = x / z in (y mass, y time)

parce qu' y est déduite de type float<'_a> -> float<'b * '_a⁻¹>, au lieu du type plus général float<'a> -> float<'b * 'a⁻¹>

De toute façon, pour plus d'informations, je vous recommande la lecture du chapitre 3 de la suite de la thèse de Doctorat:

https://personal.cis.strath.ac.uk/adam.gundry/thesis/thesis-2013-12-03.pdf