haskell - 暗黙のリフティングの正確さ

Question

モナドに対してジェネリックな値があると想像してください:

m :: (Monad m) => m A  -- 'A' is some concrete type

ここで、この値を 2 つの別々の方法で具体的なモナド変換子スタックに特化したとしましょう。

m1 :: T M A
m1 = m

m2 :: T M A
m2 = lift m

...MとT Mはモナドであり、Tはモナド変換子です:

instance Monad M where ...
instance (Monad m) => Monad (T m) where ...
instance MonadTrans T where ...

...そしてそれらのインスタンスはモナド則とモナド変換子則に従います。

次のように推測できますか。

m1 = m2

...mそのタイプ以外について何も知らないのですか？

lift mこれは、 が の有効な置換であるかどうかを尋ねるための、長ったらしい方法ですm。m置換の前後に 2 つの別個のモナドとして型チェックが必要なため、質問を表現するのは少し難しいです。私が知る限り、そのような置換が型チェックを行う唯一の方法はm、モナドに対してジェネリックである場合です。

私の漠然とした直感は、置換は常に正しいはずですが、私の直感が正しいかどうか、またはそれが正しいかどうかを証明する方法がわかりません。

Answer 1

If m :: Monad m => m A, thenはfor somemと同等である必要があります。これは、何かを取得する唯一の方法がand であるためです。しかし、使用するためには、いくつかの を生成できなければなりません。これは、 の別のアプリケーションまたは別のアプリケーションで行うことができます。いずれにせよ、最終的には使用する必要があり、モナドの法則により、式全体が と同等になることが保証されます。return xx :: A:: m xreturn(>>=)(>>=)m yreturn(>>=)returnreturn x

(mがモナドに対して完全にポリモーフィックである場合、 atm ~ Identityで使用できる必要があるため、引数を渡さない限り、凝ったモナドトリックを使用することはできません。この種のトリックは、たとえばhereおよびhereで使用されます。)

それを考えるとm = return x、モナド変換子の法則 ( lift . return = return) によって、lift m = m.

もちろん、これはこの特定のタイプにのみ当てはまります。たとえば、 がある場合、 は とm :: MonadState S m => m A簡単mに異なる可能性があります。lift mたとえば、 のようなタイプではStateT A (State A) A、getとlift getは異なります。

(そしてもちろん、これはすべて ⊥ を無視しています。繰り返しになりますが、そうしないと、ほとんどのモナドはとにかく法則に従いません。)

Answer 2

これは、あなたがと同等であるというずさんな帰納法の証拠だと思います。mlift m

私たちは何かを証明しようとしなければならないと思いますm（というより、typeのすべての可能な値について(Monad m) => m A）。Monadバインドとリターンのみで構成されていると見なし、ボトムを無視すると、トップレベルでのマストは次のいずれかになりますfail。m

mA = return (x)
mB = (mX >>= f)

モナド変換子の法則では、次の2つの形式が同等ですmA。m

lift (return (x)) = return (x)

それが基本ケースです。次に、次の理由で2番目の変圧器の法則が残されていますmB。

lift (mX >>= f) = lift mX >>= (lift . f)

mBそして、私たちがその拡張に等しいことを証明したいところ：

mX >>= f = lift mX >>= (lift . f)

mX = lift mX帰納的仮説（右？）なので、バインドの左側は同等（）であると仮定します。

それで、私たちはf = lift . fどのように見えなければならないかを理解することによって証明するために残されfています：

f :: a -> m b
f = \a -> (one of our forms mA or mB)

次のようになりlift . fます。

f = \a -> lift (one of our forms mA or mB)

それは私たちの仮説を残します：

m = lift m