2020/7の近況とラムダキューブについて

#tryangle勉強会

※このスライドはかなり雑に書いていますmrsekut.icon

概要を知るには良いかもしれませんが、真に受けないように。

久々に会う人と勉強会をしたのでこんなごっちゃな内容になっていますmrsekut.icon

アジェンダ

最近のmrsekut.iconの状況

ラムダキューブについて

多相について

型演算について

依存型について

mrsekut.iconのここ1年の雑話

2019年下半期に以下の分野を独立しているものだと思って独立に本を読んだりしていた

言語処理系

型理論

圏論

数理論理学

計算理論

全部の分野がそこまで関連しているものではないと思っていた

なんとなくこの辺好きだな〜と思っていた

ref /public-mrsekut/意味論周辺のつながりを知ったタイミング

各分野の出会いはかなりバラバラ

言語処理系

tcfm、『Go言語でつくるインタプリタ』

型理論

仕事のTS、趣味のHaskell

圏論

2019/9頃に元インターン上司が開催した圏論勉強会

数理論理学

3回生の後期に適当に授業をとった

計算理論

3回生の後期に適当に授業をとった

3回生の後期に大学の図書館で適当に本を手にとった

『(理論)12 計算モデルの基礎理論』.icon

チューリングマシン、ラムダ計算、帰納的関数論などの「計算モデル」を紹介する本

なんで手に取ったか不明だがこれを読んで色々繋がっていることに気付いた

なんとなく面白いな、と思っているものたちが繋がっていることを知った

mrsekut.iconはこの辺の分野を全部ひっくるめて「意味論ちっくなもの」と呼んでる

https://gyazo.com/92d7205760ac48c35fc25d8ceb187b90

ここからは型の話

型理論界隈にはラムダ・キューブと呼ばれる立方体がある

https://gyazo.com/61ff0a55c6cec65e2db0d4c105361c6f

もう少しわかりやすく日本語で書くとこう

https://gyazo.com/8e0e17559971ee64c2112ca4028c9743

原点の単純型付きラムダ計算から

赤線の方向に、型演算

緑線の方向に、多相

青線の方向に、依存型

手前上の線、青色つけ忘れてた(てへぺろ)

に伸びている

それ以外の頂点は合わせたもの

https://gyazo.com/0d894859021194594d9f0b9cfda6b88a

例えば$ \lambda P2は

青方向、緑方向に進んだところにあるので

多相+依存型

原点と反対側にあるCalculus of Constructionsは全部入り

略してCoCと書く

コックと読む

つまりCoqである

単純型付きラムダ計算とは？

今回はそんな重要ではない

ラムダ計算は1930年代に考案された計算モデル

今の関数型プログラミングの基礎理論

計算の本質を見出すために「関数定義」と「関数適用」のみでプログラムを作る

それに型を付けて考えたものが型付きラムダ計算

その中でも特に一つの基本型のみを扱うのが単純型付きラムダ計算

多相と型演算は割と知られている

身近にある

多相

多相にもいろいろあるがラムダ・キューブで指しているのはパラメトリック多相

最も身近な例はGenerics

最もシンプルな例がこういう恒等関数

code:js

const id = x => x;

これにどうやって型を付けようか？が論点

普通にやると型が限定されてしまう

code:ts

// id :: string -> string

const id = (x: string) => x

このid関数をnumberやboolにも使いたい場合、他の関数を用意しないといけない

名前がコンフリクトするので

code:ts

// idNum :: number -> number

const idNum = (x: number) => x

// idBool :: boolean -> boolean

const idBool = (x: boolean) => x

良くない

多相を使って解決

code:ts

// id :: T -> T

const id = <T>(x: T) => T

code:hs

id :: a -> a

id x = x

多相まとめ

Genricsみたいなやつ

「同じ実装」に対して「異なる型」をつける

型理論ではSystem Fという体系で頑張る

型演算

型の型を扱う

TypeScriptだけだと説明が難しいがこんなイメージ

Genericな型を型関数と見る

型Maybe<T>は、「型を一つ引数に取って、型を返す型関数」と見る

Maybe :: T -> Maybe<T>というイメージ

型Either<T, E>は「型を2つ引数に取って、型を返す型関数」と見る

Either :: T -> E -> Either<T, E>というイメージ

つまり型にも型がある

Maybeという型に対して、2つの型は引数に取れないでしょmrsekut.icon

具体的な型を*と表すならMaybe :: * -> *になる

同様にして、Either :: * -> * -> *になる

さらに型の型に対する制約を考えることができる

以下のHigherKinded型は2つの型引数を取る

code:hs

data HigherKinded f a

= Bare a

| Wrapped (f a)

fとaは型引数

f aを見ると、fは* -> *である必要があることがわかる

なのでHigherKindedは

Eitherと同様に「2つの型引数を取る」が、

ただの* -> * -> *ではだめで

(* -> *) -> * -> *のような型でないといけないことがわかる

型演算まとめ

「型の型」のことを「kind」と呼ぶ

型の型の制約を扱う

例えば(* -> *) -> * -> *の二番目の*はIntじゃないといけない、とか

高階多相型に書いている

依存型

これはTSでは説明は無理mrsekut.icon

依存型を使える言語の例

Coq

Idris

Agda

ATS

HaskellやScalaでもライブラリを使えば、っぽいことはできる(らしい)

依存型とは

値に依存している型

値というのは値コンストラクタのこと

Bool = True | FalseのTrueとかFalse

Int = 0 | 1 | 2 | ..の0とか1とか

値と型を同等に扱える

よくある例

Vect型

Vect n a

自然数の型nと、任意の型aを型引数に取る

以下の値xsは、「Int型の要素を5個持つ」

ということを型でも表現している

code:例.hs

xs : Vect 5 Int

xs = 1,2,3,4,5

(本来Idrisの拡張子は.idrだが、スクボのシンタックスハイライトが対応していないので.hsにしている)

Vect同士を連結する関数を定義してみる

こんなふうにVectどうしを連結する関数(++)を定義してみる

code:hs

xs : Vect 5 Int

xs = 1,2,3,4,5

ys : Vect 3 Int

ys = 6,7,8

xs ++ ys -- > 1, 2, 3, 4, 5, 6, 7, 8 : Vect 8 Int

特に型に注目

code:hs

(++) : Vect n a -> Vect m a -> Vect (n + m) a

(++) Nil ys = ys

(++) (x :: xs) ys = x :: (xs ++ ys)

型の中で演算が行われている

Vect (n + m) a

一般的な(?)型システムではできない配列の境界値検査ができるのが嬉しい

依存型の他の応用例 ref

プログラムの証明

固定長の配列、行列

依存型を使ったニューラルネットワーク ref

スーパーモナド

データベースのスキーマ

依存型まとめ

型の中で値を扱える

型の表現力が上がる

証明によく使われるが、Idrisは汎用プログラミング言語を目指している

依存型やIdrisで依存型に触れるに書いている

全体まとめ

ラムダキューブは「パラメトリック多相」「型演算」「依存型」よりなる

CoCはヤバい

ラムダキューブを更に一般化した「Pure Type System」なるものもある

人類は全てを型でやりたくなる