日々の流転

λ. Recursive types for free!, Philip Wadler

正負両方の位置にパラメータの現れるオペレータが不動点を持つような時のパラメトリシティの話かと思ってたのだけど、そうではなくて正の位置にパラメータの現れるオペレータの最小不動点と最大不動点を二階ラムダ計算で表現する話だった。

Fの最小不動点 μX.F(X) は ∀X.(F(X)→X)→X 、Fの最大不動点 νX.F(X) は ∃X.(X→F(X))×X で表される。それぞれ、weak initial F-algebra と weak final F-coalgebra になっていて、パラメトリシティが成り立つときに initial F-algebra と final F-coalgebra になる。

λ. パラメトリシティと不動点

パラメトリシティを仮定すると μX.X = ∀X.(X→X)→X によって initial object 0 を定義できる。ここでさらに不動点コンビネータを導入すると、不動点と有限直和を持つCCCの議論から困ったことになってしまう。不動点コンビネータとパラメトリシティは相性が悪い。

Theorems for free! では、不動点コンビネータを導入する場合には、パラメトリシティの適用できる関係を連続かつ正格なものに制限する必要があるとあった。μX.F(X) = ∀X.(F(X)→X)→X が initial F-algebra になることを示すには任意の射を関係として使えることが必要だったので、このような制限があれば、このμX.F(X)は initial F-algebra にはならない。これはまさにHaskellの場合で、Haskellで定義されるデータ型は weak initial algebra ではあるけど、initial algebra にはなっていない。

また、パラメトリシティと不動点を両立(?)させるには、そもそもCCC(= ラムダ計算)を諦めてしまって、線形論理を代わりに使うといったアプローチもあるみたい。

The Theory of Twiners and Linear Parametricity (Note), Ryu Hasegawa

λ. OCaml入門 (2): variance

OCamlは型定義の際にパラメータのvarianceを明示することが出来るそうだ。試してみる。

# type +'a foo = Foo of ('a -> unit) ;;
Characters 5-34:
  type +'a foo = Foo of ('a -> unit) ;;
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
In this definition, expected parameter variances are not satisfied
# type -'a bar = Bar of 'a ;;
Characters 5-24:
  type -'a bar = Bar of 'a ;;
       ^^^^^^^^^^^^^^^^^^^
In this definition, expected parameter variances are not satisfied

ふむふむ。確かにvarianceと矛盾する位置に変数が現れるとエラーになってくれますな。もう少し試す。

# type -'a foo = Foo of int ;;
type 'a foo = Foo of int
# type +'a bar = Bar of 'a foo ;;
type 'a bar = Bar of 'a foo

ありゃ。これはエラーにならないのか。ということは、型の定義中にはユーザに与えられたvarianceを使ったチェックを行うけど、一旦定義された型が他で使われたときには、ユーザによって与えられたvarianceではなく推論されたvarianceを使うということなのかな。

λ. 第四回圏論勉強会

今日は例の圏論勉強会の第四回目だった。

• CategoryTheory:圏論勉強会 (sampou.org, Programming in Haskell)

ところで、Conceptual Mathematics: A First Introduction to Categories, F. William Lawvere, Stephen H. Schanuel という本をテキストとして使っているのだけど、実は僕がこの本を注文したのは丁度3年前の今日だった。あれから、3年間で自分は少しは成長できただろうか?