しらそら2

誰だお前は: https://silasol.la/identity/mixi2/silasolla/signed

フォローしてmixi2をはじめる

Misc

にょわくじ2026

2025 年の振り返り - 芳賀雅樹のページ

不動点コンビネータと実践的な示唆について紹介します．

不動点コンビネータと無名再帰 - 芳賀雅樹のページ

Cloud Spanner のコアアーキテクチャについて，職場の Tech Blog 補足と技術的な余談 (Paxos, CAP 定理, NewSQL) をまとめました．

Cloud Spanner の記事を書きました (+ 技術的な蛇足) - 芳賀雅樹のページ

ショートショート書いてみた．

小箱 - 芳賀雅樹のページ

# セッションのテーマ

- 言語
- 理論
- 実践手法

# 想定する聴衆/前提知識

- 安全な型の抽象化やモジュール境界の設計に関心がある方
- 言語の機能の設計意図や仕様と実装の境界に関心がある方
- 仕様を厳密に記述することの工学的な価値に興味のある方
- TypeScript, Rust などの型付き言語，あるいは関数型プログラミングの基礎経験がある方 (SML 自体の経験や事前知識は不要です)

# 聴衆が得られるもの

Standard ML (SML) の形式的仕様に触れながら，仕様と実装を分離する視点や，型の抽象化やモジュール境界をどこまで仕様で規定できるかといった，ソフトウェア設計の判断軸を持ち帰ることができます．

# セッションの概要

型付き言語が普及した現在も，不変条件やモジュール境界が実装に依存してしまう課題は尽きません．今こそ，その源流に立ち返る時です．

30 年ほど前に書かれた "The Definition of Standard ML (Revised)" は，プログラミング言語の仕様を自然言語の散文ではなく，形式的な推論規則で定義した稀有な文献です．

今回の発表では，この形式的な仕様の定義を単なる学術的な読み物ではなく，モジュール境界の設計や依存関係の解決といった，現代のエンジニアが日々直面する課題に対する実践的なヒントとして読み解きます．

具体的には，現代にも通じる 4 つのトピックに触れます．

- 静的意味論 (精緻化) / 動的意味論 (評価) の分離と，型情報に依存しない動的意味論
- 不透明シグネチャによる生成的な型の抽象化と，仕様レベルで規定された型の非互換性
- 可変参照がある場合に型の健全性を守る生成的なファンクタと，型の依存解決を静的に完結するモジュール構成
- 多相性と可変参照の共存における値制約の設計や，理論と実用のトレードオフ

難解な数式の羅列は避けて，TypeScript や Rust などのコードとの対比や図解を交えながら，意図を直感的に把握できるような解説を目指します．

実装の手段ではなく「どう振る舞うべきか」を定めた抽象的な仕様が，何を保証し，何を保証しないのか，その境界を見極めて日々のソフトウェア設計にどう持ち込むかといった，SML に限らず応用できる工学的な視点を提供します．

2026 年に読む “The Definition of Standard ML” 〜現代の堅牢なソフトウェア設計の源流として

はじめに Sreake 事業部の芳賀雅樹 (@silasolla) です．普段はアプリケーションの開発支援を担

地球規模の「時間のずれ」を Cloud Spanner はどう解決したか | sreake.com | 株式会社スリーシェイク

Misc@silasolla | mixi2