Jul 2, 2022 Millet, a language server for Standard ML (SML), is now available. Check it out on: GitHub VS Code marketplace Open VSX In this post, I will: Introduce some of the main features of the project. Note some caveats and potential areas of improvement. Talk a bit about its development. Close with some thanks. Features: an overview Basic The extension provides syntax highlighting, as well as

本書では関数型言語をはじめとして多くの言語にあるパターンマッチをコンパイルする方法を紹介します。パターンマッチはシンプルに条件分岐の連鎖にコンパイルすることもできますが、よく研究された手法を使えば驚くほど効率的なコードを生成できるようになります。そのような手法を2種類紹介します。 パターンマッチはデータ型に照合しそのデータを取り出すものです。例えばRustであれば match opt { Some(x) => f(x), None => g()} のように Option 型への照合などに使えます。本書の前半ではパターンマッチの挙動や使い方などを学びます。挙動の確認にはプログラミング言語Standard MLを使い、一部Cのコードも使います。その後Common LispやJavaなどの他の言語でのパターンマッチの状況を確認します。後半ではパターンマッチのコンパイル技法について紹介します。パタ

Isabelleをいじっているあいだ（＝飽きるまで ^^;）は、ダイアリーにIsabelleの話が入るでしょう。今日は小ネタ。 「ハイコンテキストな定数・記号の解釈」とかで話題にしたmin-plus半環をIsabelleで書いてみました。あの記事では、通常の演算子記号「+」「*」をオーバーロードする話でしたが、今回はエキゾチックな演算子記号「」「」を使います -- 「零の概念とmax-plus半環の紹介」の説明と同じ記号法になります。 とりあえず書いてみたのは：[追記]コメント内の to proof は to prove ですね。テキストならすぐ修正するけど、画像だから面倒だ、直さない。[/追記] セオリー記述をお見せするのにスクリーンショット貼り付けるのが、もうナントモ複雑な気分ですが、生のソースコード・テキストじゃ読むの辛いし。（一応、最後にテキストも貼っておきます。） min-plu

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？

Poly/MLはREPLとしてもコンパイラとしても使うことのできるSML処理系です。 64bit環境に対応した処理系でもあるので、そういった意味でお手軽な場合も多そうですね。 ここではPolyMLのREPLでコードを読み込む方法を紹介します。 use とりあえず use は備えています。指定したファイルの内容を直接replに入力したように動きます。 > val use; val it = fn : use : string -> unit > use "Sample1.sml"; structure Sample1 : sig val f : unit -> unit end val it = (): unit > PolyML.make 本題。必要なデータ/ファイルだけを(再)読み込みする機能。 SML/NJのCM*1(の一分)に相当する機能がREPLに組み込まれています。 単一ファイル

このエントリはML Advent Calendar 2015及び言語実装 Advent Calendar 201515日目の記事です。 κeenです。先日流れてきたRustでJITコンパイラを作る話が面白かったのでSML#でもやってみます。 JITコンパイラってなに？ JITはJust In Timeで、日本語にすると「間に合って」になります。誤読されかねませんが「臨時コンパイラ」と訳すのが適当なのでしょうか。 普通のインタプリタがソースコードを直接評価するのに対してJITコンパイラはソースコードを内部で一旦ネイティブコードにコンパイルして実行します。 よく、JITコンパイラ/JITコンパイルのことをJITと略して呼びます。 どこで使うの？ 主に、インタプリタの高速化の目的で使われるようです。他にはコンパイラをインタプリタ化させる(REPLの実装とか)でも使えそうな気がしますが、詳しくは知

現在僕は趣味でStandard MLのサブセットの処理系を実装しようとしているのですが、皆さんのご存知の通り、Standard MLの構文解析は非常に難しい事が知られています。 今回はML Kitの実装に関する文書を参考に構文解析器を実装した時の事について書きたいと思います。 ちなみに、タイトルもその文書からの引用です。 何が難しいのか 言語仕様のpp.4-10を読むと分かる通り、アルファベットその他の列では終わらずにいくつかの記号（+、-など）のみからなる文字列も変数名に使う事もできます。 加えてどの変数も二項演算子にできるわけですから、明らかに字句解析の段階ではどの変数が二項演算子なのか判別ができません。 さらに、どの変数が二項演算子なのかはもちろん、演算子の優先順位や結合性もプログラマーが自由に決められます。それもスコープに依存して。 また、二項演算子として定義した変数の前に"op"

普段日常生活を営んでいると何となくコンパイラを作りたくなる事はありませんか？僕はあります。 演算子順位構文解析を用いることでStandard MLで行なわれているような演算子の順序の入れ替えを実現できるのではないかと思い、試しに実装してみました。 Standard MLの文法は演算子の優先順位をプログラマが指定できる事から、非常に構文解析が難しい事が知られています。 ある日何気なくTLを眺めているとMLKitの実装に関する論文が流れてきたんですが、その論文によると中置演算子の含まれた式の構文解析を後回しにし、2ステップで構文解析をするそうです。 括弧等の高レベルな文法はyaccなどで実装される第一のステップの構文解析器で処理される訳ですから、第二のステップで処理しなければならない文法は変数等と中置演算子からなる演算子順位文法であると考えられます。 また、構文解析の対象の言語は演算子順位文法

κeenです。かねてより気になっていた幽霊型(Phantom Type)について知ったのでアウトプット。 このPDFがベースになって ます。 余談ですが英語がファントム・タイプと中々中二な名前なので和訳も幻影型とかそういう方向に走って欲かったな。 「幽霊型」で調べると真っ先にこのサイトが出てくるのですが、ミスリーディングと言われていました。 別に間違ったことを書いている訳ではないのですが、幽霊型の応用例なのでこれこそが幽霊型だと思ってしまうと少し視野が狭くなってしまうようです。 モチベーション ブーリアンと整数と条件分岐と足し算と比較が出来るミニ言語を考えてみます。自動で型変換は行わない(つまりintとboolの比較などは出来ない)言語とします。こんな感じでしょうか。 datatype exp = Int of int | Bool of bool | If of exp * exp *