ocaml中的类型级别整数

任何人都可以给我关于在OCaml（3.12）中支持对它们进行加法和减法操作的类型级别整数的建议/建议吗？ocaml中的类型级别整数

举例来说，如果我有这样表示的数字：

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

我需要一种方法来定义的类型的功能是这样的：

val add: pos2 -> pos1 -> pos3

小背景：我试图端口一些haskell代码的物理维度上的操作，我需要能够定义尺寸类型（表示7个基本国际单位指数的7个级别整数的记录）的操作。我需要这样做，以避免动态绑定（使用对象时）并使编译器能够静态评估和检查所有这些表达式。

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

来源

2011-08-30 etaoin

您可能还会对Sam Lindley的文章Many Holes in Hindley-Milner感兴趣。

来源

2011-08-31 16:15:47

我只是看着这些幻灯片;这个想法很简单，很酷。但在我看来，它只处理类型级别的添加。我没有看到一种方法可以在保持简单性的同时使它适用于减法。如果你跟踪国际单位，我想你需要减法（和负整数）。 –

@Jeffrey我很抱歉给我这么慢的想法，但你知道OCaml有一个“GADT”分支，对不对？ https://sites.google.com/site/ocamlgadt/（显然，根据该页面，我们得到他们与3.13）。 –

是的，我听说3.13版本中有关“本地”GADT传入OCaml的传言，这将是相当有趣的时代。我想也许OP（etaion）想要使用当前发行版，但也许GADT分支可以接受。对于GADT来说，维度分析似乎是一个很好的测试用例。（我个人很喜欢看到一些GADT代码，它不是小语言的解释器。）问候， –

你举的例子让我觉得你正在尝试做的序言风格逻辑数这将是像

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）。

来源

2011-08-30 15:51:29 stonemetal

他希望您提供的类型和功能，但在* type *级别。即，类型变成一个类型的家族（集合），你的值Zero和Succ成为类型。函数add成为一个类型级函数，它在OCaml中是一个参数化类型，我猜（？）。这种事情总是在Haskell中完成。我没有在OCaml中看到它，这表明它可能并不那么容易。 –

谢谢stonemetal，但是像Jeffrey说的那样，我需要在类型级别发生这种情况，以便编译器可以在编译时执行这些操作并键入检查器来检查约束。这个想法是为了避免运行时检查可能失败，这取决于执行时的情况（例如，捕获语义上的非法操作，比如增加时间长度（不打算支持相对性，只是普通的旧牛顿物理），而按时间划分长度应该合法并导致新的类型 - 速度）。 – etaoin

对不起，我的高阶类型编程能力不是很好。我可能会回到OO，建立代表你需要的各种东西的类。 – stonemetal

您可能能够使用奥列格的许多惊人的建筑之一：http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html

简街有采用一流的模块另一个建议。

http://ocaml.janestreet.com/?q=node/81

声明：我很佩服大多这种编程远道而来。

来源

2011-08-30 17:40:12

谢谢，我听到你在说什么，但是在haskell中，所有这些都通过类型类很容易缝制，而不是:)你发布的这些链接，我一直在看它们，试图获得它的本质，但从来没有成功地将这些模块弯曲到我的需要。我没有得到他们实现的那些类型的等式约束，他们为什么如此重要以及如何使用他们来实现“更高亲密”的功能？我猜我会重读他们几次... – etaoin

ocaml中的类型级别整数

回答

相关问题