時々ツイッターで俎上に上がる言説として「プログラミング言語は一つ学んだら大体全部同じ」という話と「お前HaskellやLisp見ても同じことが言えるの？」、そして「いやHaskellやLispだってそこまで違うわけじゃない」という一連の流れがある。 これで思い出…
Graham HuttonのHaskellを使ったプログラミング言語意味論のチュートリアル論文Programming Language Semantics - It's Easy as 1,2,3を読んだのでメモ。 HuttonはOCamlでMonadic Parserを作ってみる（前編） - Arantium Maestumの元ネタである「Programming…
ポール・グレハムの記事の一つにWhat Makes Lisp Different?というものがある： www.paulgraham.com ポール・グレハムらしくよく書かれていて、C言語などと比較した場合のLispの特徴をうまく捉えているように思う。 その中の一つが Recursion. Recursion exi…
John McCarthyの1960年に発表された論文Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part Iのメモ。 背景 「Artificial Intelligence」という用語の名付け親であるMcCarthyが、自身が助手らと作ったLISP言語を世に出し…
前回の記事でも紹介したOlin ShiversのT Programming Languageに関する回顧録で It had a big influence on Andrew Appel, at Princeton, who subsequently adopted a lot of the ideas in it when he and Dave MacQueen's group at Bell Labs built the SML…
CPS形式のコンパイラIRについて調べていてORBITというコンパイラについての話が出てきたので、1986年に出た論文ORBIT: An Optimizing Compiler for Schemeを読んでみた。 ORBITはGuy SteeleのRABBITというScheme Compilerから「CPS形式をIRとして使う」とい…
前回はSubstitution関連で少し寄り道したが、今回こそはPrincipal Type Schemes for Functional Programsの中核である type inference Robinson's unification algorithm algorithm W の話。 type inference For assumptions A, expressions e and type-sche…
前回「type inference、Robinson's unification, algorithm Wを見ていく」と書いたが、その前にsubstitutionについてつらつらと考えてみたい。 S is a substitution of types for type variables, often written [τ_1/α_1,...,τ_n/α_n] or [τ_i/α_i] とある…
Abstract machines for programming language implementationを読んだのでメモ。 どのようなAbstract Machineがどのようなプログラミング言語の実装に使われてきたのか、というサーベイ。2000年に書かれており筆頭著者はHaskell界隈ではそれなりに知られてい…
型推論のためのAlgorithm Wを実装するため、DamasとMilnerのPrincipal Type Schemes for Functional Programsを読んでいる。 重要そうな概念としては expression type/type-scheme substitution instance/generic instance assumption assertion closure typ…
少し前にTwitterで「面接で『なんで1byteって8bitsになっているのか？』と聞くといい」というツイートが話題になっていた。 それを見た時は「まあ8bitsだとは限らないよね、現在主流のアーキテクチャがそうなってるだけで」と思っただけで終わったのだが。 …
A正規化について非常に参考にさせてもらっているMatt Mightのブログ記事で A later transformation to continuation-passing style (like that in Appel's book) is also simplified if transforming from A-Normal Form. とあるので、これまでのA正規化され…
最近@karino2さんのポッドキャスト「プログラム雑談」のバックナンバーをいろいろ聴いている： anchor.fm 二週間ほど前に書いた聴いてるポッドキャストの記事ではまだ「気になっている」という分類だったのだけど、聴き始めたらいい感じにゆるいのと技術的な…
前回のCEK抽象機械を拡張して、ミュータブルな状態のある言語も自然に実行できるようにする。 CESK抽象機械 CEK抽象機械はControl（実行する式）、Environment（変数環境）、Kontinuation（継続）の三つの要素を持つ。 CESK抽象機械はそこにStore（格納）を…
前回で定義した言語とそのA正規化されたIRをインタプリタで実行したい。 というわけでまたしてもMatt Mightのブログを参考にする： matt.might.net こちらのブログはCESKマシンの話だが、今のところ破壊的変更を言語機能として実装してないので、まずはCESK…
前回の言語に関数定義・適用を追加する。 単一引数の関数 まずは変更を簡単にするために「単一引数の関数」を実装する。 関数自体の式であるFnと関数適用のCallをASTに追加： type t = ... | Fn of string * t | Call of t * t α変換は関数式に関しては（仮…
前回に続いてA正規化の話。前回のミニマルな言語にブール型とifによる条件分岐を加える。実は条件分岐の正しいA正規化に関しては曖昧性があるようなので、後半はその話。 言語拡張 ASTに以下を追加： type t = ... | Bool of bool ... | Lt of t * t ... | I…
言語処理系の実装の手法として「A正規化」というものがある。 元のソースプログラムを変換して最適化や機械語へのコンパイルなどがやりやすい形にする、処理系IRの選択肢一つである。CPS（継続渡しスタイル）のIRと非常に似ている。 The Essence of Compilin…
去年何回か別々のところでAeropex Aftershokzという骨伝導ヘッドセットを勧める話が出ていた： honeshabri.hatenablog.com I have a decision! Thanks to recos from @teohmato @theinedibleholk @tranchedeviee @bviswana I got the Aeropex Aftershokz (bo…
mliとは？ OCamlのプログラムは基本的にいくつものモジュールに分割されて書かれる。そして「あるファイルに記述されたOCamlコード」は独立した一つのモジュールとなる（中に複数のサブモジュールが定義されていることはあり得る）。 ただし、Cの.hと.cファ…
プログラミング言語理論に関係する論文を結構読み散らかしているのだが、あまりしっかりアウトプットする機会もないので読み込みも甘いし記憶も曖昧になる。 というわけで面白そうなやつは、内容・背景・感想などをブログにメモとして残していこうと考えた。…
現代のプログラミング言語で「整数を掛け合わせる」という処理を書く場合、掛け算を意味する記号としてはアステリスク*を使う場合がほとんどである。例えば比較的最近の言語で整数の割り算には÷が使えるJuliaでも、掛け算は*で統一されている。 Wikipediaのm…
前回の記事で これを書いていて「あれ、多相って関数だけじゃなくて型に対しても使う？型コンストラクタってそれ自体が多相？」とふと疑問を抱いた。この点に関しても別の記事で書きたいが、現在の自分のスタンスとしては、特殊な例を除いて「パラメトリック…
前回に続いてカインドについてのメモ。 TaPLとともに、"Functional Programming with Overloading and Higher-Order Polymorphism"という資料をかなり参考にしている。 高カインド型 高カインド型（Higher Kinded Types）については以下のStack Overflowの返…
Types and Programming Languagesの最後のほうに「カインド」という概念が出てくる。 System Fをさらに拡張したSystem Fωという型システムが存在していて、その「拡張の方向」がカインドだということらしい。（ちなみにSystem FωはF-ing Modules論文のベース…
個人的に作りたい自作言語の構想というのは結構昔からあって、ありていに言ってしまえば「Pythonチックなインデントベースでスッキリした構文でモジュールまで含めたMLの意味論を持つ言語」となる。 ただしMLのような式ベースの言語が破綻しない構文というの…
先日こういうツイートがあった： Haskellとかの関数型言語を使用しているプログラマの皆様にお聞きしたいんですけど、「関数名 引数 引数 ...」みたいな関数呼び出し構文って見にくくは無いですか？「関数名(引数, 引数, ...)」に慣れたこちらからすると、丸…
自作言語熱が高まっていて、バックエンドをLLVMでやりたいと思っている。 OCamlでLLVMというとLLVMプロジェクト公式のKaleidoscope言語をOCamlで実装するチュートリアルが有名、なのだが、10年近く前に壊れたAPIを使っていたりと実際に使えるものではなく、…
最近なかなかブログを更新できずにいて、気持ちとしては しかしブログは「シリーズ物の記事」と考えて書こうとすると、シリーズ最後あたりは本当に書くのがつらくなるな— zehnpaard (@zehnpaard) February 21, 2022 で少し自分の首を絞めている感覚がある。 …
前々回、前回に続いて500行以上の本格的なMenhirパーサの例。 C11パーサ A simple, possibly correct LR parser for C11という論文のもとになった、Menhirを使ってなるべく正確な（過去のC11基準コンパイラがパースに失敗するプログラムもパースできる）C11…
