依存型の紹介と応用としてのClashの紹介

# 目的

19番目の Advent Calender 2017 Haskell（その2）です。

依存型とは何か、何に役に立つのか、その応用としてのClashと
[Clash](http://www.clash-lang.org/)を用いた論理回路の実装のトライアルの紹介をします。

# 依存型とは何か

[Wikipediaの依存型](https://ja.wikipedia.org/wiki/%E4%BE%9D%E5%AD%98%E5%9E%8B)の[リンク先](http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf)に他の型の値に依存する型が依存型とあります。例えば、Boolの値はTrue,Falseがありますが、Boolが型なのはもちろんですが、TrueやFalseも型として扱えるようになります。

その代表的なものとして、リストの要素数を埋め込んだ型があります。例えば、普通のBoolのリストは[Bool]な感じで長さに決まりはないですが、Vector 5 Boolのように長さ5のBool型のリストが作れます。([vector-sized](http://hackage.haskell.org/package/vector-sized-0.6.1.0/docs/Data-Vector-Storable-Sized.html)パッケージで実際に作れます。)

型に値を埋め込むだけだとありがたみがないですが、[カリー＝ハワード同型対応](https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C)で「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)といわれているので、証明をやるにはリッチな型が必要なのです。

# 依存型が何に役に立つのか

依存型の応用には以下のものがあります。他にもあると思いますが。

* プログラムの証明
    * Coq, Agdaなどの定理証明支援システム
* 固定長の配列、行列
    * Deep Learningで使うテンソルの次元を型に埋め込むケース
        * [実装例](https://blog.jle.im/entry/practical-dependent-types-in-haskell-1.html)
        * [haskellによるpythonのtensorflowのラッパ](https://github.com/GU-CLASP/TypedFlow)
    * 配列の次元を型に埋め込むケース
        * [vector-sized](http://hackage.haskell.org/package/vector-sized-0.6.1.0/docs/Data-Vector-Storable-Sized.html)
        * [clash-prelude](http://hackage.haskell.org/package/clash-prelude-0.11.2/docs/CLaSH-Sized-Vector.html)
* スーパーモナド
    * ステートを型に埋め込むケース
        * [アドベントカレンダーの10日の記事の指標付きモナド](https://qiita.com/tnagao7/items/11a6e667011d530832e8)
        * [idrisの例](https://www.idris-lang.org/SSGEP/lecture2.pdf)
* データベースのスキーマ
    * OuryさんとSwierstraさんのものがあるらしいが、[こちらに例があります。](http://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf)


# Clashとは、その近況

clashはhaskellで書けるハードウェア記述言語です。

ハードウェアの記述の階層は3つあります。

1. ゲートレベル
    * スタンダードセルやFPGAの素子レベル
2. [レジスタトランスファーレベル(RTL)](https://ja.wikipedia.org/wiki/%E3%83%AC%E3%82%B8%E3%82%B9%E3%82%BF%E8%BB%A2%E9%80%81%E3%83%AC%E3%83%99%E3%83%AB)
    * クロックによるサイクル単位の設計
    * 記憶素子のレジスタと状態のない論理回路の世界
    * レジスタは設計者が明示する
    * 論理圧縮は論理合成ツールの仕事で合成ツールはRTLをゲートレベルに変換する。
    * Clashはこのレベル。
3. 高位合成
    * レジスタは設計者が明示しない
    * コンパイラによって勝手にステートマシンができる
    * サイクルの指定がないとコンパイラが適当に設定する
    * c言語から回路を生成とかはこのレベル

ClashはRTLを記述し、verilog,VHDLなどの他のRTLを出力します。ghc-apiを使ってhaskellのコードをパースしてRTLに変換しているのでghc拡張が使えます。

単にRTLを記述するだけでなく、依存型を用いて、
8bitのビット列は```BitVector 8```
8bitのビット列を8つ束ねたものを```Vec 8 (BitVector 8)```
と書けます。

副作用のない組み合わせ回路は下記のように書けます。

```haskell
adder' :: BitVector 8 -> BitVector 8 -> BitVector 8
adder' a b = a + b
```

Systemクロックに同期する信号は```Signal System (BitVector 8)```
とし、下記のように書くとaとbを足したあとレジスタにいれる回路になります。

```haskell
adder :: Signal System (BitVector 8) -> Signal System (BitVector 8) -> Signal System (BitVector 8)
adder a b = register 0 $ a + b
```

副作用ない組み合わせ回路をつかって、[mealyマシン](https://ja.wikipedia.org/wiki/%E3%83%9F%E3%83%BC%E3%83%AA%E3%83%BB%E3%83%9E%E3%82%B7%E3%83%B3)でステートを持つ回路が記述できます。
ただ、mealyマシンだとレジスタを内部のstateに割り当てるだけなので、回路の出力にレジスタを置きたいときには使いづらいです。

```haskell
adder' :: (BitVector 8,BitVector 8) -> BitVector 8
adder' (a,b) = a + b

madder :: Signal System ((BitVector 8),(BitVector 8)) -> Signal System (BitVector 8)
madder = mealy (\state input -> ((adder' input),state))) 0
```

クロックを明示するスタイルと明示しないスタイル（Systemクロックが自動で使われる）が使い分けられ、haskellを使っているのでmapなどの高階関数が使えます。

Clashはそろそろghc 8.2に対応した1.0がリリースされます。
新しいバージョンでクロックだけでなく、リセット信号も型で明示できるようになります。
今hackageに挙がっているものとだいぶ記述の仕方が変わっているので、下記のようにしてgitのものを使いましょう。

```
> git clone git@github.com:clash-lang/clash-compiler.git
> cd clash-compiler
> git submodule init
> git submodule update
> stack install
```

# I2C Slaveとステッピングモーターコントローラの実装

今回I2C SlaveになるステッピングモーターコントローラをClashで書いてみました。[I2C](https://ja.wikipedia.org/wiki/I2C)はチップ間のバスです。また、[ステッピングモーター](https://ja.wikipedia.org/wiki/%E3%82%B9%E3%83%86%E3%83%83%E3%83%94%E3%83%B3%E3%82%B0%E3%83%A2%E3%83%BC%E3%82%BF%E3%83%BC)はプリンタに使われている位置決めが容易なモーターです。

ターゲットのデバイスは[AlteraのCycloneII EP2C5T144のFPGA](https://www.amazon.co.jp/dp/B0747SYB5C)です。

今回の回路はモーター18個に対応しています。

[こちら](https://github.com/lets-make-something/clash-stepper-motor
)にhaskellのコードとそれから生成したverilogのファイルを置きました。テスト不足でまだ動かないですが、生成されたverilogの記述をみると人間がよめる形式（registerと組み合わせ回路が明示されていて）になっていて素晴らしいです。

# 合成結果

[Quartus II 12.1](https://www.altera.co.jp/downloads/software/quartus-ii-we/121.html)で合成しました。（最新のものだとなぜかFPGAに書き込めなかったので古いものを使いました。）

結果は下記です。大変小さいデバイスですが、ロジックの利用率は8%で無駄なものはできてなさそうです。今回はピンネックでこれ以上のステッピングモーターコントローラーは詰め込めなさそうです。

```
Flow Status	Successful - Tue Dec 19 19:23:39 2017
Quartus II 64-Bit Version	12.1 Build 177 11/07/2012 SJ Web Edition
Revision Name	stepper
Top-level Entity Name	Top_topEntity
Family	Cyclone II
Device	EP2C5T144C6
Timing Models	Final
Total logic elements	391 / 4,608 ( 8 % )
Total combinational functions	304 / 4,608 ( 7 % )
Dedicated logic registers	251 / 4,608 ( 5 % )
Total registers	251
Total pins	77 / 89 ( 87 % )
Total virtual pins	0
Total memory bits	0 / 119,808 ( 0 % )
Embedded Multiplier 9-bit elements	0 / 26 ( 0 % )
Total PLLs	0 / 2 ( 0 % )
```

# まとめと今後

Haskellの依存型を用いたハードウェア記述言語のClashを紹介し、それを利用してI2C Slaveとステッピングモーターコントローラーを実装しました。依存型もClashも十分実用レベルになっていることが確認できました。

次回はちゃんとステッピングモーターが動いている動画を用意したいです。