CoqのGallinaでは2つのコンストラクタC1, C2のある型Tの式vについて、
if v then t1 else t2
が
match v with | C1 ... => t1 | C2 ... => t2 end
にdesugarされる。
なんだかよくわからないけどかっこいい！！！Haskellでもこれやりたい！！！ やりました。
RebindableSyntaxとGHC.Generics
RebindableSyntaxを有効化すると、
リテラルやif式、do式などのセマンティクスを独自に定義することができる。
例えば、if e1 then e2 else e3はifThenElse e1 e2 e3に変換される。ifThenElseを定義すれば、if式の動作を自分の好きなように書き換えられる！
GHC.Genericsを使うと、データ型について総称的なプログラミングが行える。 詳細は 9.1. Language options — Glasgow Haskell Compiler 8.8.1 User's Guide を読むと良い。 日本語訳は http://www.kotha.net/ghcguide_ja/7.6.2/generic-programming.html 。
GIf型クラス
というわけでGHC.Genericsを用いて総称的な'if'を実装していく。
以下に出てくるコード例では、次のGHC拡張が有効化されていると仮定する: FlexibleContexts, PolyKinds, RebindableSyntax, TypeOperators, UndecidableInstances
最初に、型の総称表現がif式の第一項になれることを表すGIf型クラスと、if式の実装であるifThenElse関数を宣言する。
class GIf f where gIfThenElse :: f p -> b -> b -> b ifThenElse :: (GIf (Rep a), Generic a) => a -> b -> b -> b ifThenElse c = gIfThenElse (from c)
和型を表す(:+:)についてGIfのインスタンスを宣言する。
例えばdata Bool = False | Trueと宣言されているとき、|の左側にあるFalseがL1、右側にあるTrueがR1にあたる。
instance GIf (a :+: b) where gIfThenElse (L1 _) _ x = x gIfThenElse (R1 _) x _ = x
K1とM1についてもGIfのインスタンスを宣言する。
K1は中身をifThenElseに適用する。M1は中身をgIfThenElseに適用する。
このことはそれぞれの型から自明に分かる。
instance (GIf (Rep c), Generic c) => GIf (K1 i c) where gIfThenElse (K1 x) = ifThenElse x instance GIf f => GIf (M1 i t f) where gIfThenElse (M1 x) = gIfThenElse x
これで総称的な'if'が手に入った。さっそくghciで試してみよう。
ghci> :set -XRebindableSyntax ghci> if True then 1 else 2 1 ghci> if Nothing then 1 else 2 2 ghci> if Right 'a' then 1 else 2 1
やったーーー！！！ 一つしかコンストラクタのない型ではコンパイルエラーになってほしい。確かめてみよう。
ghci> if () then 1 else 2 <interactive>:5:1: error: • Could not deduce (GIf U1) arising from an if expression from the context: Num b bound by the inferred type of it :: Num b => b at <interactive>:5:1-19 • In the expression: if () then 1 else 2 In an equation for ‘it’: it = if () then 1 else 2
良さそう。 3つ以上コンストラクタがある型でもコンパイルエラーになってほしい。確かめてみよう。
ghci> :t EQ EQ :: Ordering ghci> if EQ then 1 else 2 1
うーん……
原因を解明しよう。Rep Orderingは以下のような型になる。
type instance Rep Ordering = D1 ('MetaData "Ordering" "GHC.Types" "ghc-prim" 'False) (C1 ('MetaCons "LT" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "EQ" 'PrefixI 'False) U1 :+: C1 ('MetaCons "GT" 'PrefixI 'False) U1))
M1で付加されたメタ情報を取り除くと、U1 :+: (U1 :+: U1)になる。
つまり、3つ以上のコンストラクタを持つ型は「型と和型の和型」のような入れ子構造になっている。
3つ以上のコンストラクタを持つ型を弾くには、入れ子になった(:+:)を弾く必要がある。
NotSum型クラス
入れ子になった(:+:)を弾くために、まずは型の総称表現がa :+: bでないことを表す型クラスNotSumを次のように定義する。
class NotSum (f :: k -> Type) instance NotSum V1 instance NotSum U1 instance NotSum (a :*: b) instance NotSum (K1 i c) instance NotSum f => NotSum (M1 i t f)
(:+:)を除く、型の総称表現に用いられる型すべてをNotSumのインスタンスにした。
続いて、GIf (a :+: b)に型制約NotSum bを追加する。
instance NotSum b => GIf (a :+: b) where gIfThenElse (L1 _) _ x = x gIfThenElse (R1 _) x _ = x
これでうまく動くようになったはずだ。ghciで確認してみよう。
ghci> if EQ then 1 else 2 <interactive>:2:1: error: • Could not deduce (NotSum (C1 ('MetaCons "EQ" 'PrefixI 'False) U1 :+: C1 ('MetaCons "GT" 'PrefixI 'False) U1)) arising from an if expression from the context: Num b bound by the inferred type of it :: Num b => b at <interactive>:2:1-19 • In the expression: if EQ then 1 else 2 In an equation for ‘it’: it = if EQ then 1 else 2 ghci> if True then 1 else 2 1 ghci> if Nothing then 1 else 2 2 ghci> if Right 'a' then 1 else 2 1
うれしーーーー！！！！
