星にゃーんのブログ

ほとんど無害。

RebindableSyntaxとGHC.Genericsを使って'genericなif'を作る

Haskell

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

うれしーーーー！！！！

完成したコード

gist.github.com