7

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 つの型レベルの int の記録) の演算を定義する機能が必要です。動的バインディング (オブジェクトを使用する場合) を回避し、コンパイラがそのようなすべての式を静的に評価およびチェックできるようにするために、この方法で行う必要があります。

私の現在の理解では、操作を型コンストラクターとして実装する GADT を作成する必要がありますが、それでも私はその考えに苦労しており、ヒントがあれば大歓迎です。

4

3 に答える 3

5

ML に関する 2008 ワークショップの Sam Lindley による記事Many Holes in Hindley-Milnerにも興味があるかもしれません。

于 2011-08-31T16:15:47.933 に答える
3

Oleg の多くの驚くべき構造の 1 つを使用できるかもしれません: http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html

Jane Street は、ファーストクラスのモジュールを使用する別の提案をしています。

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

免責事項: 私は主にこの種のプログラミングを遠くから賞賛しています。

于 2011-08-30T17:40:12.463 に答える
0

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.

于 2011-08-30T15:51:29.393 に答える