Kickoff Japan ATS User Group (JATS-UG) and Ajhc's future plan

Table of contents

• What is Japan ATS User Group (JATS-UG)?
• Why need the user group?
• An E-mail

This article is a part of Theorem Prover Advent Calendar 2013 - Qiita [キータ].

What is Japan ATS User Group (JATS-UG)?

We declare to build “Japan ATS User Group (JATS-UG)”, to pool and discuss ATS infomation in Japanese! The web site is found at http://jats-ug.metasepi.org/.

Today, the web page only has the summary of ATS language and the link to translated documents. We will focus translating ATS documents into Japanese, through the end of this year.

Why need the user group?

I have a motive to research around ATS language recently. We are in Arafura as the first iteration. The Arafura design is:

“Rewrite NetBSD kernel using Ajhc Haskell compiler, with Snatch-driven development stype.”

The next iteration should be planned in parallel, because we have the method to rewrite NetBSD kernel device drivers using Ajhc now. Research is similar to betting that has good result using diversified investment. Arafura iteration’s problem is clear without any KPT (keep, problem, try) framework.

It’s caused by much time to develop Ajhc. Haskell for embedded is a big challenge in itself. We need the challenge’s success to attain the starting post to write kernel. Furthermore, John as upstream author of jhc doesn’t develop jhc actively. There is many technical puzzles on ATS domain. It’s the “Problem”.

On the other hand, Snatch-driven development method is relatively doing good. Result fully-applying the method to NetBSD kernel will not be obtained in the first iteration. However, We have found no underlying faults. And we can’t perfectly decide that using NetBSD kernel as base platform is good. We think it causes same result while the other monolithic kernel is used. That is to say that these are clearly “Keep”.

What is “Try”? I wrote the article, about ATS language has good behavior for embedded such like jhc. However, there are no Japanese infomation about ATS, and no communities about ATS in Japan… Things can’t remain as they are. Then, I would like to construct an ATS community in Japan, while I learn ATS language. It’s first “Try” to start our next iteration.

An E-mail

While thinking such things, I got an E-mail from ATS language author.

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

Umm… What I want to say is preoccupied by him. This may be caused by weight of long china history.

Jhc Haskell compiler also has a good future. ATS’s type is safe, but not rich such like Haskell’s. Haskell has type class. I think that ATS can’t write code that has higher order representation such like Haskell. That is to say, ATS may not be good to write application that use the representation. Haskell’s issue is that the representation strongly depends on GHC language implementation. There is no future on GHC growing to be good for system programming. On the other hand, how about jhc? No, it’s good for system programming, but can’t use most of the representation. So, jhc is currently Haskell implementation that imposes writing a code such like ATS’s on programmer. If the issue is relieved, we can dramatically expand Haskell language’s application range. Problem is who can pay huge man-hours to be needed for research/design/develop/debug them. While even genius such as John gets tired, who can try to solve the challenging problem? In another way, who can support John’s mind? That is, the high-solid wall on Haskell for embedded.

However, this should be a positive step. While seeing the sunset, I belive having new sunlight tomorrow. And, Merry Christmas! De-gesso.