任何人都可以给我提出有关在OCaml(3.12)中支持加法和减法操作的类型级整数的建议/建议吗？
例如,如果我有这样的数字:
type zero
type 'a succ
type pos1 = zero succ
type pos2 = zero succ succ
...
我需要一种方法来定义类型的函数,如下所示:
val add: pos2 -> pos1 -> pos3
小背景:我正在尝试为物理维度上的操作移植一些haskell代码,并且我需要能够在维度类型上定义操作(记录7个类型级别的int代表7个基本SI单位的指数).我需要这样做以避免动态绑定(使用对象时)并使编译器能够静态地评估和检查所有这些表达式.
我目前的理解是我应该创建一个GADT来实现作为类型构造函数的操作,但我仍然在努力实现这个想法,任何提示都会受到高度赞赏.