（Distributivity'1-'3より少し弱いバージョンで十分そうではある）
Distributivity'3は不要、なぜなら
undistrPairThese . distrPairThese = id
なので、'2から直ちに導かれるから。
Distributivity'2
distrPairThese <$> zip (align xs ys) zs ≡ align (zip xs zs) (zip ys zs)
これはxs, ysの要素だけ見たほうがよくて、
restrict :: forall a b. f a -> f b -> f a
restrict = zipWith const
を使って
restrict (align xs ys) zs ≡ align (restrict xs zs) (restrict ys zs)
Distributivity'1
align (zip xs ys) zs ≡ undistrThesePair <$> zip (align xs zs) (align ys zs)
これもxs, ysの要素だけ見ることができて、
expand :: forall a b. f a -> f b -> f (Maybe a)
expand as bs = justHere <$> align as bs
を使って
expand (zip xs ys) zs ≡ zipWith zip (expand xs zs) (expand ys zs)
Fを多項式Functorとする。
F a = Σ_{x ∈ M} (E x -> a)
F aの要素は(x :: M, f :: E x -> a)と書く。
FがZip (+Align)でもあるとき、それらの法則から
- Mは(Bounded) Distributive Lattice (0,1,∨,∧,≤)
- E(0) ~ Void
であって、2つの関数
inclusion :: (x ≤ y) => E x -> E y
subset :: (x ≤ y) => E y -> Maybe (E x)
から
zip (x,f) (y,g) = (x ∧ y, \i -> (f (inclusion i), g (inclusion i)))
Just <$> align (x,f) (y,g) = (x ∨ y, \i -> toThese (f <$> subset i, g <$> subset i))
とzip, alignが定義される
ここでtoTheseは同型
toThese :: (Maybe a, Maybe b) -> Maybe (These a b)
法則を使えばinclusion, subsetについて以下の等式が得られる。
inclusion . inclusion = inclusion
inclusion @X @X = id
subset <=< subset = subset
subset @X @X = Just
subset @X @y . include @y @X = Just
inclusion @(x∨y) @X . inclusion @X @(x ∧ y) = inclusion @(x∨y) @y . inclusion @y @(x ∧ y)
では余剰な法則は無いのか？
Zip単独、Align単独の法則は余剰なものは無いだろう。
Absorption lawを入れるならばべき等律は省けるかもしれない（が、Zip/Align単独でも使えるようにしたいため、省略はしないでよいだろう）
Distributivityは、束論としてはどちらか片方のみでよいはずだが…
Distributivityは(2)から(1)が導ける、OK!
... これらの等式はE xがそれぞれE 1のある部分集合と見做せて、inclusionがその部分集合の包含写像と見做せると言える。
これがZip/Align則の"想定している"振る舞いなので、Zip/Align則はこれで完全であると言っても良い！