mod_poppoが型付きラムダ計算の処理系を実装する日記

mod_poppo @mod_poppo

関数呼び出し1回につき型強制が2回発生する可能性があるわけだが、その度に恒等関数が挿入されるのは流石に避けたほうがいい気がしてきた

mod_poppo @mod_poppo

「入門LiquidHaskell−篩型による静的コード解析−」を Dodgson Labs で購入しました！ dodgsonlabs.booth.pm/items/490689 #booth_pm

mod_poppo @mod_poppo

「型システム入門」は入門書なので、依存型のようなトピックは「発展」と言う扱いになっている

mod_poppo @mod_poppo

ブログ更新した / 型システムの勉強 blog.miz-ar.info/2017/07/type-s…

κeen @blackenedgold

ダメポ、TaPL読んだことなかったんだ

κeen @blackenedgold

> Rank 2 と Rank 3 以上では型再構築に関して違いがあるらしい。 へー。

. @fetburner

Rank 3から決定不能になるんすよ

κeen @blackenedgold

そういやSystem F決定不能だった

κeen @blackenedgold

TaPL、2回くらい目を通したけど練習問題も実装演習もやってないからそろそろちゃんとやんなきゃって思ってる

mod_poppo @mod_poppo

今までは型システムを使うだけだったからTaPL読まなくても割となんとかなってきたけど、自分で真面目に実装しようと思った時にTaPLは最低限読んでおかなくてはと思った（TaPLは発展的な内容に関しては紹介程度に留まっているので、TaPLを読めば十分と言うわけではない）

. @fetburner

TaPL，輪講で良く理解していない証明を解説中に先生に突っ込まれまくり，結局本の定義が間違ってないかとなったことがあった

κeen @blackenedgold

TaPLってML多相の実装載ってるっけ？

. @fetburner

TaPLのエラッタは面白くて，例えば27章は前提が誤っているので内容丸々信用できないとかあります

. @fetburner

@blackenedgold 正当性と健全性の証明とかならあります

κeen @blackenedgold

@fetburner OCamlの実装はないんですね

. @fetburner

@blackenedgold OCamlでの実装はないですね．あと見直してみたら証明はSTLC相当のもので，ML多相のは推論規則の紹介とかで終わってました

κeen @blackenedgold

@fetburner TaPLって細かいところ詰めようとするとやっぱ入門書だなってなりますよね

. @fetburner

@blackenedgold 確かにそういう所ありますね．面白そうな話は散りばめていても詳しくは触れない．

yhara (Yutaka HARA) @yhara

"The whole of chapter 27 is not very convincing." cis.upenn.edu/~bcpierce/tapl… これか… twitter.com/fetburner/stat…

mod_poppo @mod_poppo

型システムをやっている場合ではなくて、本業の数学をやらないといけないのだ

mod_poppo @mod_poppo

この型検査器には問題がある！

mod_poppo @mod_poppo

俺、このバグが取れたら高カインド型と依存型を追加してCalculus of Constructionsを実装するんだ……。

mod_poppo @mod_poppo

やっぱ型に関するエイリアスみたいなのを言語の中できたら便利なのでは。型レベルラムダ計算へGOだな

mod_poppo @mod_poppo

言語としては型エイリアスみたいなものは持っていないが、REPLでは型エイリアスを定義できるようにしたい。パース時に型エイリアスの一覧を与えるようにするのが一番いいか？