11

のハッキング記事にControl.Applicative欠陥を見つけたと思います。アプリカティブ ファンクターの法則の説明として、次のように述べています。

class Functor f => Applicative f where

アプリケーションを備えたファンクター。純粋な式を埋め込む操作 ( pure) と、計算をシーケンス化し、それらの結果を結合する操作 ( ) を提供します<*>。

最小限の完全な定義には、次の法則を満たすこれらの関数の実装が含まれている必要があります。

身元

pure id <*> v = v

構成

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

準同型

pure f <*> pure x = pure (f x)

交換

u <*> pure y = pure ($ y) <*> u

(これは fmap について何も述べていないことに注意してください)、これらの法則がFunctorインスタンスを決定すると述べています。

これらの法則の結果として、Functorf のインスタンスは次を満たします。

fmap f x = pure f <*> x

私は最初、これは明らかに間違っていると思いました。tつまり、次の 2 つの条件を満たす型コンストラクターが存在する必要があると推測しました。

  1. tApplicative上記のルールを満たすインスタンスであり、
  2. には 2 つの異なる実装があります(つまり、関手法則を満たすinstance (Functor t) 2 つの異なる function があります)。fmap1, fmap2 :: (a->b) -> (t a->t b)

上記が正しい場合 (およびその場合のみ)、上記のステートメントは次のように書き換える必要があります。

f の Functor インスタンスは、次を満たす必要があります。

fmap f x = pure f <*> x

これらの法律の結果として、これはFunctor法律を満たしています。

私の推測が正しいかどうかに関係なく、これは明らかに正しいです。

私の質問は:私の推測は正しいですか? t希望条件のはありますか？

以下は、この質問に自分で答えようとして思ったことの説明です。

私たちが実際の Haskell プログラミングに興味のない単なる数学者であれば、この質問に簡単に肯定的に答えることができます。実際には、

t = Identity
newtype Identity a = Identity {runIdentity :: a}

上記の要件 1 と 2 を満たしています (実際、ほとんど何でも可能です)。実際、は、 で定義されてIdentityいるように、自明にFunctorおよびのインスタンスです。(これは を満たします。) の別の「実装」を定義するには、型ごとに 2 つの関数を使用します。ApplicativeData.Functor.Identityfmap f = (pure f <*>)instance (Functor f)a

transf_a, tinv_a :: a -> a

そのような

tinv_a . transf_a = id

(これは、集合論的には簡単です)。今定義する

instance (Functor Identity) where
 fmap (f :: a->b) = Identity . transf_b . f . tinv_a . runIdentity

これはFunctor法則を満たし、自明なものとは異なる実装です。

x :: a
f :: a -> b

そのような

f x /= transf_b $ f $ tinv_a x

しかし、Haskell でそれができるかどうかはまったく明らかではありません。次のようなものです：

class (Isom a) where
 transf, tinv :: a -> a

instance (Isom a) where
 transf = id
 tinv = id

specialized instance (Isom Bool) where
 transf = not
 tinv = not

Haskellで可能ですか？

編集

大事なことを書き忘れていました。私はGHCベースパッケージの一部として認識Control.Applicativeしているので、私の質問への答えが や などのGHC言語拡張で変わるかどうかにも興味がありますが、FlexibleInstancesまだOverlappingInstances理解していません.

4

2 に答える 2

2

これは、 (定義された) ととして定義されa -> aた の 2 つの住民のみが存在するタイプのプロパティです。id :: a -> aid x = xbottom :: a -> abottom = error "Infinite loop."

最初のケースのみを「合理的」に制限すると、 と を満たすfmapタイプの関数は多くても 1 つしかないという重要な数学的定理に到達します。forall a. forall b. (a -> b) -> f a -> f bfmap id = idfmap f . fmap g = fmap (f . g)

そうでない場合、あなたは正しいfmap = undefinedですfmap = (<*>) . pure。しかし、それは少し安っぽいです。

于 2015-04-15T20:54:32.927 に答える