在 ocaml 中输入级别整数

发布于 2024-12-02 08:53:26 字数 477 浏览 0 评论 0原文

有人可以给我关于在 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 个类型级别整数的记录）。我需要这样做以避免动态绑定（使用对象时）并使编译器能够静态地评估和检查所有此类表达式。

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

原文

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

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.

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.

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

寒冷纷飞旳雪 2024-12-09 08:53:26

您可能还对文章Hindley-Milner 中的许多漏洞< /a>，作者 Sam Lindley，来自 2008 年 ML 研讨会。

回复收藏 0 原文

灯下孤影 2024-12-09 08:53:26

您也许可以使用 Oleg 的许多令人惊奇的结构之一： http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html

Jane Street 有另一个使用一流模块的建议。

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

免责声明：我最欣赏这种编程方式。

回复收藏 0 原文

你列表最软的妹 2024-12-09 08:53:26

你的例子让我觉得你正在尝试做序言风格的逻辑数字，这将类似于

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。

Your example makes me think you are trying to do prolog style logic numbers which would be something like

type fancyInt = Zero | Succ of fancyInt ;;

then add would be

let rec add a b = match a with Zero -> b | Succ c -> add c (Succ b);;

Your background story hints at a different solution, create a class that represents distances. Internally store the value however you need to then provide an interface that allows you to get and set the distance in the units necessary at the time. Or if you are wanting to stay with a functional approach just create the types for your units then have of functions the same way Ocaml itself handles such things, i.e. meters_of_km.

回复收藏 0 原文

~没有更多了~