¿Se pueden implementar unidades de medida F#en OCaml?
units-of-measurement (2)
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 que las unidades se definan 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 las conversiones (supongo que eso significa que Measure tiene algunas funciones definidas que permiten que las Medidas se multipliquen, dividan y expongan):
// 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
¿Se podría implementar esta capacidad en OCaml? Alguien sugirió que mire los tipos fantasmas pero no parecen componer de la misma manera que las unidades.
(Divulgación: hice esta pregunta sobre Haskell hace unos meses, recibí una discusión interesante pero no tuve una respuesta definitiva más allá de "probablemente no").
No se puede expresar directamente en la sintaxis del sistema de tipo, pero es posible cierta codificación. Uno ha sido propuesto, por ejemplo, en este mensaje en la lista de la lista https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00069.html . Aquí está el contenido formateado de la respuesta. Por cierto, no veo ninguna razón por la cual esto no sea aplicable a Haskell.
module Unit : sig
type +''a suc
type (+''a, +''b) quantity
val of_float : float -> (''a, ''a) quantity
val metre : (''a, ''a suc) quantity
val mul : (''a, ''b) quantity -> (''b, ''c) quantity -> (''a, ''c) quantity
val add : (''a, ''b) quantity -> (''a, ''b) quantity -> (''a, ''b) quantity
val neg : (''a, ''b) quantity -> (''a, ''b) quantity
val inv : (''a, ''b) quantity -> (''b, ''a) quantity
end = struct
type ''a suc = unit
type (''a, ''b) quantity = float
let of_float x = x
let metre = 1.
let mul x y = x *. y
let add x y = x +. y
let neg x = 0. -. x
let inv x = 1. /. x
end
Esto rastrea con éxito la dimensión de quatidades:
# open Unit;;
# let m10 = mul (of_float 10.) metre;;
val m10 : (''a, ''a Unit.suc) Unit.quantity = <abstr>
# let sum = add m10 m10;;
val sum : (''a, ''a Unit.suc) Unit.quantity = <abstr>
# let sq = mul m10 m10;;
val sq : (''a, ''a Unit.suc Unit.suc) Unit.quantity = <abstr>
# let cube = mul m10 (mul m10 m10);;
val cube : (''a, ''a Unit.suc Unit.suc Unit.suc) Unit.quantity = <abstr>
# let _ = add (mul sq (inv cube)) (inv m10);;
- : (''a Unit.suc, ''a) Unit.quantity = <abstr>
y dará errores si se usan incorrectamente:
# let _ = add sq cube;;
Characters 15-19:
let _ = add sq cube;;
^^^^
Error: This expression has type
(''a, ''a Unit.suc Unit.suc Unit.suc) Unit.quantity
but an expression was expected of type
(''a, ''a Unit.suc Unit.suc) Unit.quantity
The type variable ''a occurs inside ''a Unit.suc
# let _ = add m10 (mul m10 m10);;
Characters 16-29:
let _ = add m10 (mul m10 m10);;
^^^^^^^^^^^^^
Error: This expression has type (''a, ''a Unit.suc Unit.suc) Unit.quantity
but an expression was expected of type (''a, ''a Unit.suc)
Unit.quantity
The type variable ''a occurs inside ''a Unit.suc
Sin embargo, deducirá tipos demasiado restrictivos para algunas cosas:
# let sq x = mul x x;;
val sq : (''a, ''a) Unit.quantity -> (''a, ''a) Unit.quantity = <fun>
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 crear primero 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 resolver estas ecuaciones, lo que da ''a ~ (int * int) list y una ''a ~ (int * int) list 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 la igualdad sintáctica , es decir, si dos cosas son iguales si y solo si están escritas de la misma manera (con una consideración especial para las variables independientes).
El problema con las unidades de medidas es que las ecuaciones que se generan no se pueden resolver de una manera única usando la igualdad sintáctica; la teoría correcta para usar es la teoría de los grupos abelianos (inversas, elemento de identidad, operación conmutativa). Por ejemplo, las unidades de medida m * s * s⁻¹ deben ser equivalentes a m . Existe 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 se deduce que y tiene un tipo float<''_a> -> float<''b * ''_a⁻¹> , en lugar del tipo más general float<''a> -> float<''b * ''a⁻¹>
De todos modos, para obtener más información, recomiendo leer el capítulo 3 de la siguiente tesis doctoral: