これ、読んでます

ATSプログラミング入門

入門する前に知りたかった情報として、今は ATS2 と呼ばれるバージョンになり、コンパイラは atsccではなく patscc になっているそうです。入門しながらこの記事を見ると落とし穴(インクルードやリンカエラー)にはまらずにすみます。

ATS の所感、C言語を生成する感じは初期のC++と思想として同じですが、型推論が微妙なのもありテンプレートが随分と使いにくい...？それと別にMLっぽい多相関数があるのも変な感じがしています。F#とかScalaみたいに関数型以外のパラダイムな部分で型推論や部分適用が効かないのと同じ理由でしょうか。うーん、Rustなどは一体どうやっているんでしょうか？

それにしてもC言語が直接かけるのは実に強力で、なんとOpenCLのコードも動きました。とりあえず、この言語の一番おもしろそうな証明の部分までじわじわ進めたいです。そのために少し前まで Coq を触ってたのです。

Emacs の設定

png_img

ats2-mode.el と flycheck-ats.el を導入すると超読みにくいエラーメッセージ(下ペイン)がエディタ上でハイライト(上バッファ)されて少なくとも発生場所は明確になって嬉しいです。

(setenv "PATSHOME" "/path/to/ats/ATS2-Postiats-x.y.z")

;; wget -O load-path/ats-mode.el https://raw.githubusercontent.com/mrd/ats2-mode/master/ats2-mode.el
(require 'ats-mode)
;; wget -O load-path/ats-flycheck.el https://raw.githubusercontent.com/drvink/flycheck-ats2/master/flycheck-ats2.el
(require 'ats2-flycheck)


(setq auto-mode-alist
      (append '(("\\.dats$" . ats-mode))
              auto-mode-alist))

(add-hook 'ats-mode-hook
          '(lambda ()
             (require 'smart-compile)
             (setq smart-compile-alist
                   (append smart-compile-alist
                           '(("\\.dats$" .
                              "patscc %f -o %n -DATS_MEMALLOC_LIBC && ./%n"))))
             (with-eval-after-load 'flycheck
               (flycheck-ats2-setup))
             (require 'flycheck)
             (flycheck-mode)))

どっちの拡張もファイル名と provide されるモード名が違うせいか怒られたので一致させて、ats2-mode.el の方は smart-compile で邪魔なので compile-command を指定する箇所を消しました。やはり REPL 的に試せる環境があれば言語習得が早くなりますね。