20

(*)Haskellで最も厳密でないセマンティクスで実装することは可能ですか? たとえば、このような定義は、次のようになります。

0 * ⊥ = 0
⊥ * 0 = 0

のみ：

⊥ * ⊥ = ⊥

上記のケースの 1 つを満たすパターン マッチを構築できますが、両方は構築できません。これは、ゼロ チェックが値を強制するためです。

4

2 に答える 2

21

はい。ただし、制約された不純物のみを使用します。

laziestMult :: Num a => a -> a -> a
laziestMult a b = (a * b) `unamb` (b * a)

これunambは、Conal Elliott による の「純粋な」変形ですamb。操作上、amb2 つの計算を並行して実行し、最初に来た方を返します。一方unambが他方よりも (領域理論の意味で) 厳密に大きい 2 つの値を表示的に取り、大きい方を返します。 編集：これもlubではなくunmbなので、どちらかが下でない限り、それらを等しくする必要があります。 したがって、型システムによって強制できない場合でも、保持する必要があるセマンティック要件があります。これは基本的に次のように実装されます。

unamb a b = unsafePerformIO $ amb a b

例外/リソース管理/スレッドセーフでこれをすべて正しく機能させるには、多くの作業が必要です。

laziestMult*が交換可能であれば正しいです。*1 つの引数で厳密でない場合は、「最も厳密でない」です。

詳細については、Conal のブログを参照してください。

于 2013-02-16T03:09:06.857 に答える
12

Phillip JF の回答はフラットなドメインにのみ適用されますがNum、怠惰な自然など、フラットではないインスタンスもあります。このアリーナに入ると、物事は非常に微妙になります。

data Nat = Zero | Succ Nat
    deriving (Show)

instance Num Nat where
    x + Zero = x
    x + Succ y = Succ (x + y)

    x * Zero = Zero
    x * Succ y = x + x * y

    fromInteger 0 = Zero
    fromInteger n = Succ (fromInteger (n-1))

    -- we won't need the other definitions

怠惰な自然人にとっては、操作が最も厳密でないことが特に重要です。たとえば、それらを使用して、おそらく無限のリストの長さを比較します。その操作が最小厳密でない場合、有用な情報が見つかると発散します。

予想どおり、(+)可換ではありません。

ghci> undefined + Succ undefined
Succ *** Exception: Prelude.undefined
ghci> Succ undefined + undefined
*** Exception: Prelude.undefined

したがって、標準的なトリックを適用してそうします。

laxPlus :: Nat -> Nat -> Nat
laxPlus a b = (a + b) `unamb` (b + a)

最初はうまくいくようです

 ghci> undefined `laxPlus` Succ undefined
 Succ *** Exception: Prelude.undefined
 ghci> Succ undefined `laxPlus` undefined
 Succ *** Exception: Prelude.undefined

しかし、実際にはそうではありません

 ghci> Succ (Succ undefined) `laxPlus` Succ undefined
 Succ (Succ *** Exception: Prelude.undefined
 ghci> Succ undefined `laxPlus` Succ (Succ undefined)
 Succ *** Exception: Prelude.undefined

これはNat、フラット ドメインではなく、フラット ドメインにunambのみ適用されるためです。このため、unamb高レベルの概念を定義する以外に使用すべきではない低レベルのプリミティブを検討します。ドメインがフラットかどうかは関係ありません。使用unambは、ドメイン構造を変更するリファクタリングに影響されます。同じ理由seqが意味的に醜いです。unambに一般化されるのと同じ方法seqで一般化する必要があります。deeqSeqこれはData.Lubモジュールで行われます。HasLub最初に のインスタンスを書く必要がありますNat:

instance HasLub Nat where
    lub a b = unambs [
                  case a of
                      Zero -> Zero
                      Succ _ -> Succ (pa `lub` pb),
                  case b of
                      Zero -> Zero
                      Succ _ -> Succ (pa `lub` pb)
              ]
        where
        Succ pa = a
        Succ pb = b

これが正しいと仮定すると、必ずしもそうではありません (これまでのところ 3 回目の試行です)。次のように記述できますlaxPlus'。

laxPlus' :: Nat -> Nat -> Nat
laxPlus' a b = (a + b) `lub` (b + a)

そしてそれは実際に動作します：

ghci> Succ undefined `laxPlus'` Succ (Succ undefined)
Succ (Succ *** Exception: Prelude.undefined
ghci> Succ (Succ undefined) `laxPlus'` Succ undefined
Succ (Succ *** Exception: Prelude.undefined

したがって、可換二項演算子の最も厳密でないパターンは次のように一般化する必要があります。

leastStrict :: (HasLub a) => (a -> a -> a) -> a -> a -> a
leastStrict f x y = f x y `lub` f y x

少なくとも、交換可能であることが保証されています。しかし、残念ながら、さらに問題があります。

ghci> Succ (Succ undefined) `laxPlus'` Succ (Succ undefined)
Succ (Succ *** Exception: BothBottom

少なくとも 2 である 2 つの数値の合計は少なくとも 4 であると予想されますが、ここでは少なくとも 2 である数値しか得られませんleastStrict。新しいクラス制約を導入することなくではありません。この問題を解決するには、再帰的な定義を掘り下げ、すべてのステップで両方の引数で同時にパターン マッチを行う必要があります。

laxPlus'' :: Nat -> Nat -> Nat
laxPlus'' a b = lubs [
    case a of
        Zero -> b
        Succ a' -> Succ (a' `laxPlus''` b),
    case b of
        Zero -> a
        Succ b' -> Succ (a `laxPlus''` b')
    ]

そして最後に、可能な限り多くの情報を提供するものを取得します。

ghci> Succ (Succ undefined) `laxPlus''` Succ (Succ undefined)
Succ (Succ (Succ (Succ *** Exception: BothBottom

同じパターンを時間に適用すると、同様に機能するように見えるものが得られます。

laxMult :: Nat -> Nat -> Nat
laxMult a b = lubs [
    case a of
        Zero -> Zero
        Succ a' -> b `laxPlus''` (a' `laxMult` b),
    case b of
        Zero -> Zero
        Succ b' -> a `laxPlus''` (a `laxMult` b')
    ]

ghci> Succ (Succ undefined) `laxMult` Succ (Succ (Succ undefined))
Succ (Succ (Succ (Succ (Succ (Succ *** Exception: BothBottom

言うまでもなく、ここにはいくつかのコードが繰り返されており、これらの機能をできるだけ簡潔に (したがって、エラーの可能性をできるだけ少なくして) 表現するパターンを開発することは興味深い課題です。しかし、別の問題があります...

asLeast :: Nat -> Nat
atLeast Zero = undefined
atLeast (Succ n) = Succ (atLeast n)

ghci> atLeast 7 `laxMult` atLeast 7
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ ^CInterrupted.

恐ろしく遅いです。明らかにこれは、引数のサイズが (少なくとも) 指数関数的であり、再帰ごとに 2 つの分岐に分かれているためです。妥当な時間内に実行するには、さらに微妙な作業が必要になります。

最小厳密プログラミングは比較的未開拓の領域であり、実装と実際のアプリケーションの両方でさらに研究する必要があります。私はそれに興奮しており、有望な領域だと考えています。

于 2013-02-17T21:21:13.737 に答える