ocaml中的类型级别整数 [英] type level integers in ocaml

问题描述

有人可以给我关于在OCaml(3.12)中制作类型级别整数以支持对其进行加减运算的建议吗?

Could anyone give me suggestions/advice on making type level integers in OCaml (3.12) supporting addition and subtraction operations on them?

例如，如果我有这样表示的数字:

For example, if I have numbers represented like this:

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

我需要一种在这样的类型上定义函数的方法:

I need a way to define function on types like this:

val add: pos2 -> pos1 -> pos3

小背景: 我正在尝试为物理尺寸上的操作移植一些haskell代码，并且我需要能够定义尺寸类型上的操作(代表7个基本SI单位指数的7个类型级整数的记录). 我需要通过这种方式来避免动态绑定(使用对象时)，并使编译器能够静态评估和检查所有此类表达式.

Little background: I'm trying to port some haskell code for operations on physical dimensions and i need the ability to define operations on dimension types (record of 7 type level ints representing exponents of 7 basic SI units). I need to do it this way to avoid dynamic binding (when using objects) and to enable compiler to evaluate and check all such expressions statically.

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

My current understanding is that I should make a GADT that implements operations as type constructors, but still I'm struggling with the idea, and any hint would be greatly appreciated.

推荐答案

您可能也对文章

You may also be interested in the article Many Holes in Hindley-Milner, by Sam Lindley, from the 2008 Workshop on ML.

这篇关于ocaml中的类型级别整数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！