¿Se pueden implementar unidades de medida F# en OCaml?

Question

¿Se pueden implementar unidades de medida F# en OCaml?

F # tiene una capacidad de unidades de medida (hay más detalles en este documento de investigación ).

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

Esto permite definir unidades tales como:

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

Y el código se escribirá como:

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

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

También maneja conversiones (supongo que significa que Measure tiene algunas funciones definidas que permiten que las Medidas se multipliquen, dividan y exponencien):

// 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

¿Podría implementarse esta capacidad en OCaml? Alguien sugirió que mire tipos fantasma pero no parecen componer de la misma manera que las unidades.

(Revelación: Hice esta pregunta sobre Haskell hace unos meses, obtuve una discusión interesante pero ninguna respuesta definitiva más allá de 'probablemente no').

40

units-of-measurement f#ocaml

Author: Darren, 0000-00-00

Source

1 answers

score 4 · Accepted Answer

Respuesta rápida: No, eso está más allá de las capacidades de la inferencia de tipo OCaml actual.

Para explicarlo un poco más: la inferencia de tipos en la mayoría de los lenguajes funcionales se basa en un concepto llamado unificación, que en realidad es solo una forma específica de resolver ecuaciones. Por ejemplo, inferir el tipo de una expresión como

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

Implica primero crear un conjunto de ecuaciones (donde los tipos de l, i y j son 'a, 'b y 'c respectivamente, y List.nth : 'd list -> int -> 'd, (=) : 'e -> 'e -> bool, (+) : int -> int -> int):

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

Y luego resolviendo estas ecuaciones, que producen 'a ~ (int * int) list y f : (int * int) list -> int -> int -> bool. Como puede ver, estas ecuaciones no son muy difíciles de resolver; de hecho, la única teoría subyacente a la unificación es igualdad sintáctica, es decir, si dos cosas son iguales si y solo si están escritas de la misma manera (con especial consideración para las variables no ligadas).

El problema con las unidades de medida es que las ecuaciones que se generan no se pueden resolver en un la teoría correcta a usar es la teoría de los grupos abelianos (inversos, elemento de identidad, operación conmutativa). Por ejemplo, las unidades de medida m * s * s⁻¹ deben ser equivalentes a m. Hay una complicación adicional cuando se trata de tipos principales y let-generalización. Por ejemplo, lo siguiente no escribe-check in F#:

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

Porque y se infiere que tiene el tipo float<'_a> -> float<'b * '_a⁻¹>, en lugar del tipo más general float<'a> -> float<'b * 'a⁻¹>

De todos modos, para más información, recomiendo leer el capítulo 3 de la siguiente tesis doctoral:

Http://adam.gundry.co.uk/pub/thesis/thesis-2013-12-03.pdf