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

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

Answer 1

您可能还对文章感兴趣 Many Holes in Hindley-Milner ，作者 Sam Lindley，来自 2008 年 ML 研讨会。