目的

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

依存型とは何か、何に役に立つのか、その応用としてのClashと
Clashを用いた論理回路の実装のトライアルの紹介をします。

依存型とは何か

Wikipediaの依存型のリンク先に他の型の値に依存する型が依存型とあります。例えば、Boolの値はTrue,Falseがありますが、Boolが型なのはもちろんですが、TrueやFalseも型として扱えるようになります。

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

型に値を埋め込むだけだとありがたみがないですが、カリー＝ハワード同型対応で「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)といわれているので、証明をやるにはリッチな型が必要なのです。

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

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

プログラムの証明
- Coq, Agdaなどの定理証明支援システム
固定長の配列、行列
- Deep Learningで使うテンソルの次元を型に埋め込むケース
  - 実装例
  - haskellによるpythonのtensorflowのラッパ
- 配列の次元を型に埋め込むケース
  - vector-sized
  - clash-prelude
スーパーモナド
- ステートを型に埋め込むケース
  - アドベントカレンダーの10日の記事の指標付きモナド
  - idrisの例
データベースのスキーマ
- OuryさんとSwierstraさんのものがあるらしいが、こちらに例があります。

Clashとは、その近況

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

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

ゲートレベル
- スタンダードセルやFPGAの素子レベル
レジスタトランスファーレベル(RTL)
- クロックによるサイクル単位の設計
- 記憶素子のレジスタと状態のない論理回路の世界
- レジスタは設計者が明示する
- 論理圧縮は論理合成ツールの仕事で合成ツールはRTLをゲートレベルに変換する。
- Clashはこのレベル。
高位合成
- レジスタは設計者が明示しない
- コンパイラによって勝手にステートマシンができる
- サイクルの指定がないとコンパイラが適当に設定する
- c言語から回路を生成とかはこのレベル

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

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

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

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

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

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

副作用ない組み合わせ回路をつかって、mealyマシンでステートを持つ回路が記述できます。
ただ、mealyマシンだとレジスタを内部のstateに割り当てるだけなので、回路の出力にレジスタを置きたいときには使いづらいです。

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はチップ間のバスです。また、ステッピングモーターはプリンタに使われている位置決めが容易なモーターです。

ターゲットのデバイスはAlteraのCycloneII EP2C5T144のFPGAです。

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

こちらにhaskellのコードとそれから生成したverilogのファイルを置きました。テスト不足でまだ動かないですが、生成されたverilogの記述をみると人間がよめる形式（registerと組み合わせ回路が明示されていて）になっていて素晴らしいです。

合成結果

Quartus II 12.1で合成しました。（最新のものだとなぜか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も十分実用レベルになっていることが確認できました。

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

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

目的