Lens from Scratch

久しぶりのLensの記事です.
5億回は繰り返されてきたであろうLens再実装を通して, Lens, Getter, Setter, Iso, Equality, Traversal, Prism, Foldの仕組みを理解するのが目的です.

亜Lens family

Getter

Getterは基本的にはConstをかぶせる操作とそれを剥がす操作で実現可能です.
つまりgetConst (Const k) = kですが, このConst kがデータであり, getConstは値を取り出すgetterになります.

アクセサの型がGetting r s aであるとき, sからaを取り出せる(=s -> aなるgetterである)という意味です.

(^.)はGetterとデータから具体的に値を取り出し, toは函数をGetterに変換するための函数です.

type Getting r s a = (a -> Const r a) -> s -> Const r s
 
(^.) :: s -> Getting a s a -> a
s ^. l = getConst (l Const s)
 
to :: (s -> a) -> Getting r s a
to f = \k -> Const . getConst . k . f

Tuple

タプルに対するGettingアクセサが定義できます. 2変数の場合は

-- case: 2-tuple
_1 :: Getting r (a,b) a
_1 = to fst

とすることで, (a,b) ^. _1 == aが実現できます.
あるいは, 任意個のTupleに対してこの_1や_2を使いたい場合は, 本家のパッケージのように型クラスで定義します.

class TupleIndex t a | t -> a where
  _1 :: Getting r t a
 
instance TupleIndex (a,b) a where _1 = to (\(a,_) -> a)
instance TupleIndex (a,b,c) a where _1 = to (\(a,_,_) -> a)

List

リストに対してもアクセサを提供できます.

ix :: Int -> Getting r [a] a
ix n = to (!! n)

例としては[1..10] ^. ix 7 == 8のようになります.

Setter

Setter(ここではSetting型)にはIdentityが使われます.
Identity xをIdentity yに書き換える操作がsetterで実現できます.

(.~)はSetting s t a b型のアクセサに対し, データsをbによって書き換えtを得る操作に対応します.
(%~)は函数を適用し, setsは函数をSetterに変換します.

type Setting s t a b = (a -> Identity b) -> s -> Identity t
 
infixr 4 .~
(.~) :: Setting s t a b -> b -> s -> t
(.~) l = (runIdentity .) . (l . const . Identity)

(%~) :: Setting s t a b -> (a -> b) -> s -> t
(%~) l f = runIdentity . l (Identity . f)
 
sets :: ((a -> b) -> s -> t) -> Setting s t a b
sets h = \k -> Identity . h (runIdentity . k)

Lens

さて, GetterとSetterの定義はよく似ています.
少々天下り的に導入したこれらの定義はいずれもLensの具体例になっています. (LensはGetterとSetterを一般化した概念)
定義より, GetterやSetterに対する函数はLensに対しても使えます.

lensはgetterとsetterをLensに変換する函数です.
accessor = lens getter setterのようにして使います.

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
 
lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens g h = \f s -> fmap (h s) (f (g s))

Tuple

さて先ほど定義した_1はGetterではなくLensになるように拡張します.
これによって_1がGetterとしてもSetterとしても働くようになります.

class TupleIndex s t a b | s -> a, t -> b, s b -> t, t a -> s where
  _1 :: Lens s t a b
 
instance TupleIndex (a,b) (a',b) a a' where
  _1 = lens (\(a,_) -> a) (\(_,y) b -> (b,y))
instance TupleIndex (a,b,c) (a',b,c) a a' where
  _1 = lens (\(a,_,_) -> a) (\(_,y,z) b -> (b,y,z))

List

Listに対するアクセサixも同様にLensに拡張します.

ix :: Int -> Lens [a] [a] a a
ix n = lens (!! n) (\ts x -> take n ts ++ [x] ++ drop (n+1) ts)

Traversal

次はTraversalです. これはLensより少し制約の強いもので, 大体traverseができるようなデータです.

bothは2-tupleの両方の値に一度に処理をするようなTraversalです.
both %~ f $ (a,b) == (f a, f b)みたいに使います.

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
 
traverseOf :: Applicative f => Traversal s t a b -> (a -> f b) -> s -> f t
traverseOf = id
 
both :: Traversal (a,a) (b,b) a b
both = \k (x,y) -> (,) <$> k x <*> k y

Each

Traversalに対する処理をさせるために, Traversalなアクセサを定義します.
例えば本家のパッケージではEachという, リストや配列の全ての要素に対する操作を行うアクセサが提供されています.

class Each s t a b | s -> a, t -> b, s b -> t, t a -> s where
  each :: Traversal s t a b
 
instance Each [a] [b] a b where
  each = traverse

例えばtraverseOf each print [1,2,3]はリストの各値を表示して, [(),(),()]を返します.

Fold

FoldはTraversalよりさらに制約が強い型です. ただしここではTraversalもFoldも一般化していないので同じものになっています.

foldingは函数をFoldに変換します. (^..)は結果をリストにして返すのでFoldとともによく使われます.

type Fold s a = forall f. (Applicative f) => (a -> f a) -> s -> f s
 
infixl 8 ^..
(^..) :: s -> Getting (Endo [a]) s a -> [a]
s ^.. l = (appEndo $ getConst $ l (Const . Endo . (:)) s) []
 
folding :: Foldable f => (s -> f a) -> Fold s a
folding h = \k s -> traverse_ k (h s) *> pure s

例として[[1,2],[3]] ^.. traverse . traverse == [1,2,3]や[1,2,3] ^.. folding tail == [2,3]です.

Iso

IsoはLensの(->)をProfunctorに一般化したものです.
(亜)Lensは本来ここにあるよりもっと一般化された型ですが, 今の場合は必要以上に一般化しない方針で実装をしているのでここで初めてProfunctorが登場します.

Profunctorはp a bが合った時, aとbの両方に(反変的に)函数が作用するようなデータです.

Isoは大体Iso s s a aの形で使い, s -> aとa -> sの2つの変換を保持するLensのようなものです.

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
  dimap f g = lmap f . rmap g
 
  lmap :: (a -> b) -> p b c -> p a c
  lmap f = dimap f id
 
  rmap :: (b -> c) -> p a b -> p a c
  rmap = dimap id
 
instance Profunctor (->) where
  dimap f g k = g . k . f

type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
 
iso :: (s -> a) -> (b -> t) -> Iso s t a b
iso sa bt = dimap sa (fmap bt)
 
enum :: Enum a => Iso Int Int a a
enum = iso toEnum fromEnum
 
curried :: Iso ((a, b) -> c) ((d, e) -> f) (a -> b -> c) (d -> e -> f)
curried = iso curry uncurry
 
reversed :: Iso String String String String
reversed = iso reverse reverse

Equality

本家のパッケージにはIsoより更に制約の弱いEqualityという型もあります.
Isoから更にProfunctorとFunctorの制約を外したものですが, 制約がないせいでほとんど何も出来ないためあまり役に立つことはないでしょう.

type Equality s t a b = forall p f. p a (f b) -> p s (f t)
 
simple :: Equality a a a a
simple = id

Prism

PrismはLensに制約を加えたものです. ここではPrismも一般化されていないのでFoldと同じものになっています.

Prismは大体LensですがEitherを主に扱うためのものです.
prismは函数をPrismに変換し, _LeftはEitherのLeftへのアクセサです.

type Prism s t a b = forall f. Applicative f => (a -> f b) -> s -> (f t)
 
prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
prism bt sta = \k s -> case sta s of
  Left t -> pure t
  Right a -> fmap bt $ k a
 
_Left :: Prism (Either a c) (Either b c) a b
_Left = \k s -> case s of
  Left a -> fmap Left $ k a
  Right c -> pure $ Right c

さてこのままではPrismを何かのデータ型に作用させることができませんが, 次のReviewによってそれが可能になります.

Review

ReviewはPrismの(->)の部分を一般化します.

ReviewはPrismの最初と最後の(->)の部分をProfunctorに一般化します. これによって, ReviewはProfunctorの間の変換になります.

ここで, Tagged s bはbのみをデータとしてもち, sは幽霊型になっているデータです.

instance Profunctor Tagged where
  dimap _ g = Tagged . g . unTagged

type Review s a = forall p f. (Applicative f) => p a (f a) -> p s (f s)
type AReview s a = Tagged a (Identity a) -> Tagged s (Identity s)
 
re :: AReview s a -> Getting r a s
re r = to (runIdentity . unTagged . r . Tagged . Identity)
 
review :: AReview s a -> a -> s
review r a = a ^. re r

さて, ここでAReviewは(->)ではなくTaggedというProfunctorを使っています.
このため今の定義ではAReviewはPrismにはなりません. よってPrismの定義もProfunctorを使ったものに変えて, reviewがPrismに対しても使えるようにしましょう.

Prism再び

ところで, Prismの定義をProfunctorに書き換えると, prismと_Leftの定義は描き直す必要があります.
しかし実はprismを定義するためには(prismがEitherを扱うこととの兼ね合いで)Profunctorでは不十分で, もっと制約の強い(ここではChoice)型クラスが必要になります.

class (Profunctor p) => Choice p where
  left' :: p a b -> p (Either a c) (Either b c)
  left' = dimap (either Right Left) (either Right Left) . right'
 
  right' :: p a b -> p (Either c a) (Either c b)
  right' = dimap (either Right Left) (either Right Left) . left'
 
instance Choice (->) where
  left' k (Left a) = Left $ k a
  left' _ (Right c) = Right c
 
instance Choice Tagged where
  left' = Tagged . Left . unTagged

type Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)
 
prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
prism bt sta = dimap sta (either pure (fmap bt)) . right'
 
_Left :: Prism (Either a c) (Either b c) a b
_Left = prism Left (either Right (Left . Right))

これでAReviewはPrismとなり, review _Left "hoge" == Left "hoge"のようにreviewが使えるようになります.

Cons

今定義されたPrismを使ってConsを定義します.
ConsはリストやVectorなどの, 先頭が定義できるようなデータを表します.

(<|)はConsの先頭に要素を追加するような函数です.
また, _headはConsの先頭の要素へのアクセサです.

class Cons s t a b | s -> a, t -> b, s b -> t, t a -> s where
  _Cons :: Prism s t (a,s) (b,t)
 
instance Cons [a] [b] a b where
  _Cons = prism (uncurry (:)) $ \ass -> case ass of
    (a:as) -> Right (a,as)
    [] -> Left []
 
infixr 5 <|
(<|) :: Cons s s a a => a -> s -> s
a <| s = review _Cons (a,s)

_head :: Cons s s a a => Traversal s s a a
_head = \k s -> _Cons (\(a,s') -> (,) <$> k a <*> pure s') s

0 <| [1,2,3] == [0,1,2,3]のように使います.

参考

• Haskellのlensの使い方 (詳しめ) - うさぎ小屋
• lens: Lenses, Folds and Traversals | Hackage
• lens-family-core: Haskell 98 Lens Families | Hackage

終わりに

これで, Control.Lensにある亜Lensファミリーの重要と思われる型の大部分はカバーできたと思います.
あとの細々したところは実際の実装を追うのがよいでしょう.
Lensは巨大で複雑ですがこのように一つ一つ1から実装していけばそこまで難しくはないと思います. 個々のレベルではIdentityとかConstとかTaggedとかを使って型合わせゲームしているだけでちゃんと動きます.

というわけで以上です.
最後にコード全体を載せておきます.

無限ループによる証明

Software FoundationsのIMPあたりをやってて疑問が湧いた.

w = while True do Skip endが停止しないことを示したい.
つまり, $\langle w, s \rangle \to s' \Rightarrow False$ を示したい. ($s, s' : \mathbb{Z} \to \mathbb{Z}$ は変数の値を保持する環境)

普通に証明するなら以下のようになると思う:
証明図の高さに関する帰納法による. まず高さが0のとき, 明らかに<w,s>→s'は公理から導くことはできないので高さ0の証明図を持たない. よって$\langle w, s \rangle \to s' \Rightarrow False$である.
次に, $\forall s, s'. \langle w, s \rangle \to s'$が高さnの証明図をもたないと仮定し, $\langle w, s \rangle \to s'$が高さ(n+1)の証明図をもたないことを証明する. $\langle w, s \rangle \to s'$が高さ(n+1)の証明図をもつことを仮定すると, wの定義とwhile-loopに関する推論規則より$\langle w, s \rangle \to s'$が高さnの証明図で示せる. これは帰納法の仮定に矛盾するので証明が完了する.

Agdaなどの依存型を持つ言語では, prop :: w -> Falseに対応する函数を作ってやればよい.
<w,s>→s'にあたるデータ型を再帰的に定義している場合, 例えばこの証明は無限ループを使ってprop (While-Loop True _ k) = kみたいにすると, 証明図の仮定に当たる, 「一つ前の」<w,s>→s'を使うことができる.
けれど一体これは何を証明していることになるんだろう？
明らかに上の証明とは違う気がするし, そもそも無限ループになっているのに証明が完了しているというのがよく分からない. 直観的には「<w,s>→s'を仮定すると全く同じ形が仮定の部分に出現する」ということが重要なんだろうという気がするけれど、そこからどうやって矛盾を導いているんだろう.

ちなみにIsabelleでは以下のようにやった.
上の証明の気持ちがある程度反映されているつもり. (と言っても証明だけでは伝わらない気もするけど)

lemma while_induction:
  assumes red: "(WHILE b DO c END) %: st ⇓ st'"
  and base: "⋀t t'. ⟦ beval3 t b = False; t' = t ⟧ ⟹ P t t'"
  and step: "⋀t t' t''. ⟦ beval3 t b = True; c %: t ⇓ t'; (WHILE b DO c END) %: t' ⇓ t''; P t' t'' ⟧ ⟹ P t t''"
  shows "P st st'"
proof-
  have "(WHILE b DO c END) %: st ⇓ st' ⟹ P st st'"
    using ceval.induct [of _ _ _ "λc0 t t'. WHILE b DO c END = c0 ⟶ P t t'"] apply rule
    apply (simp, auto, simp add: base)
    apply (fastforce simp add: step)
    apply (fastforce simp add: step)
    done
  thus ?thesis by (simp add: red)
qed
 
theorem loop_never_stops: "¬ (loop %: st ⇓ st')"
proof (unfold loop_def, auto)
  assume p: "WHILE BTrue DO SKIP END %: st ⇓ st'"
  show "False"
    using while_induction [of BTrue SKIP st st' "λ_. λ_. False"]
    by (rule, simp add: p, auto)
qed

de Bruijn Indexとβ変換

$ KMN \equiv (\lambda xy. x)MN \longrightarrow_{\beta} M $を示したいとする.

α変換

$y \notin \text{FV}(M)$ならば, $ (\lambda xy. x)MN \to (\lambda y. M) N \to M[y:=N] \equiv M $となる.
問題は$y \notin \text{FV}(M)$ならば$ M[y:=N] \equiv M $の部分で, これを示すにはMについての帰納法を使う.

$M \equiv x$(変数)の時は$x=y, x \neq y$で場合分けして明らか. $M \equiv (\lambda x. M_0)$の時は, α変換によって$x \neq y$としてよく, このとき$M[y:=N] \equiv (\lambda x. M_0)[y:=N] \equiv (\lambda x. M_0[y:=N])$となり, あとは帰納法の仮定よりOK. $M \equiv (M M')$のときは帰納法の仮定と代入の性質から明らか.

さてこれをIsabelle(proof assistant)で証明しようとすると, α変換によって$x \neq y$としてとれるというところを示すのが難しい.
α変換の煩わしさを軽減するためにλ式の定義を少し変えて, de Bruijn Indexによる定義をする.

de Bruijn Index

<λ-expr> ::= <var :: nat> | λ. <λ-expr> | (<λ-expr> <λ-expr>)

によって定義する. 変数の代わりに自然数を使い, さらに函数抽象をするときに束縛変数を指定しない.
<var :: nat>は, その変数のいくつ前にあるλによって束縛されているかを表す(この変数の添字の割り振り方をde Bruijn Indexと呼ぶらしい).

例として, $\lambda. \lambda. 1 \equiv \lambda xy. x$, $\lambda. \lambda. 0 (\lambda. 0 1) \equiv \lambda xy. y (\lambda z. z y)$である.

de Bruijn Indexのλ式のβ変換をどのように定義するかを考える.
λ式Mの中で, Mの中の変数nがあったとき, nに対応するλがMに含まれていることとnがMの束縛変数であることは等しい.

このとき, $(\lambda. M) N$のβ変換は, Mの中の自由変数の値を一つ減らし(λがはずれるため), Nの中の自由変数の値はλに対応するMの中の変数の深さだけ増やす.
例: $(\lambda. \lambda. \lambda. 5 2) (\lambda. 0 1) \to (\lambda. \lambda. (5-1) (\lambda. 0 (1+2))) \equiv (\lambda. \lambda. 4 (\lambda. 0 3)) $

de Bruijn Indexによるλ式の表現は, 束縛変数の添字の振り方に自由度がないのでα変換を考える必要がない.

元の問題へ

結局元の問題に戻ると, $ KMN \longrightarrow M $を示すのが目的だった.
de Bruijn Indexでは, $ (\lambda. \lambda. 1) M N \to (\lambda M) N \to M $ となることを示せばよい.
けれど, これもあまり上手くいかなかったので結局どうすればいいのだろう.

K,M,Nが変数条件を満たす時, unshift 1 (λ shift 1 (shift 1 M)) $ N ⟶ Mが示せればいいと思うけれど.