ジャガー/リチャーズ:あなたはいつもあなたが望むものを手に入れることができるとは限りませんが、いつか試してみるとあなたはあなたがあなたが必要なものを手に入れることに気付くかもしれません。
リスト内のカーソル
snoc-およびcons-listを使用して構造のコンポーネントを再構築し、空間プロパティを明確に保ちます。私は定義します
data Bwd x = B0 | Bwd x :< x deriving (Functor, Foldable, Traversable, Show)
data Fwd x = F0 | x :> Fwd x deriving (Functor, Foldable, Traversable, Show)
infixl 5 :<
infixr 5 :>
data Cursor x = Cur (Bwd x) x (Fwd x) deriving (Functor, Foldable, Traversable, Show)
コモナドを作ろう
class Functor f => Comonad f where
counit :: f x -> x
cojoin :: f x -> f (f x)
カーソルがコマンドであることを確認しましょう
instance Comonad Cursor where
counit (Cur _ x _) = x
cojoin c = Cur (lefts c) c (rights c) where
lefts (Cur B0 _ _) = B0
lefts (Cur (xz :< x) y ys) = lefts c :< c where c = Cur xz x (y :> ys)
rights (Cur _ _ F0) = F0
rights (Cur xz x (y :> ys)) = c :> rights c where c = Cur (xz :< x) y ys
あなたがこの種のものに目を向けているなら、あなたはそれCursor
が空間的に楽しい変種であることに気付くでしょうInContext []
InContext f x = (x, ∂f x)
ここで、∂はファンクターの形式微分を取り、ワンホールコンテキストの概念を与えます。この回答で述べたように、InContext f
は常にであり、ここにあるのは、フォーカスで要素を抽出し、各要素を独自のコンテキストで装飾して、リフォーカスされたカーソルでいっぱいのコンテキストを効果的に与える微分構造によって引き起こされるものです。カーソルを動かさずにフォーカスします。例を見てみましょう。Comonad
Comonad
counit
cojoin
> cojoin (Cur (B0 :< 1) 2 (3 :> 4 :> F0))
Cur (B0 :< Cur B0 1 (2 :> 3 :> 4 :> F0))
(Cur (B0 :< 1) 2 (3 :> 4 :> F0))
( Cur (B0 :< 1 :< 2) 3 (4 :> F0)
:> Cur (B0 :< 1 :< 2 :< 3) 4 F0
:> F0)
見る?フォーカスされている2は、cursor-at-2になるように装飾されています。左側には、cursor-at-1のリストがあります。右側には、cursor-at-3とcursor-at-4のリストがあります。
カーソルの作成、カーソルの転置?
さて、あなたが求めている構造Comonad
は、のn倍の構成ですCursor
。持ってみましょう
newtype (:.:) f g x = C {unC :: f (g x)} deriving Show
コモナドを説得f
しg
て作曲するには、counit
sはきちんと作曲しますが、「分配法則」が必要です。
transpose :: f (g x) -> g (f x)
だからあなたはcojoin
このような複合体を作ることができます
f (g x)
-(fmap cojoin)->
f (g (g x))
-cojoin->
f (f (g (g x)))
-(fmap transpose)->
f (g (f (g x)))
どのような法律がtranspose
満たされるべきですか?おそらく次のようなもの
counit . transpose = fmap counit
cojoin . transpose = fmap transpose . transpose . fmap cojoin
または、fとgのシーケンスをある順序から別の順序に移動する2つの方法で同じ結果が得られるようにするために必要なことは何でも。
transpose
forCursor
をそれ自体で定義できますか?ある種の移調を安価に取得する1つの方法は、それがzippilyBwd
に適用可能であることに注意することです。したがって、そうです。Fwd
Cursor
instance Applicative Bwd where
pure x = pure x :< x
(fz :< f) <*> (sz :< s) = (fz <*> sz) :< f s
_ <*> _ = B0
instance Applicative Fwd where
pure x = x :> pure x
(f :> fs) <*> (s :> ss) = f s :> (fs <*> ss)
_ <*> _ = F0
instance Applicative Cursor where
pure x = Cur (pure x) x (pure x)
Cur fz f fs <*> Cur sz s ss = Cur (fz <*> sz) (f s) (fs <*> ss)
そして、ここであなたはネズミのにおいを嗅ぎ始めるべきです。形状の不一致により切り捨てが発生し、自己転置が自己逆であるという明らかに望ましい特性が損なわれます。どんな種類の不規則さも生き残れません。転置演算子を取得します:sequenceA
、そして完全に通常のデータの場合、すべてが明るく美しいです。
> regularMatrixCursor
Cur (B0 :< Cur (B0 :< 1) 2 (3 :> F0))
(Cur (B0 :< 4) 5 (6 :> F0))
(Cur (B0 :< 7) 8 (9 :> F0) :> F0)
> sequenceA regularMatrixCursor
Cur (B0 :< Cur (B0 :< 1) 4 (7 :> F0))
(Cur (B0 :< 2) 5 (8 :> F0))
(Cur (B0 :< 3) 6 (9 :> F0) :> F0)
しかし、内側のカーソルの1つを位置合わせから外すだけでも(サイズを不規則にすることを気にしないでください)、問題が発生します。
> raggedyMatrixCursor
Cur (B0 :< Cur ((B0 :< 1) :< 2) 3 F0)
(Cur (B0 :< 4) 5 (6 :> F0))
(Cur (B0 :< 7) 8 (9 :> F0) :> F0)
> sequenceA raggedyMatrixCursor
Cur (B0 :< Cur (B0 :< 2) 4 (7 :> F0))
(Cur (B0 :< 3) 5 (8 :> F0))
F0
外側のカーソル位置が1つで、内側のカーソル位置が複数ある場合、正常に動作する転置はありません。自己構成Cursor
により、内部構造を相互に不規則にすることができるため、いいえtranspose
、いいえcojoin
。あなたは定義することができます、そして私は定義しました
instance (Comonad f, Traversable f, Comonad g, Applicative g) =>
Comonad (f :.: g) where
counit = counit . counit . unC
cojoin = C . fmap (fmap C . sequenceA) . cojoin . fmap cojoin . unC
しかし、内部構造を規則的に保つことは私たちの責任です。あなたがその負担を受け入れる気があるなら、あなたは繰り返すことができます。なぜならApplicative
、そしてTraversable
は作曲の下ですぐに閉じられるからです。ここに断片があります
instance (Functor f, Functor g) => Functor (f :.: g) where
fmap h (C fgx) = C (fmap (fmap h) fgx)
instance (Applicative f, Applicative g) => Applicative (f :.: g) where
pure = C . pure . pure
C f <*> C s = C (pure (<*>) <*> f <*> s)
instance (Functor f, Foldable f, Foldable g) => Foldable (f :.: g) where
fold = fold . fmap fold . unC
instance (Traversable f, Traversable g) => Traversable (f :.: g) where
traverse h (C fgx) = C <$> traverse (traverse h) fgx
編集:完全を期すために、すべてが定期的である場合の動作は次のとおりです。
> cojoin (C regularMatrixCursor)
C {unC = Cur (B0 :< Cur (B0 :<
C {unC = Cur B0 (Cur B0 1 (2 :> (3 :> F0))) (Cur B0 4 (5 :> (6 :> F0)) :> (Cur B0 7 (8 :> (9 :> F0)) :> F0))})
(C {unC = Cur B0 (Cur (B0 :< 1) 2 (3 :> F0)) (Cur (B0 :< 4) 5 (6 :> F0) :> (Cur (B0 :< 7) 8 (9 :> F0) :> F0))})
(C {unC = Cur B0 (Cur ((B0 :< 1) :< 2) 3 F0) (Cur ((B0 :< 4) :< 5) 6 F0 :> (Cur ((B0 :< 7) :< 8) 9 F0 :> F0))} :> F0))
(Cur (B0 :<
C {unC = Cur (B0 :< Cur B0 1 (2 :> (3 :> F0))) (Cur B0 4 (5 :> (6 :> F0))) (Cur B0 7 (8 :> (9 :> F0)) :> F0)})
(C {unC = Cur (B0 :< Cur (B0 :< 1) 2 (3 :> F0)) (Cur (B0 :< 4) 5 (6 :> F0)) (Cur (B0 :< 7) 8 (9 :> F0) :> F0)})
(C {unC = Cur (B0 :< Cur ((B0 :< 1) :< 2) 3 F0) (Cur ((B0 :< 4) :< 5) 6 F0) (Cur ((B0 :< 7) :< 8) 9 F0 :> F0)} :> F0))
(Cur (B0 :<
C {unC = Cur ((B0 :< Cur B0 1 (2 :> (3 :> F0))) :< Cur B0 4 (5 :> (6 :> F0))) (Cur B0 7 (8 :> (9 :> F0))) F0})
(C {unC = Cur ((B0 :< Cur (B0 :< 1) 2 (3 :> F0)) :< Cur (B0 :< 4) 5 (6 :> F0)) (Cur (B0 :< 7) 8 (9 :> F0)) F0})
(C {unC = Cur ((B0 :< Cur ((B0 :< 1) :< 2) 3 F0) :< Cur ((B0 :< 4) :< 5) 6 F0) (Cur ((B0 :< 7) :< 8) 9 F0) F0} :> F0)
:> F0)}
ハンコックのテンソル積
規則性のためには、作曲よりも強いものが必要です。「g-structures-all-the-same-shapeのf-structure」の概念を捉えることができる必要があります。これは、計り知れないピーター・ハンコックが「テンソル積」と呼んでいるものです。これを書きますf :><: g
。すべての内側のg構造に共通する「外側」のf字型と「内側」のg字型が1つあるため、転置は簡単に定義できます。そして常に自己逆です。ハンコックのテンソルはHaskellで便利に定義できませんが、依存型の設定では、このテンソルを持つ「コンテナー」の概念を簡単に定式化できます。
あなたにアイデアを与えるために、コンテナの縮退した概念を考えてみましょう
data (:<|) s p x = s :<| (p -> x)
ここで言うs
のは「形」p
のタイプと「位置」のタイプです。値は、形状の選択とx
各位置でのストレージで構成されます。依存するケースでは、位置のタイプは形状の選択に依存する場合があります(たとえば、リストの場合、形状は数値(長さ)であり、その数の位置があります)。これらのコンテナにはテンソル積があります
(s :<| p) :><: (s' :<| p') = (s, s') :<| (p, p')
これは一般化されたマトリックスのようなものです。形状のペアが寸法を示し、位置の各ペアに要素があります。との値を入力p
してp'
依存する場合、これを完全にうまく行うことができます。これは、まさにハンコックによるコンテナのテンソル積の定義です。s
s'
テンソル積のInContext
さて、あなたが高校で学んだかもしれないように、∂(s :<| p) = (s, p) :<| (p-1)
どこp-1
よりも要素が1つ少ないタイプがありp
ます。∂(sx ^ p)=(s p)* x ^(p-1)のように。1つの位置を選択して(図形に記録して)、削除します。障害は、p-1
依存型なしで手に入れるのが難しいことです。ただし、位置を削除せずにInContext
選択します。
InContext (s :<| p) ~= (s, p) :<| p
これは従属ケースでも同様に機能し、喜んで取得します
InContext (f :><: g) ~= InContext f :><: InContext g
InContext f
これは常にであることがわかります。これは、sのComonad
テンソル積InContext
はそれ自体がInContext
sであるため、コモナティックであることを示しています。つまり、ディメンションごとに1つの位置を選択します(これにより、全体で1つの位置が得られます)。以前は、1つの外側の位置と多くの内側の位置がありました。テンソル積が構成に置き換わるため、すべてがうまく機能します。
ナペリア関手
Functor
しかし、テンソル積と構成が一致するサブクラスがあります。これらは、次Functor
のようなf
ものf () ~ ()
です。つまり、とにかく形状が1つしかないため、構成内の不規則な値は最初から除外されます。これらFunctor
はすべて、対数(与えるために累乗する必要のある指数)と考えることができる(p ->)
いくつかの位置セットに対して同型です。それに対応して、ハンコックはジョン・ネイピア(その幽霊はハンコックが住んでいるエジンバラの一部に出没する)にちなんでこれらの関手を呼びます。p
x
f x
Naperian
class Applicative f => Naperian f where
type Log f
project :: f x -> Log f -> x
positions :: f (Log f)
--- project positions = id
Naperian
ファンクターには対数があり、そこにある要素に位置をマッピングするイオン関数を誘導しますproject
。Naperian
ファンクターはすべてzippilyApplicative
でpure
あり<*>
、プロジェクション用のKおよびSコンビネーターに対応しています。各位置にその位置の表現が格納されている値を作成することもできます。覚えているかもしれない対数の法則が喜んで現れます。
newtype Id x = Id {unId :: x} deriving Show
instance Naperian Id where
type Log Id = ()
project (Id x) () = x
positions = Id ()
newtype (:*:) f g x = Pr (f x, g x) deriving Show
instance (Naperian f, Naperian g) => Naperian (f :*: g) where
type Log (f :*: g) = Either (Log f) (Log g)
project (Pr (fx, gx)) (Left p) = project fx p
project (Pr (fx, gx)) (Right p) = project gx p
positions = Pr (fmap Left positions, fmap Right positions)
固定サイズの配列(ベクトル)は、で与えられることに注意してください(Id :*: Id :*: ... :*: Id :*: One)
。ここOne
で、は定数単位の関手であり、その対数はVoid
です。したがって、配列はNaperian
です。今、私たちも持っています
instance (Naperian f, Naperian g) => Naperian (f :.: g) where
type Log (f :.: g) = (Log f, Log g)
project (C fgx) (p, q) = project (project fgx p) q
positions = C $ fmap (\ p -> fmap (p ,) positions) positions
これは、多次元配列がであるということを意味しますNaperian
。
InContext f
forのバージョンを作成するNaperian f
には、位置をポイントするだけです。
data Focused f x = f x :@ Log f
instance Functor f => Functor (Focused f) where
fmap h (fx :@ p) = fmap h fx :@ p
instance Naperian f => Comonad (Focused f) where
counit (fx :@ p) = project fx p
cojoin (fx :@ p) = fmap (fx :@) positions :@ p
したがって、特に、Focused
n次元配列は確かにcomonadになります。ベクトルはであるため、ベクトルの合成はn個のベクトルのテンソル積ですNaperian
。ただし、Focused
n次元配列は、その次元を決定するn個のベクトルの合成ではなくn倍のテンソル積になります。Focused
このコモナドをジッパーで表現するには、テンソル積を作成できる形で表現する必要があります。これは将来の演習として残しておきます。