Haskellのtypeの中身はkind!で!(型レベルハンバーガーの型やいかに?)

 ここ4日間ぐらい、主にDataKindsTypeFamiliesを用いた型レベルハンバーガーの開発(型レベルプログラミング)を行っていた。

成果物はここにあるよ。

typeした型の中身を表示する:kind!

 Hamberger.hsではこんな感じで、型レベル関数の結果を左辺に格納している。

type BasicHamburgerC = HamburgerC Space Space Space Space

type HamburgerC1 = AddTopping BasicHamburgerC Cheese
type HamburgerC2 = AddTopping HamburgerC1 Tomato
type HamburgerC3 = AddTopping HamburgerC2 Meet
type HamburgerC4 = AddTopping HamburgerC3 Ushi
type HamburgerC5 = AddTopping HamburgerC4 Ushi

例えばHamburgerC4HamburgerC5の結果が見たいとき、 もしこれらが(Showである)値であればprintしてあげればいいものの、これらは型である。

 typeされた型を展開して表示するには、GHCiで:kind!を使う。

GHCi> :kind! HamburgerC4
HamburgerC4 :: HamburgerT
= 'HamburgerC 'Cheese 'Tomato 'Meet 'Ushi

GHCi> :kind! HamburgerC5
HamburgerC5 :: HamburgerT
= 'Fail

 ちなみに:infoすれば、それらどうやって(値レベルでいう)束縛を行われたのか と 行われた箇所が見れる。

GHCi> :info HamburgerC4
type HamburgerC4 = AddTopping HamburgerC3 'Ushi :: HamburgerT
        -- Defined at Hamburger.hs:59:1

GHCi> :info HamburgerC5
type HamburgerC5 = AddTopping HamburgerC4 'Ushi :: HamburgerT
        -- Defined at Hamburger.hs:60:1

一言

 ここの一連のtype、よく関数ローカルでいくつかの名前をletしていくのと似てるよねー。

筆者プロフィール

my-latest-logo

aiya000(あいや)

せつラボ 〜圏論の基本〜」 「せつラボ2~雲と天使と関手圏~」 「矢澤にこ先輩といっしょに代数!」を書いています!

強い静的型付けとテストを用いて、バグを防ぐのが好き。Haskell・TypeScript。