целочисленные значения уровня в ocaml

Question

Может ли кто-нибудь дать мне предложения / советы по созданию целых чисел уровня типа в OCaml (3.12), поддерживающих операции сложения и вычитания над ними?

Например, если у меня есть числа, представленные так:

type zero
type 'a succ
type pos1 = zero succ
type pos2 =  zero succ succ
...

Мне нужен способ определения функции для таких типов, как этот:

val add: pos2 -> pos1 -> pos3

Небольшая предыстория: я пытаюсь перенести некоторый код на haskell для операций над физическими измерениями, и мне нужна возможность определять операциина типах измерений (запись 7-ти уровней типа, представляющих показатели 7 базовых единиц СИ).Мне нужно сделать это таким образом, чтобы избежать динамического связывания (при использовании объектов) и дать возможность компилятору статически оценивать и проверять все такие выражения.

В настоящее время я понимаю, что мне следует создать GADT, который реализует операции как типконструкторы, но все же я борюсь с этой идеей, и любая подсказка будет принята с благодарностью.

Answer 1

Вас также может заинтересовать статья Много отверстий в Хиндли-Милнере , Сэм Линдли, из Семинара 2008 года по ML.

Answer 2

Возможно, вы сможете использовать одну из многих удивительных конструкций Олега: http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html

У Джейн-стрит есть еще одно предложение с использованием первоклассных модулей.

http://ocaml.janestreet.com/?q=node/81

Отказ от ответственности: я в основном восхищаюсь этим видом программирования издалека.

Answer 3

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

type fancyInt = Zero | Succ of fancyInt ;;

тогда добавить будет

let rec add a b = match a with Zero -> b | Succ c -> add c (Succ b);;

Ваш фоновый рассказ намекает на другое решение, создайте класс, который представляет расстояния. Внутренне сохраняйте значение, однако вам необходимо предоставить интерфейс, который позволит вам получить и установить расстояние в единицах, необходимых в данный момент. Или, если вы хотите остаться с функциональным подходом, просто создайте типы для ваших юнитов, а затем используйте функции так же, как сам Ocaml обрабатывает такие вещи, т.е.