Erlang VM上で動く言語

8年の開発期間を経て，Erlang 仮想マシン(BEAM)上でLisp言語をサポートするLisp Flavoured Erlang(LFE)がバージョン1.0の安定版に到達した。開発者のRobert Virding氏は，Erlangの初期開発者のひとりでもある。

LFEはLisp-2，すなわちCommon Lispタイプの，Erlang コンパイラのフロントエンドだ。マクロベースのメタプログラミングを可能にし，再帰と高階関数の利用をサポートする。また，Erlangの哲学を継承することにより，メッセージパッシングアクタモデルを採用し，“シェア・ナッシング”パラダイムをプログラマに求めるとともに，完全なパターンマッチングも提供している。Erlangと100%の互換性を持つコードを生成するLFEは，Open Telecom Platform (OTP)を使用した標準的なErlangおよびアプリケーションとのシームレスな共存も可能である。OTPは，高可用性，コンカレント，スケーラブルなアーキテクチャを備えた開発を可能にすることを目的に，Erlangで記述されたミドルウェアとライブラリのコレクションである。

qiita.com

「Erlangの文法は大嫌いだけどErlang VMの機能は慣れてるLispで使いたい」という強い要望と意思を持った人でないと使っていけないかな…と思いました。

Lisp ハッカーはスゴイな！（＝どこにでも進出して、自分達の色で染めていくｗ）

Java VM上で動くClojureを使ってた人なら、Erlang VM上で動くLFEでもOKでしょう。

OCaml風のAlpaca

「Lispがアリなら、OCamlやHaskellもアリでしょｗ」と思ったら、本当にありやがりました！

Erlang VM上で動く静的型システムを備えたOCaml風関数型言語の処理系があるらしいことを知った。アルパカ言語というらしい。これすごいんちゃうか。#alpaca_lang #erlang #ocaml #type #アルパカ https://t.co/KSHatd9sBe
— Yoshihiro503 (@yoshihiro503) May 11, 2017

「Alpaca」と命名されたML風の言語が、Erlang VM上で動くそうです。

github.com

Alpaca is a statically typed, strict/eagerly evaluated, functional programming language for the Erlang virtual machine (BEAM).

At present it relies on type inference but does provide a way to add type specifications to top-level function and value bindings. It was formerly known as ML-flavoured Erlang (MLFE).

（参考）

qiita.com

仕組みとしてはalpaca-langというErlangVM上で動作するML風Erlangを参考にしました。

Coq風なVerlang

Coqは「定理証明支援システム」で、プログラムの動作を検証するためにも使える仕組みです。

「OCamlが行けるなら、Coqも行けるのでは？」と思ったらありました。

qiita.com

Coq には Extraction という、Coq のコードを別の言語に変換する機能があり、この機能によってコードを検証済みの部品として実際のプログラムに使えるようになっています。標準では OCaml, Haskell, Scheme への変換が可能になっています。

この記事では、Verlang という、Coq の Extraction 対象に Erlang のコア言語である Core Erlang を加えるパッチ (つまり Coq2Erlang 的なもの) について紹介したいと思います。

github.com

（参考）Coqとは？

Coqの説明は難しいので、詳細は検索して下さい。m(__)m

Coq - Wikipedia

Coqは証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。

employment.en-japan.com

qiita.com

定理証明支援とは数学の定理を自動で証明することではなく、ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである。

Coq　パッケージマネージャー　ocamlと同じopam

証明支援には半自動と全自動があるみたいです。

自動定理証明 - Wikipedia

自動定理証明（英: automated theorem proving, ATP）とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。

産業への応用

産業分野での応用例としては、LSIの設計とその検証が挙げられ、モデル的手法とともに使われている。Pentium FDIV バグ以来、FPUの設計は極めて厳密に行われている。AMDやインテルはプロセッサの設計検証に自動定理証明を使っている。

Haskell風のcodec-beam

HaskellでもErlang VM上で動くコードを書けます。

「てか、Haskell使えるなら、Erlangぐらい使えるだろ？Erlangを直接使えよ！」という声も聞こえてきそうですが、Erlang VMの人気があるからですね？

hackage.haskell.org

Erlang VM byte code assembler for implementing compile-to-beam languages.

The goal is to a provide delightful API for generating BEAM instructions from pure Haskell.

github.com

以上、Erlang VM上で動くプログラミング言語の調査結果でした。

他にもあったら、是非教えて下さい。m(__)m

Erlangのエコシステムを参考にして、Java／Java VMの代替を検討してみたいと思います。