Leibniz

ライプニッツの同値関係を表したものだ。scalaの=:=もそうだが、これの強化版が===だ。

使う前にまず確認用の型を定義してみよう。

trait Space
trait Earth extends Space
trait Japan extends Earth
trait Tokyo extends Japan

早速つかってみよう。

implicitly[Space === Space]
// ok
implicitly[Space === Earth]
// err

implicitly[Space =:= Space]
// ok
implicitly[Space =:= Earth]
// err

うん。scalaの=:=と同じだ。

=:=は関数として取得できる。

===はLeibnizのインスタンスを返す。しかし関数にもなれる。

scala> implicitly[Space === Space]
res1: scalaz.Leibniz.===[Space,Space]

scala> implicitly[Space === Space]: (Space => Space)
res2: Space => Space = <function1>

Leibnizの定義をみてみよう。

sealed abstract class Leibniz[-L, +H >: L, A >: L <: H, B >: L <: H]

type ===[A,B] = Leibniz[⊥, ⊤, A, B]

⊥はNothingで、⊤はAnyだ。そしてAとBをとるのが===だと。

そしてLeibnizは、ちょっと複雑なので具体化してみてみよう。

Leibniz[
  -Nothing, // -L
  +Any >: Nothing, // +H
  A >: Nothing <: Any,
  B >: Nothing <: Any
]

AはNothing以上で、Any以下と。Bも同様。

つまりScala界での境界を表している。

すべてのクラスはAnyの子だというのは知っていたが、Nothingの親というのは気づかなかった。確かにそうか。

ということは、自分で世界を定義できるのでは。

type =::=[A >: Tokyo <: Space, B >: Tokyo <: Space] = Leibniz[Tokyo, Space, A, B]

implicitly[Space =::= Space]
//ok

implicitly[Any =::= Any]
//err

いや自分で範囲を決めたらそうなるか。

合成してみよう

composeはtransを使ってるのでtransをみてみる。

def trans[L, H >: L, A >: L <: H, B >: L <: H, C >: L <: H](
  f: Leibniz[L, H, B, C],
  g: Leibniz[L, H, A, B]
): Leibniz[L, H, A, C]

推移律だからA=>Cが返るようだ。

しかし===はAとBが同じでないといけないものだ。

つまり、A=>CはAでしかない。

分かりやすいように型aliasをつけてみよう。

type SpaceA = Space
type SpaceB = Space
type SpaceC = Space

trans[Nothing, Any, SpaceA, SpaceB, SpaceC](implicitly[SpaceB === SpaceC], implicitly[SpaceA === SpaceB])
// Leibniz[Nothing,Any,SpaceA,SpaceC]

まぁA=>Cになってるけど、ようはSpaceに変わりない。

一応composeも。

implicitly[SpaceB === SpaceC] compose implicitly[SpaceA === SpaceB]
// Leibniz[⊥,⊤,SpaceA,SpaceC]

うんSpaceに変わりない。

AとBを逆にする関数もあった。symmだ。

Leibniz.symm[Nothing, Any, SpaceA, SpaceB](implicitly[SpaceA === SpaceB])
// Leibniz[Nothing,Any,SpaceB,SpaceA]

逆にしても同じものは同じだ。

ほかのインスタンス関数

関数にして返すonFというのがあった。

implicitly[Space === Space].onF[Int](i => new Space{})
// Int => Space

(onCovとonContraに関しては嘘書きましたxuweiさんにコメントよんでくださいm(_ _)m)↓

onCovというのもあったが、共変のものを受け取るようだがFunctorだったらなんでもいいという定義で、反変も受け取れる。これが間違っているのか意図的なのか分からない。

implicitly[Space === Space].onCov(Option(new Space{}))
// Option[Space]

~~反変を受け取るものもあった。これは反変しか受け取れないようだ。そういう定義なっていた。~~

implicitly[Space === Space].onContra({(s:Space) => s})
// Space => Space

implicitly[Space === Space].onContra(Option(new Space{}))
// err

lift

ちゃんとOptionの中身も検査するために必要な型が多いようだ。

Leibniz.lift[Nothing, Nothing, Any, Any, Option, SpaceA, SpaceB](implicitly[Space === Space])
// Leibniz[Nothing,Any,Option[SpaceA],Option[SpaceB]]

liftされた。

型を2つとる型もいけるようだ。しかしlift2はやばい。定義からしてやばい。

def lift2[
    LA, LB, LT,
    HA >: LA, HB >: LB, HT >: LT,
    T[_ >: LA <: HA, _ >: LB <: HB] >: LT <: HT,
    A >: LA <: HA, A2 >: LA <: HA,
    B >: LB <: HB, B2 >: LB <: HB
  ](
    a: Leibniz[LA, HA, A, A2],
    b: Leibniz[LB, HB, B, B2]
  ) : Leibniz[LT, HT, T[A, B], T[A2, B2]]

使うほうもやばい。11個の型パラメータが必要だ。

Leibniz.lift2[Nothing, Nothing, Nothing, Any, Any, Any, Writer, SpaceA, SpaceA, SpaceB, SpaceB](implicitly[SpaceA === SpaceA], implicitly[SpaceB === SpaceB])
// Leibniz[Nothing, Any, Writer[SpaceA,SpaceB], Writer[SpaceA,SpaceB]]

lift3もあるが、もういいだろう。

unlift

unliftする関数もあった。lowerとかいうやつだ。

Leibniz.lower[Nothing, Any, Option, SpaceA, SpaceB](implicitly[Option[SpaceA] === Option[SpaceB]])
// Leibniz[Nothing, Any, SpaceA, SpaceB]

unliftできた。

数学的すぎてついていけない感じだ。

今日はここまで。