Japan ATS User Group (JATS-UG)の発足とAjhcの今後について

Table of contents

• Japan ATS User Group (JATS-UG) について
• なんでいきなりユーザーグループ？
• 一通のメール

この記事は Theorem Prover Advent Calendar 2013 - Qiita [キータ] の12/24(火曜)分じゃなイカ。

Japan ATS User Group (JATS-UG) について

突然でゲソが、ATS言語に関しての日本語情報を集約する組織である、 “Japan ATS User Group” 略して “JATS-UG” ¹ を発足することをここに宣言するでゲソ! このユーザグループのホームページは http://jats-ug.metasepi.org/ でゲソ。

現在このページではATS言語の概要説明と 翻訳ドキュメント置き場 へのリンクぐらいしかないでゲソ。 とりあえず年内はドキュメント翻訳に力を入れたいと思っているでゲソ。

なんでいきなりユーザーグループ？

最近ワシがATSを調べているのには理由があるのでゲソ。 現在我々がいるイテレーションは Arafura でゲソ。 このArafuraイテレーションで採用しているデザインは

「NetBSD kernelをAjhc Haskellコンパイラを用いてスナッチ設計する」

だったでゲソ。 NetBSD kernelのデバイスドライバをAjhcでスナッチする環境がととのった今、 次のイテレーションの計画をオーバーラップして行なうべきでゲソ。 技術探索は賭け事と似ていて分散投資した方が成功率が上がるため、 イテレーションは短かくまわした方が効果的じゃなイカ？ 本当はまっとうなKPTなどをした方がいいでゲソが、現状の問題点は明らかでゲソ。

それはAjhcの開発に工数を取られすぎているという問題でゲソ。 Haskellを組み込み応用するということ自体が既に挑戦であり、 その挑戦がある程度成功しないと製品化のスタート地点に立てないのでゲソ。 しかもこのAjhcの開発にアップストリームであるJohnはほとんど工数を払えていないでゲソ。 さらにAjhcには組み込み応用するための技術的課題が山積しているじゃなイカ。 つまりProblemでゲソ。

一方、スナッチ設計という手法については比較的うまくいっているでゲソ。 NetBSD kernelに適用した結果はこのイテレーションでも完全に判明することはないでゲソが、 今のところ根本的欠陥は見つかっていないでゲソ。 NetBSD kernelの採用についてはまだなにもわからないでゲソが、 おそらく最初のイテレーションではどんなkernelを使っても似たようなもんだと思うでゲソ。 つまり、この2つは明らかにKeepじゃなイカ？

じゃあTryはなんでゲソ？ 昨日の記事 に書いたでゲソがATSはjhcと似たような特性を持っていて、 組み込み開発に適用することができそうでゲソ。 ところがこのATS、日本語の情報がまったくなく、さらには日本にはコミュニティさえないようだったでゲソ。。。 埋もれておくにはもったいないコンパイラなのにでゲソ! これはマズイじゃないか。 そこで、ワシがATSを勉強するついでに各種文書を翻訳して日本にATSコミュニティを築こうと思うのでゲソ。 これが次のイテレーションを開始するために必要な最初のTryでゲソ。

一通のメール

そこーしているとATSの作者からメールが届いたじゃなイカ。 なになに？でゲソ。

Date: Mon Dec 23 11:40 JST 2013

Hi Metasepi-chan,

I spent quite some time today browsing metasepi.org.

I am really interested in your Metasepi project, partly because I myself
wanted to implement NetBSD in ATS about 5 years ago. Unfortunately, I
never had time to get the project started as I needed to spend so much time
on ATS2. By the way, I had planned to use the very same approach which you
call "Snatch". I had also considered Minix but I chose NetBSD because
it was a real OS.

I think I know first-handedly the dilemma you are currently in.
On one hand, you want to be able to fully focus on writing the kernel.
On the other hand, you also need to add features to Ajhc constantly
to address all kinds of issues that keep popping up, which undoubtedly
makes it very difficult for you to focus.

I would highly recommend that you use ATS to implement NetBSD kernel.
Unlike jhc, there is no semantics gap between ATS and C. In
particular, they both use the same native unboxed data representation.
Once you become familiar with ATS, you can readily visualize the C code
that your ATS source is to be compiled into. ATS is truly an ideal
language for the kind of "Snatch" approach you want to take to re-write
NetBSD. If you take the lead, then I will be happy to "chip in" :)

I also spent some time reading documentation on jhc. Personally, I
feel that there is simply too much uncertainty to use it in real kernel
implementation. Features like GC could make the kernel highly unpredictable,
scaring away potential users.

I think that we both believe C is the right language for systems
programming. The problem with C is that it is too difficult to write
correct C programs. ATS is designed to allow the programmer to
correctly write the kind of C programs he or she wanted to write in the
first place. While jhc generates C code, the kind of C code it generates
may not be suited for kernel. This is what I call a semantics gap.

I write this message in the hope that we could join effort in doing
something that has not been done up to now: Writing a real kernel in
(largely) functional style that can truly deliever safety-wise as well as
performance-wise.

Cheers,

--Hongwei

なんかワシが言いたいことを全部先取りされてしまったでゲソ。 これも中国四千年の重みという奴かもしれないじゃなイカ。

しかし、それでもjhcの先に未来がないということにはならないでゲソ。 ATSの型表現は安全ではあっても、Haskellのように豊かではないでゲソ。 決定的なのは型クラスの不在でゲソ。 Haskellの上でくりひろげられている非常に高階なプログラミングは、 ATSを使っても実現できるとは思えないでゲソ。 つまり、高階な記述を使ったアプリケーションにはATSはおそらく向いていないということじゃなイカ。 Haskellの問題点は、その高階な表現を完全にGHCの実装に依存してしまっていることでゲソ。 GHCが組み込みドメインで使えるようになる見込みはほぼゼロでゲソ。 じゃぁjhcはどーなのカ？ というと今度はGHCの豊かな表現力の多くが通用しないのでゲソ。 つまりjhcはATSのような記述をプログラマに強いるHaskell実装に現状なってしまっているのでゲソ。 もしjhcの持つこの問題をいくばくかでも軽減できれば、Haskellの応用範囲は劇的に広がることになるはずじゃなイカ。 問題は、誰がその膨大な工数を払うことができるのか、ということでゲソ。 Johnのような天才でさえ擦り切れてしまう、このあまりにも挑戦的な課題に誰が立ち向かうことができるのか。 言い方をかえれば、誰がJohnの心をささえることができるのか。 それがHaskellの組み込み応用という分野に高くそびえたつ冷たい壁なんじゃなイカ？

でもこれも前進に他ならないのでゲソ。 のぼった日は沈み、 そして願わくばまた日の出の時刻に光が見えることを信じて。 メリークリスマス! でゲソ。