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

我目前的理解是我应该创建一个GADT来实现作为类型构造函数的操作,但我仍然在努力实现这个想法,任何提示都会受到高度赞赏.

Answer 1

您可能也对2008年ML研讨会上的Sam Lindley 撰写的文章Hindley-Milner的许多孔感兴趣。