東北大学電気通信研究所大堀・上野研究室

大堀・上野研究室では，当研究室の研究成果を応用し，高信頼プログラミング環境の中核となる新しいプログラミング言語SML#の研究開発や，その実用化に向けた産学連携研究を推進しています．

本ページでは，SML#の目標と概要を紹介します．

SML#プロジェクトに関する詳細はSML#プロジェクトのWebサイトを，当研究室の一般的な研究内容は大堀・上野研の研究内容を，それぞれご覧ください．

SML#の目標

SML#が目指す一般的な目標を一言で言うならば「Standard MLを実用的な言語にすること」です．

MLと呼ばれる言語は，1970年代にこの世に生まれてから今日までの間，研究者やコンパイラ開発者の間では，時に研究対象として，時に開発言語として，多くの人に愛され育まれてきました．MLを愛する人にとっては，MLの高い生産性，信頼性，安全性は，ごく当たり前のことです．

その一方で，産業的ソフトウェア開発の現場においては，MLは使用する言語の候補にすらなり得ていません．この原因は，単なる歴史的な先入観や教育上の問題ではありません．もしMLが誰にとっても本当に素晴らしい言語であるならば，今や誰もがこぞって学び使っているはずで，そのような問題は問題ですらないはずです．

SML#開発チームは，この原因を，MLを実用化するための技術的な課題の多くが未解決のまま残されているからである，と考えています．SML#開発チームが考える実用性とは，普通の言語で普通にできること，例えばC言語のプログラマがC言語で普通に行うように，OSやデータベースと直接連携し，既存の豊富なライブラリを駆使し，データは計算機アーキテクチャにとって自然なデータ表現でメモリ上に保存され，マルチコアCPU上でマルチコアが当然のように扱え，巨大なソフトウェアプロジェクトにも拡大可能な分割コンパイルとリンクを行うことです．

これらをMLの高階関数，多相性，モジュールなどの高度な言語機能と両立させ，高効率な実行系を構築することは，単なる実装努力だけで実現できることではなく，MLの原理に立ち返った基礎研究や，高度なコンパイラのための実装技術の開発を必要とします．これらの課題を解決し，膨大な研究成果に裏付けられたMLの高度な機能と，膨大な実用実績がある言語に匹敵する実用性を兼ね備えた，まさに次世代のプログラミング言語と呼ぶにふさわしいMLを実現することが，SML#プロジェクトの狙いです．

SML#の特徴

関数型言語

SML#は関数型言語と呼ばれるプログラミング言語です．手続き型言語は，計算機に対する命令列をプログラムとして記述します．一方，関数型言語は，計算対象をすべてプログラム内に宣言するスタイルで記述するため，従来の命令型言語よりも単純で可読性の高いコードを記述させることができ，生産性を向上させます．

$\begin{array}{l} \sum_{i = 0}^0 f(i) = f(0) \\ \sum_{i = 0}^n f(i) = \sum_{i = 0}^{n - 1} f(i) + f(n) \end{array}$

fun sigma f 0 = f 0
  | sigma f n = sigma f (n - 1) + f n

データベースやOSとの連携

いくら可読性が高くとも，研究の世界だけではなく，実際に動いている既存のソフトウェアシステムと相互に繋がらなければ，そのプログラムには価値がありません．関数型言語と，現実世界をシームレスに繋げるために，関係データベースやOSの記述言語であるC言語との直接連携の確立を目指しています．

レコード多相性[TOPLAS'95]

レコードの一部のフィールドのみにアクセスする関数にレコードカインドを持つ多相型を与えます．それによって，余分なフィールドをもつレコードを扱えるようになり，フィールドが不足する場合に型エラーが出るようになります．型主導コンパイルにより，効率的なコードを生成します．

# fun area rect = #width rect * #height rect;
val area = fn : ['a#{width: int, height: int} -> int]

# area {width = 3, height = 4};
val it = 12 : int

# area {x = 1, y = 2, width = 3, height = 4};
val it = 12 : int;

# area {x = 1, y = 2};
Type Error

Cとの直接連携[コンピュータソフトウェア'10]

SML#のデータがメモリ上でCと互換のデータ表現を持つように，コードを生成します．これにより，Cの関数をSML#のデータを引数に直接呼び出せます．

# val system = _import "system" : string -> int;
val system = fn : string -> int

# system "figlet -f lean 'SML#'";
                                                
      _/_/_/  _/      _/  _/          _/  _/    
   _/        _/_/  _/_/  _/        _/_/_/_/_/   
    _/_/    _/  _/  _/  _/          _/  _/      
       _/  _/      _/  _/        _/_/_/_/_/     
_/_/_/    _/      _/  _/_/_/_/    _/  _/        
                                                
                                                
val it = 0 : int

外部データの型理論[ICFP'11][ECOOP'16][ML'16]

自然結合を含むSQLやJSONを型システムのレベルでSML#にシームレスに組み込んでいます．これにより，型安全な外部データの取り扱いができます．

# open JSON;
...

# val [x, y] = _json (import "[3.14, \"SML#\"]") as void dyn list;
val x = _ : JSON.void JSON.dyn
val y = _ : JSON.void JSON.dyn

# _json x as real;
val it = 3.14 : real

# _json y as string;
val it = "SML#" : string

# _json x as int;
Runtime Type Error

数学的モデルに基づく安全性や記述性の確立

ラムダ計算や論理学，型理論等の数学的モデルを基礎として，ウェブアプリケーションや大規模計算がもつ，現実の問題に対する新しいプログラミングモデルや，プログラムの安全性を追求しています．

$\vdash \lambda x . e \Downarrow \mathit{Cls}(E, x, e)$

SML#の開発

SML#の目標

SML#の特徴

関数型言語

データベースやOSとの連携

最新のハードウェアで期待される性能の実現

レコード多相性[TOPLAS'95]

Cとの直接連携[コンピュータソフトウェア'10]

外部データの型理論[ICFP'11][ECOOP'16][ML'16]

数学的モデルに基づく安全性や記述性の確立

最新の実用研究

SML＃を用いた宣言的並列グラフ処理

株式会社日立ソリューションズ東日本様との産学連携:安全なWebアプリフレームワーク開発

NECソリューションイノベータ株式会社様との産学連携:実用的なERPシステムの開発

サイトメニュー

SML#の開発

SML#の目標

SML#の特徴

関数型言語

データベースやOSとの連携

最新のハードウェアで期待される性能の実現

レコード多相性[TOPLAS'95]

Cとの直接連携[コンピュータソフトウェア'10]

外部データの型理論[ICFP'11][ECOOP'16][ML'16]

数学的モデルに基づく安全性や記述性の確立

最新の実用研究

SML＃を用いた宣言的並列グラフ処理

株式会社日立ソリューションズ東日本 様との産学連携:安全なWebアプリフレームワーク開発

NECソリューションイノベータ株式会社 様との産学連携:実用的なERPシステムの開発

サイトメニュー

株式会社日立ソリューションズ東日本様との産学連携:安全なWebアプリフレームワーク開発

NECソリューションイノベータ株式会社様との産学連携:実用的なERPシステムの開発