types - 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 个基本 SI 单位的指数）。我需要这样做以避免动态绑定（使用对象时）并使编译器能够静态评估和检查所有此类表达式。

我目前的理解是，我应该制作一个将操作实现为类型构造函数的 GADT，但我仍然在为这个想法苦苦挣扎，任何提示都将不胜感激。

score 5 · Accepted Answer

您可能还对2008 年 ML 研讨会上 Sam Lindley撰写的文章Many Holes in Hindley-Milner感兴趣。

score 3 · Accepted Answer

Jane Street 有另一个使用一流模块的建议。

免责声明：我很欣赏这种远距离的编程。

score 0 · Accepted Answer

你的例子让我觉得你正在尝试做序言风格的逻辑数字，就像

type fancyInt = Zero | Succ of fancyInt ;;

然后添加将是

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

你的背景故事暗示了一个不同的解决方案，创建一个代表距离的类。在内部存储该值，但是您需要提供一个接口，该接口允许您以当时所需的单位获取和设置距离。或者，如果您想继续使用函数式方法，只需为您的单元创建类型，然后拥有与 Ocaml 本身处理此类事情相同的函数，即meters_of_km。

3 回答 3