35

Haskell に関する多くの記事では、実行時ではなくコンパイル時にいくつかのチェックを行うことができると述べています。したがって、可能な限り単純なチェックを実装したいと思います。0 より大きい整数に対してのみ関数を呼び出せるようにします。どうすればいいですか？

4

6 に答える 6

44 
module Positive (toPositive, Positive(unPositive)) where

newtype Positive = Positive { unPositive :: Int }

toPositive :: Int -> Maybe Positive
toPositive n = if (n < 0) then Nothing else Just (Positive n)

上記のモジュールはコンストラクターをエクスポートしないため、型の値を作成する唯一の方法PositiveはtoPositive、正の整数を指定することです。これを使用してラップを解除しunPositive、実際の値にアクセスできます。

次に、以下を使用して正の整数のみを受け入れる関数を記述できます。

positiveInputsOnly :: Positive -> ...
于 2012-08-10T22:49:52.137 に答える
36

Haskell は、他の言語が実行時に実行するいくつかのチェックをコンパイル時に実行できます。あなたの質問は、任意のチェックがコンパイル時に解除されることを望んでいることを暗示しているようです。これは、証明義務の大きな可能性がなければ不可能です (つまり、プログラマーであるあなたは、プロパティがすべての用途に対して真であることを証明する必要があることを意味する可能性があります)。 ）。

Inch以下では、非常にクールなサウンドのツールについて言及しながら、ピッグワーカーが触れたこと以上のことを言っているようには感じません。各トピックに追加された単語が、ソリューション空間の一部を明確にすることを願っています。

What People Mean (Haskell の静的保証について話す場合)

通常、人々が Haskell によって提供される静的保証について話しているのを聞くとき、彼らは Hindley Milner スタイルの静的型チェックについて話しているのです。これは、ある型を別の型と混同できないことを意味します。そのような誤用はコンパイル時に検出されます (例:let x = "5" in x + 1無効です)。明らかに、これは表面をかじっただけであり、Haskell での静的チェックのいくつかの側面について議論することができます。

スマート コンストラクター: 実行時に 1 回チェックし、型を介して安全性を確保する

Gabriel の解決策は、Positive正の値しか取り得ない型 を使用することです。正の値を作成するには実行時にチェックが必要ですが、正の値を取得すると、関数を使用する際に必要なチェックはありません。ここから静的 (コンパイル時) 型チェックを利用できます。

これは、多くの問題に対する適切な解決策です。黄金数について語るときも同じことを勧めた。とはいえ、これはあなたが釣りをしているものだとは思いません。

正確な表現

dflemstr は、負の数を表すことができない型 を使用できるとコメントしましたWord(正の数を表すのとは少し異なる問題です)。この方法では、不変条件に違反するタイプの居住者が存在しないため、(上記のように) 保護されたコンストラクターを使用する必要はありません。

適切な表現を使用するより一般的な例は、空でないリストです。空にならない型が必要な場合は、空でないリスト型を作成できます。

data NonEmptyList a = Single a | Cons a (NonEmptyList a)

これは、Nil代わりに を使用する従来のリスト定義とは対照的ですSingle a。

ポジティブな例に戻ると、ペアノ数の形式を使用できます。

data NonNegative = One | S NonNegative

または、ユーザー GADT を使用して符号なし 2 進数を作成します (さらにNum、 やその他のインスタンスを追加して、 のような関数を許可できます+):

{-# LANGUAGE GADTs #-}

data Zero
data NonZero
data Binary a where
  I :: Binary a -> Binary NonZero
  O :: Binary a -> Binary a
  Z :: Binary Zero
  N :: Binary NonZero

instance Show (Binary a) where
        show (I x) = "1" ++ show x
        show (O x) = "0" ++ show x
        show (Z)   = "0" 
        show (N)   = "1"

外部証明

Haskell ユニバースの一部ではありませんが、より豊富なプロパティを記述および証明できる代替システム (Coq など) を使用して Haskell を生成することは可能です。この方法では、Haskell コードは次のようなチェックを単純に省略できますx > 0が、x が常に 0 より大きいという事実は静的な保証になります (繰り返しますが、安全性は Haskell によるものではありません)。

pigworker が言ったことから、私はInchこのカテゴリに分類します。Haskell は、目的のタスクを実行できるほど十分に成長していませんが、Haskell を生成するツール (この場合、Haskell 上の非常に薄いレイヤー) は進歩を続けています。

より記述的な静的プロパティに関する研究

Haskell を使った研究コミュニティは素晴らしいです。一般的な使用にはあまりにも未熟ですが、人々は関数の部分性や契約を静的にチェックするなどのことを行うツールを開発しました。周りを見渡せば豊かな畑だ。

于 2012-08-11T05:57:43.437 に答える
32

Haskell の整数制約を管理するAdam Gundry のInchプリプロセッサをプラグインできなかったら、彼の監督者としての義務を果たせなかったでしょう。

Maybeスマート コンストラクターと抽象化バリアはすべて非常に優れていますが、実行時にあまりにも多くのテストをプッシュし、パディングを必要とせずに静的にチェックアウトする方法で自分が何をしているのかを実際に知る可能性を考慮していません。. （衒学者が書いています。別の回答の著者は、0 が正であると示唆しているように見えますが、これは論争の的であると考える人もいるかもしれません。もちろん、真実は、0 と 1 の両方が頻繁に発生するさまざまな下限の用途があるということです。上限にある程度の使用があります。)

Xi の DML の伝統に従って、Adam のプリプロセッサは、Haskell がネイティブに提供するものにさらに精度のレイヤーを追加しますが、結果のコードはそのまま Haskell に消去されます。Iavor Diatchki が行ってきた型レベルの自然数に関する作業と連携して、彼が行ったことを GHC とよりよく統合できれば素晴らしいことです。私たちは何が可能かを理解したいと思っています。

一般的なポイントに戻ると、Haskell は現在、理解によるサブタイプの構築 (たとえば、0 より大きい Integer の要素) を可能にするほど十分に依存型付けされていませんが、多くの場合、静的制約を許容するよりインデックス化されたバージョンに型をリファクタリングできます。現在、シングルトン型の構造は、これを実現するための利用可能な不快な方法の中で最もクリーンです。一種の「静的」整数が必要であり、種類の住民はInteger -> *「動的表現を持つ」などの特定の整数のプロパティをキャプチャします（これはシングルトン構造であり、各静的なものに一意の動的対応物を与えます）が、次のようなより具体的なものも必要です「ポジティブであること」。

インチは、合理的に適切に動作する整数のサブセットを操作するために、シングルトンの構築に煩わされる必要がなかった場合の想像を表しています。依存型プログラミングは Haskell で可能な場合が多いですが、現在は必要以上に複雑になっています。この状況に対する適切な感情は恥ずかしさであり、私はそれを最も強く感じています.

于 2012-08-10T23:52:51.257 に答える
15

これはずっと前に回答されており、私自身の回答をすでに提供していることは知っていますが、暫定的に利用可能になった新しいソリューション、Liquid Haskell に注意を向けたいと思いました。

この場合、次のように記述して、特定の値が正でなければならないことを指定できます。

{-@ myValue :: {v: Int | v > 0} #-}
myValue = 5

f同様に、次のように、関数が正の引数のみを必要とするように指定できます。

{-@ f :: {v: Int | v > 0 } -> Int @-}

Liquid Haskell は、指定された制約が満たされていることをコンパイル時に検証します。

于 2013-06-28T23:02:00.487 に答える
5

これ、または実際には、自然数の型 (0 を含む) に対する同様の欲求は、実際には Haskell の数値クラス階層に関する一般的な不満であり、これに対する真にクリーンなソリューションを提供することは不可能です。

なんで？の定義を見てくださいNum:

class (Eq a, Show a) => Num a where
    (+) :: a -> a -> a
    (*) :: a -> a -> a
    (-) :: a -> a -> a
    negate :: a -> a
    abs :: a -> a
    signum :: a -> a
    fromInteger :: Integer -> a

使用に戻らない限り(これは悪い習慣です) 、とerrorの定義を提供する方法はありません。(-)negatefromInteger

于 2012-08-11T00:34:39.820 に答える
4

型レベルの自然数は GHC 7.6.1 で計画されています: https://ghc.haskell.org/trac/ghc/ticket/4385

この機能を使用すると、"自然数" 型を簡単に記述でき、実現できなかったパフォーマンスが得られます (たとえば、手動で記述された Peano 型の場合)。

于 2012-08-13T06:45:41.567 に答える