型推論がある型システムを実装した上で改善していく。 具体的には TaPLのType Reconstruction準拠の単相な型推論を純粋関数型な単一化で実装 型変数の作成と単一化を破壊的代入で行うようにする（効率化） 型推論をLet多相に拡張 型変数を汎化していいかの確…

typeof関数のRefとError関連のケースを部分型に対応させる。今回でエラーに関する話は最後。 Ref 以前書いたとおり、安易にRefにBottomを含む型を持たせると型安全性が破壊されてしまう。なのでRefに入る値の型にはBottomがまったくないという厳しめの制約を…

今回はtypeof関数がレコード、バリアント、Fix関連でどう部分型に対応していくかを見ていく。 レコード レコードはフィールドの値が一つでもBottom型だったら全体がBottom型になる： | ERecord les -> let lts = (List.map (fun (l,e)->(l, typeof env e)) l…

今回はtypeof関数がSTLCのVar, Abs, AppそしてBool, Nat, Let関連でどう部分型に対応していくかを見ていく。 まずは変わらない部分から。 EVar, EAbs, ETrue, EFalse, ENat, ELetは変わらない： let rec typeof env = function | EVar var -> List.assoc var…

前回に続いて、エラー処理のある言語を型検査できる型システムを実装する話。今回は部分型全般やBottom型に対するチェックを行うヘルパ関数について。 導入するヘルパ関数は四つ： ある型がある型の部分型かどうかを調べるis_subtype 部分型関係を考慮に入れ…

以前Pythonのfor-loopでの変数スコープについてちょこっと書いた。 zehnpaard.hatenablog.com 最近Go言語でも似たような（？）問題があることを知ったので備忘録として残しておく。ちなみに私はGo言語は資料を少し読んだことはあるが書いたことはないので正…

前回書いたとおり、エラー式の型であるBottom型が部分型として正しく振る舞えるような変更を加えていく必要がある。 Bottom型に関して注意しておくべき最大のポイントは以下の二つ： Bottom型はすべての型の部分型である。ということはBottom型の式は他のど…

例外を投げるようなエラー処理のための型システムを追加していく。 今までの変更に比べて圧倒的に複雑なので複数回にわけている。 何が複雑かというと、「エラーが投げられた箇所の式の型は何か？」という問題の答えが「任意の型を取り得る」というものだか…

MLの一つの特徴として、デフォルトではほとんどの変数やデータ構造に破壊的代入が不可だが、破壊的代入が可能なデータ構造を明示的に選択することが可能、という非純粋な関数型プログラミング言語であることが挙げられる。そういった非純粋性を支える一つの…

再帰関数を定義できるようにするために不動点オペレータFixを追加する。型のないラムダ計算だと普通のラムダ抽象として定義できるのだが、STLCでは型をつけることができないので組み込みのオペレータとして用意する必要がある。 TaPLからの例を取ると： ff =…

型システムにバリアント型とケースに対するパターンマッチを追加する。 こういうやつ： type t = Name of string | Id of int let to_str = function Name s -> s | Id n -> string_of_int n 代数的データ型における直和型であり、前回の直積型と合わせると…

前回のLetまで実装した型システムにレコードを追加する。 gist.github.com レコードというのは{x=1; y=true}のような値にラベルのついたデータ構造。ちなみにタプルは型システム的にはレコードの亜種と考えていい（ラベルが0~の整数だと見做せる）。どちらも…

前回のコードにLetによる変数束縛を追加する。 gist.github.com コードの追加としては2行のみと非常に短い。 型 変更なし 式 追加するのはLetだけ： type exp = ... | ELet of string * exp * exp ELet(変数、変数を束縛する式、本体の式）という構成になっ…

前回のSTLC+Boolに自然数と関連する機能を追加していく。 gist.github.com 型 TNatという自然数を表す型を追加： type ty = ... | TNat 式 三種類の式を追加： type exp = ... | ENat of int | EAdd of exp * exp | EIsZero of exp 自然数リテラルを表すENat…

前回のSTLCにBool型と関連する式を追加してみる： gist.github.com まずは型にTBoolを追加： type ty = ... | TBool 式にTrue, FalseとIf式を追加： type exp = ... | ETrue | EFalse | EIf of exp * exp * exp If式はcondition式、if-true-branch式、if-fal…

前回Simple Boolからはじめると書いたのだが、よく考えると単純型付きラムダ計算（STLC）ではじめるのが当然な筋な気がしてきた。 ので急遽Simple BoolからBoolを取っ払ってSTLCだけをまずみてみる： gist.github.com 定義されるものとしては 「型」を表す型…

最近は言語処理系に関してまったく手を動かしていなかった＆ブログに何も書いていなかったので練習がてら・・・ Types and Programming Languagesには非常にたくさんの型システムの実例と関連したOCamlコードが載っている。ただし多くは写経したらそのまま実…

「関数型プログラミングが主流になりつつある」という話が（またしても）ツイッターで出ていた。LINQやらReactやらを引き合いに出した英語記事が議論の引き金のようだ。その話題の一部として「そもそも何をもって関数型プログラミングと呼んでいるのだ？」と…

前回に続きJOSSについて。今回は「オブジェクト指向」の名付け親、Smalltalkの設計者などで知られるアラン・ケイがJOSSに影響を受けたらしい、という話。 ACMインタビュー 私がJOSSという言語を意識し出したのはアラン・ケイの2004年のACMインタビューを読ん…

JOSSという言語とプログラミング環境があった、らしい。 en.wikipedia.org 初出は1963年、LISPの5年後でBASICの1年前である。RANDコーポレーションのJOHNNIACマシンを数学者が対話的に扱うための言語とシステムで、開発者はCliff Shaw。以前ブログで取り上げ…

気づいたらブログを更新しないまま6月が過ぎてしまった。 記事を書く上での自分の中の期待値とコストが増大していき、下書きで数千文字書いた時点で終わりが見えなくなってしまって放置する。そういうケースが３〜４本出てくると徒労感が募って手が出なくな…

逆説的でキャッチーなフレーズ「Worse is Better」の原点であるRichard GabrielのThe Rise of "Worse is Better"を再読したのでメモ。 概要 The Rise of "Worse is Better"は1989年にRichard Gabrielが書いた「Lisp: Good News, Bad News, How to Win Big」…

こういうツイートがあった Python君さぁ… pic.twitter.com/HDdQrSO8yp— not (@not_522) May 25, 2022 「まあ大体IEEE 754のせい」でほぼ終わる話ではあるのだけど、少し深掘りもしたのでちょびっと備忘録メモ。 問題を（少し順番を変えた上で）再掲すると： …

ツイッターでPythonの文法の話題が盛ん（三角関数と同じで周期的に話題になる）で、個人的にはあまり同意できない意見も多いのだがなかなか面白いトピックもある。 例えば以下のようなコード： fs = [] for i in range(5): fs.append(lambda: i) for f in fs…

ここ数年インターネットを徘徊していて見つけた「傑作論文集」をブックマークして部分的につまみ食いしたりしてきた。 自分用の備忘録として＆他の人にも有用かもしれない、ということで記事にしておく。 計算機科学全般 書籍だが、MIT出版の出しているIdeas…

John Backusという計算機科学者には大きな功績が三つある： IBMでFORTRANの開発を提案・主導したこと 構文の形式的な定義を可能とするBackus-Naur FormをALGOLの開発のために提案したこと チューリング賞受賞講演で、FORTRANのような命令型プログラミングか…

（注：あの頃というのは私が多感だった2000年代のことである） 最近マイクロソフトのRaymond Chenの「マイクロソフト社員がIBMに出向していた時に文化の違いに辟易してコーヒーメーカーに関して小さな反抗をした」というものブログ記事を見た。 devblogs.mic…

プログラミング言語理論の最初期の金字塔の一つ、The Next 700 Programming Languagesを読み直したので論文メモ。これは過去に何回か読み直している個人的にも非常に思い入れのある論文。論文メモ書きたいなとここ数ヶ月ずっと思っていた。 背景 The Next 70…

かなり前に、DijkstraとWirthがAPLの話をIversonから聞いて「俺たちの目が黒いうちはこんな言語は絶対流行らせない」と言ったという話をどこかで読んだ気がしていてソースを探していたのだけど、なかなか見つからずに残念に思っていた。 DijkstraがAPLのこと…

Graydon Hoareが2019年にカナダのブリティッシュ・コロンビア大学でコンパイラ関連のゲスト講義した時の資料21 compilers and 3 orders of magnitude in 60 minutes - a wander through a weird landscape to the heart of compilationを読んだら大変面白か…