25

次の 2 つの例のように、型を制約できる型付きプログラミング言語はありますか?

  1. Probability は、最小値 0.0 と最大値 1.0 の浮動小数点数です。

    type Probability subtype of float
where
    max_value = 0.0
    min_value = 1.0

  2. 離散確率分布はマップです。ここで、キーはすべて同じタイプである必要があり、値はすべて確率であり、値の合計 = 1.0 です。

    type DPD<K> subtype of map<K, Probability>
where
    sum(values) = 1.0

私の知る限り、これは Haskell や Agda では不可能です。

4

8 に答える 8

31

必要なものは、絞り込みタイプと呼ばれます。

ProbabilityAgdaで定義することが可能です: Prob.agda

合計条件付きの確率質量関数タイプは、264 行で定義されています。

ATSなど、Agda よりも直接的な改良型を持つ言語があります。

于 2013-10-04T10:52:34.360 に答える
26

これは、Haskell をリファインメント タイプで拡張するLiquid Haskellを使用して Haskell で行うことができます。述語はコンパイル時に SMT ソルバーによって管理されます。つまり、証明は完全に自動化されますが、使用できるロジックは SMT ソルバーが処理するものによって制限されます。(幸いなことに、最新の SMT ソルバーはかなり汎用性があります!)

問題の 1 つは、Liquid Haskell が現在 float をサポートしているとは思えないことです。そうでない場合は、SMTソルバーの浮動小数点数の理論があるため、修正できるはずです。浮動小数点数が実際には有理数であると偽ることもできます (またはRational、Haskell で使用することさえできます!)。これを念頭に置いて、最初のタイプは次のようになります。

{p : Float | p >= 0 && p <= 1}

2 番目のタイプは、特にマップが推論しにくい抽象型であるため、エンコードが少し難しくなります。マップの代わりにペアのリストを使用した場合、次のように「メジャー」を記述できます。

measure total :: [(a, Float)] -> Float
total []          = 0 
total ((_, p):ps) = p + probDist ps

( a でラップ[]することnewtypeもできます。)

totalリストを制約するために絞り込みで使用できるようになりました。

{dist: [(a, Float)] | total dist == 1}

Liquid Haskell の巧妙なトリックは、多少制約のあるロジックを使用する代わりに、コンパイル時にすべての推論が自動化されることです。(メジャーのようなものtotalは、書き方にも非常に制約があります。これは、「コンストラクターごとに 1 つのケースのみ」などのルールを持つ Haskell の小さなサブセットです。) これは、このスタイルの絞り込み型は強力ではありませんが、フル型よりもはるかに使いやすいことを意味します。 -依存型に対応し、より実用的なものにします。

于 2014-08-29T15:59:54.553 に答える
10

Perl6 には、任意の条件を追加して「サブタイプ」を作成できる「タイプサブセット」の概念があります。

特にあなたの質問について：

subset Probability of Real where 0 .. 1;

と

role DPD[::T] {
  has Map[T, Probability] $.map
    where [+](.values) == 1; # calls `.values` on Map
}

（注：現在の実装では、「where」部分は実行時にチェックされますが、「実際の型」は（クラスを含む）コンパイル時にチェックされis pure、std（これは主に perl6 です) (これらは*などの演算子にもあります)、それはそれに費やされる努力の問題に過ぎません (それ以上の努力は必要ありません)。

より一般的に：

# (%% is the "divisible by", which we can negate, becoming "!%%")
subset Even of Int where * %% 2; # * creates a closure around its expression
subset Odd of Int where -> $n { $n !%% 2 } # using a real "closure" ("pointy block")

次に、数値が Smart Matching operator と一致するかどうかを確認できます~~。

say 4 ~~ Even; # True
say 4 ~~ Odd; # False
say 5 ~~ Odd; # True

そして、s (または multi 何でも、実際には multi メソッドなど) のおかげでmulti sub、それに基づいてディスパッチできます。

multi say-parity(Odd $n) { say "Number $n is odd" }
multi say-parity(Even) { say "This number is even" } # we don't name the argument, we just put its type
#Also, the last semicolon in a block is optional
于 2014-08-29T19:24:09.347 に答える
2

Whiley 言語は、あなたが言っていることと非常によく似たものをサポートしています。例えば：

type natural is (int x) where x >= 0
type probability is (real x) where 0.0 <= x && x <= 1.0

これらのタイプは、次のように事前/事後条件として実装することもできます。

function abs(int x) => (int r)
ensures r >= 0:
    //
    if x >= 0:
        return x
    else:
        return -x

言語は非常に表現力豊かです。これらの不変条件と事前/事後条件は、SMT ソルバーを使用して静的に検証されます。これは上記のような例を非常にうまく処理しますが、現在、配列とループの不変条件を含むより複雑な例には苦労しています。

于 2014-09-02T03:20:32.333 に答える
2

最初の部分については、はい、それは整数部分範囲を持つ Pascal です。

于 2014-08-30T00:29:15.303 に答える
0

Modula 3 には部分範囲型があります。(序数の部分範囲。)したがって、例 1 で、確率をある精度の整数範囲にマップする場合は、次のように使用できます。

TYPE PROBABILITY = [0..100]

必要に応じて有効数字を追加します。

参照: 部分範囲序数の詳細については、こちらを参照してください。

于 2014-08-30T06:44:21.650 に答える