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

mod_poppo @mod_poppo

ラムダ計算はむずかしい

mod_poppo @mod_poppo

System Fの実装をでっち上げた（軽く試した限りでは動いているように見えるがどこかでバグっているかもしれない） github.com/minoki/LambdaQ… pic.twitter.com/PweHxCF3h7

拡大

mod_poppo @mod_poppo

画像は、みんな大好きチャーチ数で 1+1 を計算しているところです（ただし表示するために組み込みの整数に変換している）

mod_poppo @mod_poppo

本当に実装したいものはまだこの先にあるのに、System Fだけで丸一日かかってしまったな

mod_poppo @mod_poppo

readlineのHaskellバインディングを使う際にリンクエラーが出る件は、readlineのライブラリパスを設定せずに ghc-options に -optl/opt/local/lib/libreadline.dylib みたいなのを設定すると良い

スマートコン @mr_konn

readline 使うのはやめて Haskeline を使うという手もある

mod_poppo @mod_poppo

consの定義が上手くいかない…

mod_poppo @mod_poppo

環境にある型を参照するやつがうまくいってないっぽいな

mod_poppo @mod_poppo

ラムダ計算マスターへの道は遠い

mod_poppo @mod_poppo

ラムダ計算の民のためのHaskell入門

mod_poppo @mod_poppo

部分型関係の公理（？）から推移律を取り除いても問題ないみたいなやつ、カット除去みを感じさせる

mod_poppo @mod_poppo

頑張ってデバッグした結果、リストが動くようになった pic.twitter.com/rIO30jkk6n

拡大

mod_poppo @mod_poppo

そろそろFsubの実装に取り掛かりたいけど、レコードがなくても Int <: Real みたいな非自明な部分型関係があればFsub名乗っていいよね？

mod_poppo @mod_poppo

System Fsubを実装した（ということにしておく）。型強制意味論によるSystem Fへの変換も実装したいけど、少し面倒くさそうなのでまた今度にしよう

mod_poppo @mod_poppo

型変数に関する文脈と通常の変数に関する文脈を別々に扱うのは不合理だということに気づいてしまったし、TaPLのサンプルコードがその辺どうしているのかちゃんと読み込む必要がある

mod_poppo @mod_poppo

言語自作沼に首まで浸かっている

画力・博士号・油田 @bd_gfngfn

オッ，言語自作沼はいいぞ

画力・博士号・油田 @bd_gfngfn

言語自作沼よくて，大学院入試の面接の待ち時間にも処理系の改造をやるようになる．

mod_poppo @mod_poppo

最終的には各種アセンブリを吐き出すところまで行きたい

mod_poppo @mod_poppo

束縛への参照を内側から数えたインデックスで表すやつの名前を間違えて覚えていたようだ

mod_poppo @mod_poppo

部分型付けの型強制意味論を実装するの、型チェックを丸ごと再実装することになってつらい（実際の言語を実装する際は最初から型強制意味論で実装してしまえばいいからこんなことにはならない）

mod_poppo @mod_poppo

依存型のある言語で証明しながら言語処理系を書きたい

mod_poppo @mod_poppo

素直に実装したら恒等関数が大量発生して見た目がひどいことになりそう

mod_poppo @mod_poppo

LiquidHaskellってよく知らないけど調べてみるべきか