3

レンズを理解するためにこの記事を読んでいます。これが Edward Knett のレンズ パッケージとは異なることは承知していますが、それでも基礎には役立ちます。

したがって、レンズは次のように定義されます。

type Lens a b = (a -> b, b -> a -> a)

レンズがカテゴリを形成することが言及されており、私は型クラスのインスタンスを作成しようとしていますCategory。まず、関数の型定義を書きました。

(.) :: Lens y z -> Lens x y -> Lens x z
id :: Lens x x

そして、この後、私は一日中それを見つめています。その定義を書くための思考プロセスは正確には何ですか？

4

3 に答える 3

4

私はこの記事(Joseph Abrahamson による fpcomplete の Lenses from Scratch) が非常に優れていることを発見しました。それはあなたが始めたレンズの同じ表現から始まり、その構成を定義し、レンズにもっと似た表現への道に沿って続きます。

編集:この種のことを行う場合、タイプホールが優れていることがわかります:

(<.>):: Lens y z -> Lens x y -> Lens x z
(getA,setA) <.> (getB,setB) = (_,_)

これで 2 つの穴ができました。タプルの最初の部分には (出力が消去されました) と書かれています。

Found hole ‘_’ with type: x -> z
...
Relevant bindings include
  setB :: y -> x -> x
  getB :: x -> y
  setA :: z -> y -> y
  getA :: y -> z
  (<.>) :: Lens y z -> Lens x y -> Lens x z

バインディングをよく見ると、必要なものはすでに揃っています。getB :: x -> yそしてgetA :: y -> z関数合成と一緒に(.) :: (b -> c) -> (a -> b) -> a -> c

したがって、喜んでこれを挿入します。

(<.>):: Lens y z -> Lens x y -> Lens x z
(getA,setA) <.> (getB,setB) = (getA . getB, _)

そして、次のような 2 番目のタイプの穴に進みます。

Found hole ‘_’ with type: z -> x -> x
Relevant bindings include
  setB :: y -> x -> x
  getB :: x -> y
  setA :: z -> y -> y
  getA :: y -> z

私たちが持っている最も類似したものはsetA :: z -> y -> y、ラムダを挿入して引数をキャプチャすることから始めます。

(getA,setA) <.> (getB,setB) = (getA . getB, \z x -> _)

タイプホールを次のように変更します。

Found hole ‘_’ with type: x
Relevant bindings include
  x :: x
  z :: z
  setB :: y -> x -> x
  getB :: x -> y
  setA :: z -> y -> y
  getA :: y -> z

型チェックを挿入することはできxますが、必要なものは得られません (設定しても何も起こりません)。を与えることができる唯一の他のバインディングxは issetBであるため、それを挿入します。

(getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB _ _)

最初のタイプの穴は次のように述べています。

Found hole ‘_’ with type: y
Relevant bindings include
  x :: x
  z :: z
  setB :: y -> x -> x
  getB :: x -> y
  setA :: z -> y -> y
  getA :: y -> z

したがって、y が必要で、スコープ内にあるものを見て、を与えると a を与えることgetBができますが、これはたまたま持っていますが、これは役に立たないレンズにつながり、再び何もしません。別の方法は、次を使用することです。yxsetA

(getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA _ _) _)

(ここから少し速度を上げていきます) ここでも、最初の穴はz、ラムダへの引数としてたまたま持っている型の何かを必要としています。

(getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA z _) _)

type の最初の型の穴を埋めるために、ラムダの引数を指定してy使用できます。getB :: x -> y

(getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA z (getB x)) _)

これにより、残りのタイプ ホールが 1 つ残ります。これは、簡単に に置き換えることができx、最終的な定義につながります。

(<.>):: Lens y z -> Lens x y -> Lens x z
(getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA z (getB x)) x)

id必要に応じてタイプ ホールとフーグルを使用して、自分で定義を試みることができます。

于 2014-03-14T12:37:30.463 に答える
1

それはかなり簡単なプロセスのようです。idただし、カテゴリを取得することも確認する必要があります-これには等式の推論が必要です-たとえば、 with型のセッターを実装する方法が少なくとも1つあるため、x->x->xそのうちの1つだけがカテゴリを作成します。

それでは、適切なタイプの関数を取得することから始めましょう。

Lens y z -> Lens x y -> Lens x z ==
(y->z, z->y->y) -> (x->y, y->x->x) -> (x->z, z->x->x)

x->zから取得する方法x->yと作成する方法は明らかy->zです。さて、xoldxと newから new を構築する方法と、 oldから oldyを取得する方法があるので、 new fromと oldを構築できれば完了です。yxyzy

(.) (yz, zyy) (xy, yxx) = (yz . xy, \z x -> yxx (zyy z (xy x)) x)

id についても同様:

Lens x x ==
(x->x, x->x->x)

そう

id = (id, const)

これまでのところ、タイプはチェックされています。では、カテゴリがあることを確認してみましょう。1 つの法律があります。

f . id = f = id . f

一方向の確認 (少し非公式なので、 と で異なることを参照する必要があることに注意してください.) :idf . idfg . id

f . id = (fg, fs) . (id, const) =
(fg . id, \z x -> const (fs z (id x)) x) =
(fg, \z x -> fs z (id x)) = (fg, fs)

他の方法で確認する:

id . f = (id, const) . (fg, fs) =
(id . fg, \z x -> fs (const z (fg x)) x) =
(fg, \z x -> fs z x) = (fg, fs)
于 2014-03-14T14:42:12.120 に答える
1

これを試して：

(.) :: Lens y z -> Lens x y -> Lens x z
(getZfromY , setZinY) . (getYfromX , setYinX) = (getZfromX , setZinX)
             where getZfromX someX = ...
                   setZinX someZ someX = ...

アイデアは、2 つのゲッターを組み合わせて新しいゲッターを作成し、2 つのセッターを組み合わせて新しいセッターを作成することです。

ID については、次のことを考えてください。

id :: Lens x x
id = (getXfromX , setXinX)
    where getXfromX someX = ...
          setXinX newX oldX = ...
于 2014-03-14T12:42:44.620 に答える