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つの基本的なSI単位の指数を表す7つのタイプのレベルintのレコード）を定義する能力が必要です。動的バインディング（オブジェクトを使用する場合）を回避し、コンパイラがそのような式をすべて評価して静的にチェックできるようにするには、この方法で行う必要があります。

現時点では、タイプコンストラクタとして操作を実装するGADTを作成する必要があると私は理解していますが、まだ私はそのアイデアに苦しんでおり、ヒントは非常に高く評価されます。

出典

2011-08-30 etaoin

また、2008年のMLワークショップのサムリンドリーの記事Many Holes in Hindley-Milnerに興味があるかもしれません。

出典

2011-08-31 16:15:47

私はちょうどこれらのスライドを見た;アイデアはとてもシンプルでクールです。しかし、それは私には型レベルの追加だけを処理するようです。シンプルさを保ちながら減算のために働かせる方法はありません。あなたがSI単位を追跡しているなら、あなたは減算（そして負の整数）が必要だと思います。 –

@ジェフリー私はゆっくりと私に来るアイデアをお詫びしますが、OCamlの "GADT"ブランチがあることは知っていますよね？ https://sites.google.com/site/ocamlgadt/（明らかに、そのページによれば、私たちは3.13でそれらを取得しています）。 –

はい、私は、 "native" GADTの噂が、OCamlに3.13で来ると聞いてきました。かなり興味深い時です。おそらく、OP（エタオン）が現在のリリースで何かを手に入れたいと思うかもしれませんが、おそらくGADTブランチは受け入れられるでしょう。次元分析は、GADTにとっておそらく良いテストケースのように思えます。（私は個人的に小さな言語のための通訳ではないいくつかの例のGADTコードを見たいと思っています。）よろしく、 –

あなたの例では、私はあなたが別のソリューションで

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

あなたのバックグラウンドストーリーのヒントになります追加

type fancyInt = Zero | Succ of fancyInt ;;

ようなものになるだろうプロローグスタイルのロジック番号をやろうとしていると思わせます距離を表すクラスを作成します。内部的に値を保存しますが、その時に必要な単位で距離を取得および設定できるインターフェイスを提供する必要があります。または、機能的なアプローチをとどめたい場合は、ユニットのタイプを作成してから、Ocaml自身が処理するのと同じように、つまりmeters_of_kmの関数を持つようにしてください。

出典

2011-08-30 15:51:29 stonemetal

彼はあなたが与えるタイプと機能を望んでいますが、*タイプ*のレベルです。すなわち、タイプはタイプのファミリー（セット）になり、あなたの値ZeroとSuccはタイプになります。関数addは型レベルの関数になります。これはOCamlではパラメータ化された型です（？）。この種のことは、常にハスケルで行われています。私はOCamlでこれを見たことがないので、それほど簡単ではないかもしれません。 –

stonemetalありがとうございますが、Jeffrey氏のように、コンパイル時にこれらの操作を実行できるように、タイプレベルでこれを実行する必要があります。その考え方は、実行時の状況に応じて失敗する可能性のあるランタイムチェックを避けることです（つまり、長さを追加する（相対性をサポートすることを意図していない、ちょうど古いNewtonian物理学）のではなく、新しいタイプのベロシティが得られます）。 – etaoin

申し訳ありませんが、私の高次タイプのプログラミング能力はあまり良くありません。私はおそらくオブジェクト指向に戻って、必要な様々な種類のものを表現するクラスを作成します。 – 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

ありがとう、私はあなたが言うことを聞いているが、それはすべてのタイプのクラスで簡単に縫いつけられているので、それはすべての時間を見てきた、それらのモジュールを私のニーズに合わせて曲げることに成功したことはありませんでした。私は彼らが実装している型平等制約を得ていない、なぜ彼らはとても重要で、 "より親切な"関数を達成するためにそれらをどのように正確に使用するのか？私はそれらを何度か読み返すだろうと思う... – etaoin

答えて

関連する問題