10

私はCRDTについてこの論文を読み始めました。これは、データを変更する操作が可換であることを確認することにより、変更可能なデータを同時に共有する方法です。これはHaskellでの抽象化の良い候補であるように思われました-データ型とその型で通勤する操作を指定するCRDTの型クラスを提供し、並行プロセス間で実際に更新を共有するライブラリの作成に取り組みます。

私が理解できないのは、型クラスの仕様で操作が通勤しなければならないという契約をどのように表現するかです。

簡単な例：

class Direction a where
  turnLeft :: a -> a
  turnRight :: a -> a

turnLeft . turnRightと同じであるという保証はありませんturnRight . turnLeft。フォールバックは、モナドの法則に相当するものを指定することだと思います。コメントを使用して、型システムによって強制されない制約を指定します。

4

4 に答える 4

11

必要なのは、以下の疑似 Haskell のような証明負担を含む型クラスです。

class Direction a where
    turnLeft  :: a -> a
    turnRight :: a -> a
    proofburden (forall a. turnLeft (turnRight a) === turnRight (turnLeft a))

ここで、すべてのインスタンスは、コンパイラが型チェックを行うための関数と証明の両方を提供する必要があります。Haskellには証明の概念がない(まあ、限られた)ため、これは(Haskellにとって)希望的観測です。

OTOH、Coq は、Haskell に抽出できる依存型付き言語の証明アシスタントです。私は以前にCoq の型クラスを使用したことがありませんが、次の例を使用して簡単に検索できます。

Class EqDec (A : Type) := {
   eqb : A -> A -> bool ;
   eqb_leibniz : forall x y, eqb x y = true -> x = y }.

したがって、高度な言語はこれを行うことができるように見えますが、標準的な開発者の学習曲線を下げるには、間違いなく多くの作業が必要です.

于 2010-12-23T20:45:08.197 に答える
7

TomMD の回答に加えて、Agda を使用して同じ効果を得ることができます。型クラスはありませんが、ほとんどの機能 (動的ディスパッチを除く) をレコードから取得できます。

record Direction (a : Set) : Set₁ where
  field
    turnLeft  : a → a
    turnRight : a → a
    commLaw   : ∀ x → turnLeft (turnRight x) ≡ turnRight (turnLeft x)

投稿を編集して、なぜ Haskell でこれができないのかという質問に答えようと思いました。

Haskell (+ 拡張機能) では、上記の Agda コードで使用されているように同等性を表すことができます。

{-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}

data (:=:) a :: * -> * where
  Refl :: a :=: a

これは、2 つの型が等しいという定理を表しています。たとえばais と同等bですa :=: b。

それらが同等である場合、コンストラクターを使用できますRefl。これを使用して、定理 (型) の証明 (値) に対して関数を実行できます。

-- symmetry
sym :: a :=: b -> b :=: a
sym Refl = Refl

-- transitivity
trans :: a :=: b -> b :=: c -> a :=: c
trans Refl Refl = Refl

これらはすべて型が正しいため、真です。しかし、これは;

wrong :: a :=: b
wrong = Refl

明らかに間違っており、実際に型チェックに失敗します。

ただし、これらすべてを通じて、値と型の間の壁は破られていません。値、値レベルの関数、および証明は、依然としてコロンの片側に存在します。型、型レベル関数、および定理は互いに共存しています。turnLeftとturnRightは値レベルの関数であるため、定理に関与することはできません。

AgdaとCoqは依存型言語であり、バリアが存在しないか、クロスオーバーが許可されています。Strathclyde Haskell Enhancement (SHE)は、Haskell コードのプリプロセッサであり、DTP の効果の一部を Haskell にチートすることができます。これは、値の世界のデータを型の世界に複製することによって行われます。値レベル関数の複製をまだ処理しているとは思いません。もしそうなら、これは複雑すぎて処理できないのではないかと思います。

于 2010-12-23T21:18:48.853 に答える
3

すでに述べたように、型システムを使用して Haskell でこれを直接強制する方法はありません。しかし、コメントで制約を指定するだけでは不十分な場合は、妥協点として、目的の代数的プロパティの QuickCheck テストを提供できます。

これらの行に沿ったものは、チェッカー パッケージで既に見つけることができます。インスピレーションを得るために参照することをお勧めします。

于 2010-12-23T21:18:09.620 に答える
2

私が理解できないのは、操作が型クラスの仕様で交換しなければならないという契約をどのように表現するかです。

あなたがそれを理解できない理由は、それが不可能だからです。この種のプロパティを型にエンコードすることはできません - 少なくとも Haskell ではできません。

于 2010-12-23T20:06:40.423 に答える