Могут ли единицы измерения F # быть реализованы в OCaml?

F # имеет единицы измерения меры (более подробно в этом исследовательском документе).

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

Это позволяет определять единицы измерения, такие как:

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

И код, который будет записан как:

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

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

Он также обрабатывает конверсии (я предполагаю, что означает, что "Мера" имеет определенные функции, которые позволяют умножать, делить и экспонировать Меры):

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

Может ли эта возможность быть реализована в OCaml? Кто-то предложил мне посмотреть на типы phantom, но они, похоже, не составлены так же, как единицы.

(Раскрытие информации: Я задал этот вопрос о Хаскелле несколько месяцев назад, получил интересную дискуссию, но окончательный ответ не был "вероятно, нет" ).

Ответ 1

Быстрый ответ: Нет, это вне возможностей текущего вывода типа OCaml.

Объяснить это немного больше: вывод типа в большинстве функциональных языков основан на концепции, называемой унификацией, которая на самом деле является лишь конкретным способом решения уравнений. Например, выведя тип выражения типа

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

включает сначала создание набора уравнений (где типы l, i и j равны 'a, 'b и 'c соответственно, и List.nth : 'd list -> int -> 'd, (=) : 'e -> 'e -> bool, (+) : int -> int -> int):

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

а затем решая эти уравнения, что дает 'a ~ (int * int) list и f : (int * int) list -> int -> int -> bool. Как вы можете видеть, эти уравнения не очень трудно решить; на самом деле единственной теорией, лежащей в основе унификации, является синтаксическое равенство, т.е. если две вещи равны тогда и только тогда, когда они написаны одинаково (с особым учетом несвязанных переменных).

Проблема с единицами измерения состоит в том, что генерируемые уравнения не могут быть решены уникальным образом с использованием синтаксического равенства; правильной теорией для использования является теория абелевых групп (обратные, единичный элемент, коммутативная операция). Например, единицы измерения m * s * s⁻¹ должны быть эквивалентны m. Существует еще одно осложнение, когда речь идет о основных типах и let-generalization. Например, следующее не проверяет тип F #:

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

поскольку y выводится тип float<'_a> -> float<'b * '_a⁻¹>, а не более общий тип float<'a> -> float<'b * 'a⁻¹>

Во всяком случае, для получения дополнительной информации, я рекомендую прочитать главу 3 следующей докторской диссертации:

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

Ответ 2

Он не может быть непосредственно выражен в синтаксисе системы типов, но возможна некоторая кодировка. Один из них был предложен, например, в этом сообщении в caml-списке https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00069.html. Вот сформированный контент ответа. Кстати, я не вижу причин, почему это не применимо к 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

Это успешно отслеживает размерность четности:

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

и он будет давать ошибки, если они используются неправильно:

# 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

Однако для некоторых вещей он будет вызывать слишком ограничительные типы:

# let sq x = mul x x;;
val sq : ('a, 'a) Unit.quantity -> ('a, 'a) Unit.quantity = <fun>