前回から引き続き、Haskell Implementors’ Workshop 2019への参加レポートとして、私の印象に残った発表を紹介します。
今回は、Copilotという、C言語のコードを生成するHaskell製内部DSLについての発表です。

Contents

Copilot 3.0: a Haskell runtime verification framework for UAVs
Copilotを試してみる

Link to
hereCopilot 3.0: a Haskell runtime verification framework for UAVs

発表者: Frank Dedden Royal Netherlands Aerospace Center, Alwyn Goodloe NASA Langley Research Center, Ivan Perez NIA / NASA Formal Methods

Haskell製の内部DSLからC言語のソースコードを生成する、Copilotの紹介です。
似た謳い文句の内部DSLとしてivoryがありますが、Copilotは、ハードウェアの実行時検証を行うC言語のコードを生成することに、より特化しています。
「センサーから信号を受け取って、一定の条件を満たした場合に何らかの処理を実行する」という処理をHaskellで宣言的に記述すると、メモリの消費量・実行時間において常に一定なC言語のコードを生成することが出来ます。

メモリが限られていて、リアルタイムな処理が必要なハードウェアにとって「邪魔にならない監視」を実現するための必須条件なのでしょう。
現状HaskellはGCが必要であるといった制約もあり、リアルタイムな処理や厳格なメモリー管理が必要な機器での採用は難しいですが、Ivoryや今回発表されたCopilotはあくまでも「C言語のコードを生成するだけ」なので、生成するHaskellではメモリー管理をする必要がありません。
にっくきスペースリークに悩まされる心配もないのです。
こういったHaskell製内部DSLは、Haskellの持つ強い型付けによるメリットを享受しながら、変換した言語の実行時におけるパフォーマンスを出しやすい、といういいとこ取りなメリットがあるので、もっと広まってほしいユースケースですね。

Link to
hereCopilotを試してみる

ℹ️ 実際に使用したコードはHaskell-jp BlogのGitHubのリポジトリーにあります。
ℹ️ 使用したcopilotパッケージのバージョンは、3.0.1です。
ℹ️ サンプルコードの解説については、notogawaさんのアドバイスも参考になりました（Haskell-jpのslack-logではこのあたり。執筆時点でCSSが当たってないため読みづらいですが一応）。ありがとうございます！

せっかくなんでCopilotを試してみましょう。
公式サイトにあったサンプルコードそのまんまですが、生成されるCのコードを眺めてみます。

👇のコマンドでサンプルコードが入ったリポジトリーをgit cloneした後、

git clone https://github.com/haskell-jp/blog
cd blog/examples/2019/hiw-copilot

👇のコマンドでビルド・C言語によるコードの生成できるはずです。

stack build copilot
stack exec runghc heater.hs

こちらが生成元のHaskellのコードです。

import Language.Copilot
import Copilot.Compile.C99

import Prelude hiding ((>), (<), div)

temp :: Stream Word8
temp = extern "temperature" Nothing

ctemp :: Stream Float
ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0

spec = do
  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
  trigger "heatoff" (ctemp > 21.0) [arg ctemp]

main = reify spec >>= compile "heater"

まず、tempとctempという識別子に定義した式が、センサーが発信する、連続的に変化する値を表しています。
Copilotの言葉はこれをStreamと呼んでいます。

specという識別子で定義している式が、「どのセンサーから信号を受け取って、どんな条件を満たした場合にどの処理を実行するか」規定しているようです。
👆の場合、ctempというStreamが18.0を下回ったらheatonというイベントを発火し、21.0を超えたらheatoffというイベントを発火する、と定めているわけですね。
そしてmain関数で実行しているreify spec >>= compile "heater"という箇所で、.hファイルと.cファイルを書き込んでいます。

そして、生成されたヘッダーファイルheater.hがこう👇

extern uint8_t temperature;
void heatoff(float heatoff_arg0);
void heaton(float heaton_arg0);
void step(void);

で、肝心のCのコード本体heater.cがこちらです。

#include <stdint.h>
#include <stdbool.h>
#include <string.h>

#include "heater.h"

static uint8_t temperature_cpy;

bool heatoff_guard(void) {
  return ((((float)(temperature_cpy)) * ((150.0) / (255.0))) - (50.0)) > (21.0);
}

float heatoff_arg0(void) {
  return (((float)(temperature_cpy)) * ((150.0) / (255.0))) - (50.0);
}

bool heaton_guard(void) {
  return ((((float)(temperature_cpy)) * ((150.0) / (255.0))) - (50.0)) < (18.0);
}

float heaton_arg0(void) {
  return (((float)(temperature_cpy)) * ((150.0) / (255.0))) - (50.0);
}

void step(void) {
  (temperature_cpy) = (temperature);
  if ((heatoff_guard)()) {
    (heatoff)(((heatoff_arg0)()));
  };
  if ((heaton_guard)()) {
    (heaton)(((heaton_arg0)()));
  };
}

先ほどStreamとして定義した値のうち、tempは、temperatureというグローバル変数と、それを一時的に保存するtemperature_cpyという二つの変数に翻訳されました。
specにおいてtriggerという関数で列挙した「どのセンサーから信号を受け取って、どんな条件を満たした場合にどの処理を実行するか」というルールは、stepという関数に現れたようです。
この関数を利用する側では、heaton関数とheatoff関数を別途定義した上で、temperatureにセンサーから受け取った値を代入してstepを呼ぶことによって、temperatureの値が条件に一致したとき、heaton関数とheatoff関数を実行してハードウェアの制御ができるのでしょう。
Haskell側で定義したもう一つのStream、ctempは、heaton_guard、heaton_arg0、heatoff_guard、heatoff_arg0、それぞれの関数に書かれた、temperature_cpyの値を変換する式に現れているようです。

正直なところこの程度であれば、直接Cで書いた方が余計なカッコもないし読みやすそうではあります。
tempをctempに変換する式(150.0 / 255.0) - 50.0が変換後のソースコードでは冗長に適用されていることから、もっと最適化できそうですし。
とはいえ、わざわざDSLを作ったからには、より複雑で、Haskellでなければ書いてられないようなケースが、Copilotの開発者の現場ではあるのでしょう（なんせNASAの方も関わっているぐらいですから！）。
詳しいユースケースや、ビルド時のフローといった運用方法を聞きたいところですね。

HIW 2019で発表された、Copilotという内部DSLについて

～HIW 2019参加レポートその4～

Link to
hereCopilot 3.0: a Haskell runtime verification framework for UAVs

Link to
hereCopilotを試してみる

Link to hereCopilot 3.0: a Haskell runtime verification framework for UAVs

Link to hereCopilotを試してみる

Link to
hereCopilot 3.0: a Haskell runtime verification framework for UAVs

Link to
hereCopilotを試してみる