Just $ A sandbox

プログラミングとかPCとかの技術的なメモ

objective覚書

objective-0.6.1

O' = data Object e m
= forall x. e x -> m (x, Object e m)
= hom(e, m . (-,O'))   (as Nat)

functor Kを用いてe = hom(a,K-) = forall x. a -> K xと書けるとき(Data.Functor.Kan.Ranを見よ)

O' = hom(hom(a,K-), m . (-,O'))
= hom(K^-1(hom(a,-)), m . (-,O'))
  -- by K^-1 -| Ran K
= hom(hom(a,-), Ran K (m . (-,O')))
  -- covariant yoneda
= Ran K (m . (-,O')) a
= forall r. (a -> K r) -> m (r,O')

Object e mがわかっているとき, eと適当な型の直積をとっても良い:

O' = data Object (forall x. (a,e x)) m
= hom((a×-) . e, m . (-,O'))
= hom(e , hom(a,-) . m . (-,O'))
= data Object e (forall x. a -> m x)

eとして Request a b r = (a,b->r) を取ったものはProcessとして定義されている.

P' = data Process a b m
= Object (Request a b) m
= hom((a×-) . hom(b,-), m . (-,P'))
= hom(hom(b,-), hom(a,-) . m . (-,P'))
= a -> m (b, P')

左Kan拡張を使ってもいいけれど同値な式以上の意味はなさそう.
Lanがより単純な項に書き換えられるなら何かあるのかも?

O' = data Object e m = Hom(Lan (-,O') e, m)

Codensity Monad

Codensity という型がある. 定義は以下.

newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }

instance Functor (Codensity k) where
  fmap f (Codensity m) = Codensity (\k -> m (k . f))

instance Monad (Codensity f) where
  return x = Codensity (\k -> k x)
  m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

これの何が良いかと言うと, これは以下のようにMonadFreeな作用を持つ.

instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where
  wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))

Codensityはnewtypeで実装されているから, 実行時には CodensityrunCodensity によるオーバーヘッドは考えなくて良い. だから, m のMonadFreeのメソッドを直接呼ぶよりも効率よくなる可能性が高い. 特に, 元々のmが「重い」モナドなら, Codensity をかぶせるだけで劇的に速くなることがある.

Codensityのパフォーマンスの話は http://www.iai.uni-bonn.de/~jv/mpc08.pdf などを参考にしてもらうことにして, 以下ではCodensityの(圏論的な)説明をしてみる.

以下, 定義などは逐一述べないので必要に応じてnLabなり参考文献に挙げたものを参照してください.

RanとCodensity

functor p : C → Dに対し, functor  p^{-1} \colon \mathcal{E}^\mathcal{D} → \mathcal{E}^\mathcal{C}を,  p^{-1}(F) = F \circ p によって定める. ただしここで  \mathcal{E}^\mathcal{D} とはDからEへの関手のなす関手圏のこと.

functor f : C → E, p : C → Dに対し, pに沿ったfの右Kan拡張  p \ddagger f を考える.
 p \ddagger が存在すれば, これは  p^{-1} の右随伴である.

D
↑ ↘ p‡f
| ⇓ ↘
C ――→ E

随伴の定義から,

 \hom(p^{-1}(-),f) \cong \hom(-,p \ddagger f)

ここで,  \mathcal{C} の対象aを一つ固定し, 米田関手yを用いて

 \hom(p^{-1}(ya),f) \cong \hom(ya,p \ddagger f)

 p^{-1} の定義に戻れば,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f)

さらに右辺で(共変)米田の補題を用いて,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f) \cong (p \ddagger f)(a)

なる同型を得る. ゆえに (p \ddagger f)(a) が存在したとすれば最左辺と同型になる.
さて今はHaskellでの話がしたいので, 対象とは型であり, 射とは函数である.  \hom(ya \circ p,f) とは, 自然変換の集合であるが, これを ya \circ p \rightarrow fなる自然変換からなる型と同一視する.

このような仕方で (p \ddagger f)(a)を最左辺で定義すると,
自然変換 ya . p ~> fRankNTypes を用いて, forall b. (a -> p b) -> f b なる型を持つ.

よって,

newtype Ran p f a = Ran (forall b. (a -> p b) -> f b)

を得る. これは http://hackage.haskell.org/package/kan-extensions-4.1.0.1/docs/Data-Functor-Kan-Ran.html で定義されている.

最後に, pもfもmで固定してしまうと,

newtype Ran     m m a = Ran       (forall b. (a -> m b) -> m b)
newtype Codensity m a = Codensity (forall b. (a -> m b) -> m b)

により, Codensityが得られた.

HaskellでのFunctor, Monad

上のような操作でCodensityは得られるが, 上の操作では pやfは関手 であった.
しかしCodensityはFunctorのinstanceで(Functor m) =>を要求しない (つまり, mがFunctorやMonadでなくとも, CodensityはFunctorおよびMonadになる).

最初の実装で確かにCodensityがFunctorやMonadになることは確認が必要なので, Agdaで証明を書いてみた.

確かに,

instance Functor (Ran p f)
instance Functor (Codensity k)
instance Monad (Codensity f)

なるインスタンスが正しく実装されていることが分かる.

参考文献

Agdaで集合論をやろうとして上手く行かなかった

この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した.

写像の定義を

_⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B

としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる.
x ∈ A を像の方に押し込めて

_⟶_ A B = ∀ x → ∃ \y → x ∈ A → y ∈ B

のように定義すると, 今度は x ∈ A に依って決まる写像が定義できなくなる.

最初の方法ではZFCから排中律を示すところで引っかかり(本来異なる集合 A,B に対して A ≡ B を言おうとするので型エラーになって上手く行かない), あとの方法では置換公理を使う場面でひっかかる(函数の像を扱うとき).
よっていずれにせよ上手く行かない.

この前の記事のコメントではAgdaの型を用いて を定義する方法も教えてもらった.

data _∈_ {l} {A : Set l} (x : A) (B : Set l) : Set (suc l) where
  in-eq : A ≡ B → x ∈ B

この方法だと, の定義がもろにAgdaの型システムに依存しているので, 方針はガラッと変わるはず.
多分これで今やっていることの模倣はできると思うけれど, そもそも何を公理として仮定して良いのかが分からないし, もともとAgdaの型システムではどういうことができるのかもよく分からないのでなんとも言えない.

Agdaの方に上手く寄れば, 多分普通の数学の模倣はできるような気がするけれど, 少なくとも数学のやり方をそのまま持ってくるだけでは上手く行かないのかなぁと思った.
こういうことをするなら, Agdaよりもっと向いている言語を他に探したほうがいいのかもとも思った.
でもAgdaはHaskellerの自分にとっては学びやすかったし, 気に入ったところも多かったので少し残念.

供養

https://github.com/myuon/agda-cate

(圏論はそれなりに上手く行っているので, 圏論方面はもう少し開発を続けるかもしれない)

矛盾の証明

矛盾を示すときに使える方法としては主に以下の2つだと思う

  • 命題 ¬PP をぶつける
  • 矛盾 の特徴付けを使う

矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから,
空集合の公理がそのまま矛盾の特徴付けになる.
∃ \(A : Set) → (∀ x → ¬ (x ∈ A))

否定命題にPをぶつけるというのは口で言うほど簡単ではなくて, まずどの否定命題を選んでくるかからよく考えないといけない.

一体何の話かというと, Agdaで「ZFC ⇒ 排中律 (P ∨ (¬ P))」を示すときに,

https://myuon.github.io/agda-cate/Sets.Sets.NonDatur.html#660

A = ⟦ x ∈ [0,1] ∣ x ≡ 0 ∨ P ⟧ -- A := {x ∈ {0,1} ∣ x = 0 ∨ P}
B = ⟦ x ∈ [0,1] ∣ x ≡ 1 ∨ P ⟧ -- B := {x ∈ {0,1} ∣ x = 1 ∨ P}
X = [ A , B ] -- X := {A,B}

みたいにするんだけど, 以下の議論では, ここにさらっとでてくる自然数0と1が異なることが仮定されている.

0と1は上のように非順序対を作って使うので適当なsetでないといけないんだけど, 当然AgdaのData.Natで定義されているNatの元は(inductive data typesで定義されているから)setではない.
そこで 0 = ∅, 1 = ∅ ∪ {∅} に戻って0と1が異なることを示さないといけなかったけれど, これには空集合の公理や対の公理や和集合の公理が必要で, しかもそんなに明らかなことでもない.
https://myuon.github.io/agda-cate/Sets.Sets.Natural.html#793

Natの世界でもSetの世界でも0と1が異なることを示すには, 0=1を仮定して矛盾を導かなければいけないので, それがいつも自明なことではないなと実感した.

というかむしろ, Agdaの場合は同値なものがrewriteによって書き換えるだけで証明が済んでしまうことが多いので, 等しさが特別扱いやすいだけなのかもしれないけど.

Classical set theory in Agda

Agda歴2週間くらいのザコです。 Agda圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。

標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているように見えるだけであんまり使い物にならない。
具体的に言うと和集合の公理がないので(binary cupとindexed bigcupはある)任意個のUnionがとれない。
他にも、そもそも∈の定義が函数適用なので X ∈ B と書いときにXとBでは型が違うのがすごくキモいとか。キモいというかこれのせいでZFの一部の公理は型があわなくて表現できなかったりもする。

そういうわけでまずは集合を使えるようにするというだけ。
コードは一番下に載っけました。

コードについて

二重否定除去

Relation.Nullary.Negation

elem

属するの演算と2つの公理。
elem-∈は(x : A)と(x ∈ A)がcompatibleになるように。
≡-∈は示せなさそうで必要になったから入れたけど本当に必要なんだろうか。よく分からない。

postulate
  _∈_ : Set → Set → Set₁
  elem-∈ : {A : Set} → ∀ x → x ∈ A → A
  ≡-∈ : {A X Y : Set} → X ≡ Y → X ∈ A → Y ∈ A

公理

仮定したのは以下。

  • 外延性の公理
  • 対の公理
  • 和集合の公理
  • 無限公理
  • 分出公理
  • 冪集合の公理
postulate
  extensionality : {A B : Set} → A ≡ B ⇔ Lift {_} {zero} (∀ x → (x ∈ A ⇔ x ∈ B))
  ∃-paring : ∀(A B : Set) → ∃ \(P : Set) → ∀ x → x ∈ P ⇔ (x ≡ A) ∨ (x ≡ B)
  ∃-union : (A : Set) → ∃ \(B : Set) → ∀ X → X ∈ B ⇔ (∃ \C → (C ∈ A) ∧ (X ∈ C))
  infinite : ∃ \A → (∅ ∈ A) ∧ (∀ X → X ∈ A → X ⁺ ∈ A)
  replacement : (A : Set) → (P : Set → Set₁) → ∃ \B → ∀ x → x ∈ B ⇔ (x ∈ A) ∧ P x
  powerset : (A : Set) → ∃ \B → ∀ X → X ∈ B ⇔ X ⊆ A

空集合の存在だけは(Data.Empty.⊥を使って)示せるので示した。

あとは命題の表現に便利そうな函数とか部分集合とか共通部分とか適当な補題を示したりした。
本に載っているままのやり方だけど

-- ``Russellのparadoxを回避"する命題。
cor-1-4 : (A : Set) → ∃ \B → B ∉ A

も示せた。

コメント

これだけのことが検索しても全くヒットしなくてつらかった。誰もAgdaで数学しないのかなって思った。

あと、仮定した公理が適切なものかどうかもよく分からない。なんか変なことしてたら教えてください。
選択公理とかも入れてもう少し綺麗にしてから自分のライブラリに入れて使おうと思います。

参考にした本

たまたま手元にあった。

集合と位相 (岩波基礎数学選書)

集合と位相 (岩波基礎数学選書)

コード

https://gist.github.com/myuon/ea11f62f9a9a9fed02b0

Printf実装を通して学ぶGADTs, DataKinds, ConstraintKinds, TypeFamilies

問題

問. Haskellで以下のようなCライクなprintf函数を実装してください。

> printf ["Hello, ", _s, "\n", "an integer:", _d, "\n", "a float:", _f] ["World!", (10 :: Int), (3.1415 :: Float)] 

-- 出力結果:
> Hello, World!
> an integer:10
> a float:3.1415

Cのprinfとは異なり、%dや%fが文字列に直接埋め込まれていません。よって当然型が合わなければ、すなわち printf [_d] [(3.1 :: Float)] などとかくとコンパイルエラーになってほしいわけです。

解答

私が実装したものが以下にあります。

https://gist.github.com/myuon/9084939

以下ではこのコードについて解説していきたいと思います。

解説

まず、printfの第一引数も第二引数もそれぞれの元の型はバラバラです。今はまだ_d_fの型をどうするかについては考えていませんが、とにかく型が違うということだけ分かればまずはヘテロリストの実装からスタートすることになります。

GADTs, DataKinds

ヘテロリストは全ての型がバラバラなので型を保持するのではなくてカインドを保持するようにします。つまり、普通のリストは型がaのデータを並べたものですが、今回実装するヘテロリストはカインドが*のデータを並べたものと考えます。

data HList (as :: [*]) where
  Nil :: HList '[]
  (:::) :: a -> HList as -> HList (a ': as)
infixr :::

HListの定義にはGADTとDataKindsが使われています。GADTはデータコンストラクタ函数のように定義できる*1もので、確かに上ではdata ... whereという書き方がされています。

DataKindsは定義したデータコンストラクタを型に、型をカインドに同じ名前のまま持ち上げるものです。分かりやすい例を挙げてみましょう。以下は簡単な型レベル自然数の例です。

data Nat = Zero | Succ Nat

-- DataKinds拡張を使うと、以下のようなものも自動で生成される
-- data Zero
-- data Succ (n :: Nat)
-- ただし Zero :: Nat, Succ n :: Nat である

これによって、標準的なリスト型は[]カインドに持ち上げられ、'[], (':)というデータコンストラクタを昇格してできた型が作られ、*カインドをもつ型のリストが使えるようになります。 このことを踏まえれば上のコードは、HListというデータ型の定義であって、asという変数はカインド*をもつ型のリストになっていることが分かります。(:::) :: a -> HList as -> HList (a ': as)によって、与えられた型をそのままリストに追加しているのが分かります。さらに実際に動かして型を調べてみるとよいでしょう。

> :t Nil
Nil :: HList ('[] *)

> :t "100" ::: (10 :: Int) ::: Nil
"100" ::: (10 :: Int) ::: Nil :: HList ((':) * [Char] ((':) * Int ('[] *)))

TypeFamilies, ConstraintKinds

さて、HListShowインスタンスにできるでしょうか。HListに登場する全ての型がShowインスタンスであればできそうです。このように型への制限を表すのがConstraintで、それをカインドのレベルで扱えるようにするのがConstraintKinds拡張です。

import GHC.Prim (Constraint)

type family All (cx :: * -> Constraint) (xs :: [*]) :: Constraint
type instance All cx '[] = ()
type instance All cx (x ': xs) = (cx x, All cx xs)

TypeFamiliesを使えば型を直接扱う函数を定義できます。これによってAllという型への制限を表す函数を定義します。cx :: * -> Constraintの部分に適当な型クラスがきます。例えばAll Showは、カインド*のリストxsに対し、その全ての元がShowインスタンスになっているという制限を表すことができるわけです。

コレを使ってHListShowインスタンスにしてしまいます。

instance (All Show as) => Show (HList as) where
  show Nil = "[]"
  show (x ::: xs) = show x ++ ":" ++ show xs

-- 実行例
-- > "100" ::: 4.2 ::: 10 ::: [1..5] ::: Nil
-- "100":4.2:10:[1,2,3,4,5]:[]

TextFの実装

以上でヘテロリストが実装できました。これを使えば我々の目的であるprintf函数の型も大体見当がつくでしょう。

printf :: HList as -> HList bs -> IO ()
printf x y = undefined

printfは2つのHListxとyを受け取って、もしもxの先頭がString型であれば、それをそのまま出力します。そうでなければ、xの先頭とyの先頭の型があっているか(xの先頭が_dだったらyの先頭はInt型であるか)を判断して、合っていればそれを出力します。このようにprintfは型によって実装が変わるので、型クラスの出番です。

class TextF as bs where
  textf :: HList as -> HList bs -> String

また、printfはIO ()になって少し扱いにくいので、textf :: HList as -> HList bs -> Stringという純粋函数を定義して、それを使ってprintfを実装することにしました。

いよいよ実装です。まずは、それぞれのリストas, bsがともに空である場合。

instance TextF '[] '[] where
  textf _ _ = ""

そして、asの先頭がString型かどうかでパターンマッチを行います。

instance (TextF as bs) => TextF (String ': as) bs where
  textf (x ::: xs) y' = x ++ textf xs y'
 
instance (TextF as bs) => TextF ((x -> String) ': as) (x ': bs) where
  textf (x ::: xs) (y ::: ys) = x y ++ textf xs ys

asString型のデータか、x -> String型の函数が入っているということにしました。つまり、_d_f_d :: Int -> String, _f :: Float -> Stringの型であって、さらに_d 10_f 3.1415などの値が画面に出力されることになります。 よって、このような_d_fshowそのものですから、これを定義してあげることにします。

_d :: Int -> String
_d = show
 
_s :: String -> String
_s = id
 
_f :: Float -> String
_f = show

(String -> Stringだけは、そのままshowするとクォーテーションがついてくるのでそのままにしてあります。)

まとめ

以上で、printfの実装が完全に出来ました。 では実際に動かして遊んでみましょう。

> printf Nil Nil

> printf ("hello!" ::: _s ::: Nil) ("world!" ::: Nil)
hello!world!
> printf ("hoge:" ::: _d ::: Nil) (3.1415 ::: Nil)
*** 型エラー ***
> printf ("hoge:" ::: _d ::: Nil) ((20 :: Int) ::: Nil)
hoge:20
> printf ("hoge:" ::: 10 ::: Nil) (Nil)
*** 型エラー ***

はい、正しく動いているようです。

なお、問ではこれを printf ["hello","world!"] [] のようにリストカッコを用いて書くように言っていましたが、そのようなリストの表記を使えるようにするGHC拡張として、OverloadedListsが提案されているようです。 また、このprintfをCと同じように可変長引数にすることは頑張ればできると思うのでよければやってみてもいいかもしれません。(丸投げ)*2

GADTs, DataKinds, ConstraintKinds, TypeFamiliesなどのGHC拡張を使えば、このような型レベルプログラミングも比較的[要出典]簡単に実装することができます。便利なGHC拡張はドンドン使っていきましょう。

参考

参考にしたページと参考になりそうなページ

*1:各データコンストラクタの像を適当な形に制限するために使うものだと思っていますが正確なところは知りません

*2:型クラスを用いた可変長引数の実装はText.Printfが分かりやすいと思います。

Haskellでもできる!実践・オブジェクト指向

Lensにほとんど触れたことのない人にはこちらの記事がオススメです:Lensで行こう! - Just $ A sandbox

Haskellでもオブジェクト指向をしましょう!
Haskellは直接オブジェクト指向的な機能を提供してはいませんが、我らがLensの力を借りることでオブジェクト指向的な設計を意識したコーディングが可能です。

今回利用するのは主に以下のモジュールです。

Lensのおさらい

Lensを使ったことのある人にはおなじみだと思いますので、特に解説はしません。

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t  -- Lens型(GetterやSetterの一般形)
type Lens' s a = Lens s s a a  -- Lensの省略形

(^.) :: s -> Getting a s a -> a  -- 値をgetする
(.~) :: ASetter s t a b -> b -> s -> t  -- 値をsetする
(%~) :: Profunctor p => Setting p s t a b -> p a b -> s -> t  -- 函数を適用したものをsetする
(.=) :: MonadState s m => ASetter s s a b -> b -> m () -- 値をMonadStateの文脈でsetする( (.~)のMonadState版 )
(%=) :: (Profunctor p, MonadState s m) => Setting p s s a b -> p a b -> m () -- 函数を適用したものをMonadStateの文脈でsetする( (%~)のMonadState版 )
(<~) :: MonadState s m => ASetter s s a b -> m b -> m ()  -- アクションを実行した結果をsetする

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b  -- getterとsetterからLensをbuildする

特に最後のlens函数は重要です。例えば適当なdata型をmakeLensesするとき、何が起こっているかを明示すると

data Hoge a b = Hoge { _foo :: a, _baz :: b }
makeLenses ''Hoge

-- 以下が生成される
foo :: Lens' (Hoge a b) a
foo = lens _foo (\h x -> h { _foo = x })

baz :: Lens' (Hoge a b) b
baz = lens _foo (\h x -> h { _baz = x })

となります。 lensに、getter :: Lens' s a -> asetter :: Lens' s a -> a -> Lens' s aを渡すことで、出来上がるlens getter setterは上手くLensとして振る舞ってくれます。

型クラスとオブジェクト

Lensでオブジェクトを定義しましょう。
例として、ブロック崩しゲームのようなものを考えてみましょう。ブロック崩しには当然、ボールやバーが必要ですのでこれを定義してみます。

data Ball = Ball { _posBall :: (Int, Int), _velBall :: (Int, Int), _r :: Int } deriving (Eq, Show)
makeLenses ''Ball

data Bar = Bar { _posBar :: (Int, Int), _velBar :: (Int, Int), _width :: Int, _height :: Int } deriving (Eq, Show)
makeLenses ''Bar

posHogeはオブジェクトの座標にあたります。わざわざ名前を変えているのは、函数の多重定義になってしまうからです。また、オブジェクトは座標を更新して動かしたいので、このようなメソッドを定義します。
Haskellでは、いわゆるメソッドに当たる部分は型クラスのメソッドとして定義します。メソッドはオブジェクトに関する値を戻り値にとる函数というよりもオブジェクト自体を操作する函数であることが多いのでデータ型とは分けて定義するほうが便利です。また、型クラスのメソッドなら、同じ名前でもデータ型によって異なる振る舞いが定義できます。

class Move c where
  update :: State c ()

instance Move Ball where
  update = do
    (vx,vy) <- use velBall
    posBall %= (\(x,y) -> (x+vx, y+vy))

instance Move Bar where
  -- Barは横にしか動けない
  update = do
    (vx,_) <- use velBall
    posBar %= (\(x,y) -> (x+vx,y))

特に意味はないですが、オブジェクトによって函数の振る舞いを変えることが出来ました。
さて、posBallposBarが同じ座標を表しているのに名前が違うのは何かと面倒なので、これも型クラスを使ってまとめてしまいます。

class HasPos c where
  pos :: Lens' c (Int, Int)

instance HasPos Ball where
  pos = posBall
instance HasPos Bar where
  pos = posBar

はい、これでposBallposBarを区別する必要はありません。これを使えば、posをもつ任意の要素に対するメソッドが定義できます。

reset :: (HasPos c) => State c ()
reset = do
  pos .= (0,0)

resetHasPos型クラスのインスタンスならなんでも適用できます。つまり、BallBarはどちらもresetで操作をすることができるわけです。便利ですね!

Classyとサブクラス

さて、上ではHasPosを定義して名前の衝突を防ぎましたが、これを共通する全ての函数について行わなければならないのは面倒です。そこで、posvelなどの共通するメンバをもつ抽象クラスを作り、BallBarはこれらを内部に含む(ある意味ではサブクラス・継承したクラスのようなもの)クラスとして定義することにしましょう。

data GameObj = GameObj { _pos :: (Int, Int), _vel :: (Int, Int) }
makeClassy ''GameObj

-- 以下が自動生成される
class HasGameObj c where
  gameObj :: Lens' c GameObj

instance HasGameObj GameObj where
  gameObj = id

pos :: (HasGameObj c) => Lens' c (Int, Int)
vel :: (HasGameObj c) => Lens' c (Int, Int)

makeClassyGameObjからHasGameObj型クラスを生成します。これによって、HasGameObjインスタンスになったものは自由にposvelを使えるようになります。
どういうことか見てみましょう。

data Ball = Ball { _ballObj :: GameObj, _r :: Int } deriving (Eq, Show)
makeLenses ''Ball

instance HasGameObj Ball where
  gameObj = ballObj

これでBallHasGameObjインスタンスになったので、b :: Ballに対してb ^. posとかb & vel .~ (1,0)などとかけるようになったわけです。

また、少しデザインパターン的ですが、自分自身を更新する函数を内部に持つオブジェクトの定義も出来ます。
同じ型を持つオブジェクトの実装を変えられるようにしたい -qiita

これは、例えば変な動きをするボールを作りたいときに、ボールの動きをデータの生成時に指定したいみたいな状況で使えると思います。
(上の記事のAutonomieの実装を参照。autoを例えばBall型で、runAutoState Ball ()とすればこのような実装も可能。)

ここまででかなりのことはできるようになったと思います。
今回は記事タイトルの通り、「実践」を意識した解説を行いました。例えば私はChimeraという弾幕シューティングゲームを全てHaskellで実装していますが、Lensはこれくらい本格的なプロジェクトになっても通用するレベルの強力さを秘めています。

Lensは(たぶん)他にも使い方があります。あなたもこの強力なライブラリで快適なHaskellコーディングを楽しみましょう!
さあいますぐインストール! *1

*1:2014/02/02時点でlens-4.0がリリースされています。