30

アルゴリズムを書くとき、私は通常コメントに不変条件を書き留めます。

たとえば、1つの関数が順序付きリストを返し、もう1つの関数がリストが順序付けられることを期待する場合があります。
定理証明が存在することは知っていますが、使用した経験はありません。

また、スマートコンパイラ[sic！]は、それらを利用してプログラムを最適化できると思います。
それで、不変条件を書き留めて、コンパイラーにそれらをチェックさせることは可能ですか？

4

4 に答える 4

58

以下はスタントですが、かなり安全なスタントなので、家で試してみてください。面白い新しいおもちゃのいくつかを使用して、順序の不変条件をmergeSortに焼き付けます。

{-# LANGUAGE GADTs, PolyKinds, KindSignatures, MultiParamTypeClasses,
    FlexibleInstances, RankNTypes, FlexibleContexts #-}

物事を単純にするために、自然数を使用します。

data Nat = Z | S Nat deriving (Show, Eq, Ord)

しかし、私は<=型クラスPrologで定義するので、型チェッカーは暗黙的に順序を理解しようとすることができます。

class LeN (m :: Nat) (n :: Nat) where
instance             LeN Z n where
instance LeN m n =>  LeN (S m) (S n) where

番号を並べ替えるには、任意の2つの番号をどちらかの方法で並べ替えることができることを知っておく必要があります。2つの番号が非常に注文可能であるとはどういう意味かを考えてみましょう。

data OWOTO :: Nat -> Nat -> * where
  LE :: LeN x y => OWOTO x y
  GE :: LeN y x => OWOTO x y

実行時の表現があれば、2つの数字ごとに実際に注文可能であることを知りたいと思います。最近では、のシングルトンファミリを構築することでそれを実現していNatます。Natty nのランタイムコピーのタイプですn。

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

数字をどのように回避するかをテストすることは、証拠を除いて、通常のブールバージョンと非常によく似ています。タイプが変わるため、ステップケースでは開梱と再梱包が必要です。インスタンスの推論は、関連するロジックに適しています。

owoto :: forall m n. Natty m -> Natty n -> OWOTO m n
owoto Zy      n       = LE
owoto (Sy m)  Zy      = GE
owoto (Sy m)  (Sy n)  = case owoto m n of
  LE -> LE
  GE -> GE

番号を並べる方法がわかったので、順序付きリストを作成する方法を見てみましょう。計画は、それが緩い境界の間で順番に何であるかを説明することです。もちろん、要素を並べ替え可能から除外したくないので、境界のタイプは、要素タイプを下部要素と上部要素で拡張します。

data Bound x = Bot | Val x | Top deriving (Show, Eq, Ord)

<=それに応じて概念を拡張し、タイプチェッカーが境界チェックを実行できるようにします。

class LeB (a :: Bound Nat)(b :: Bound Nat) where
instance             LeB Bot     b        where
instance LeN x y =>  LeB (Val x) (Val y)  where
instance             LeB (Val x) Top      where
instance             LeB Top     Top      where

そして、ここに番号の順序付きリストがあります：anOList l uは次のようなシーケンスx1 :< x2 :< ... :< xn :< ONilですl <= x1 <= x2 <= ... <= xn <= u。x :<下限を超えるチェックは、テールの下限としてx課されます。x

data OList :: Bound Nat -> Bound Nat -> * where
  ONil :: LeB l u => OList l u
  (:<) :: forall l x u. LeB l (Val x) =>
          Natty x -> OList (Val x) u -> OList l u

merge順序付きリストは、通常の場合とまったく同じ方法で記述できます。重要な不変条件は、両方のリストが同じ境界を共有する場合、それらのマージも共有することです。

merge :: OList l u -> OList l u -> OList l u
merge ONil      lu         = lu
merge lu        ONil       = lu
merge (x :< xu) (y :< yu)  = case owoto x y of
  LE  -> x :< merge xu (y :< yu)
  GE  -> y :< merge (x :< xu) yu

ケース分析のブランチは、結果の要件を満たすのに十分な順序付け情報を使用して、入力からすでにわかっていることを拡張します。インスタンス推論は、基本的な定理証明者として機能します。幸いなことに（または、少し練習すれば）、証明の義務は十分に簡単です。

契約を結びましょう。この方法で番号を並べ替えるには、番号の実行時の監視を作成する必要があります。

data NATTY :: * where
  Nat :: Natty n -> NATTY

natty :: Nat -> NATTY
natty Z      =                           Nat Zy
natty (S n)  = case natty n of Nat n ->  Nat (Sy n)

この翻訳によって、ソートしたいものにNATTY対応するものが得られることを信頼する必要があります。との間のNatこの相互作用は少しイライラしますが、それがちょうど今Haskellに取り入れられていることです。それができたら、通常の分割統治法で構築できます。NatNattyNATTYsort

deal :: [x] -> ([x], [x])
deal []        = ([], [])
deal (x : xs)  = (x : zs, ys) where (ys, zs) = deal xs

sort :: [Nat] -> OList Bot Top
sort []   = ONil
sort [n]  = case natty n of Nat n -> n :< ONil
sort xs   = merge (sort ys) (sort zs) where (ys, zs) = deal xs

私たちにとって意味のあるプログラムが、タイプチェッカーにとっても同じくらい意味のあるものであることに、私はしばしば驚いています。

[これが、何が起こっているかを確認するために作成したスペアキットです。

instance Show (Natty n) where
  show Zy = "Zy"
  show (Sy n) = "(Sy " ++ show n ++ ")"
instance Show (OList l u) where
  show ONil = "ONil"
  show (x :< xs) = show x ++ " :< " ++ show xs
ni :: Int -> Nat
ni 0 = Z
ni x = S (ni (x - 1))

そして、何も隠されていませんでした。]

于 2012-05-18T20:42:18.190 に答える
26

はい。

Haskell型システムで不変条件をエンコードします。次に、コンパイラーは、不変条件が保持されていない場合にプログラムがコンパイルされないように、強制します（たとえば、型チェックを実行します）。

順序付きリストの場合、ソート時にリストのタイプを変更するスマートコンストラクターを実装する安価なアプローチを検討できます。

module Sorted (Sorted, sort) where

newtype Sorted a = Sorted { list :: [a] }

sort :: [a] -> Sorted a
sort = Sorted . List.sort

これで、保持されていると想定する関数を記述できSorted、コンパイラーは、ソートされていないものをそれらの関数に渡すことを防ぎます。

さらに進んで、非常に豊富なプロパティを型システムにエンコードできます。例：

練習すれば、コンパイル時に、言語によって非常に洗練された不変条件を適用できます。

ただし、型システムはプログラムのプロパティを証明するためにあまり設計されていないため、制限があります。頑丈な証明については、モデル検査またはCoqなどの定理証明言語を検討してください。Agdaという言語はHaskellに似た言語であり、その型システムは豊富なプロパティを証明することを目的としています。

于 2012-05-18T16:41:56.727 に答える
16

ええと、答えはイエスとノーです。タイプとは別に不変条件を記述してチェックする方法はありません。ESC / Haskellと呼ばれるHaskellのリサーチフォークにこれが実装されていましたが、http：//lambda-the-ultimate.org/node/1689

他にもさまざまなオプションがあります。1つは、assertを使用できます：http：//www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html

次に、適切なフラグを使用して、本番用にこれらのアサートをオフにすることができます。

より一般的には、タイプの不変条件をエンコードできます。ここにさらに追加するつもりでしたが、パンチラインに負けません。

もう1つの例は、赤黒木のこの非常に優れたエンコーディングです。http: //www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

于 2012-05-18T16:39:55.540 に答える
4

ここでの他の答えはすべて素晴らしいですが、あなたの質問がコンパイラのチェックについて具体的に言及していても、少なくともQuickCheckのヒントがなければ、このページは不完全だと思います。QuickCheckは、コンパイル時に型システムではなく実行時に機能しますが、型システムで静的に表現するには難しすぎたり不便だったりする可能性のあるプロパティをテストするための優れたツールです。

于 2012-05-24T04:37:07.233 に答える