Levity polymorphism対応の型クラスと、定数メソッド

Levity polymorphismを使うと、通常の（boxed, liftedな）型だけではなくて、unliftedな型（慣習として型名の最後に # がついているやつ）に対しても型クラスによる抽象化を提供できる。

例えば、通常の Int とunboxedな Int# に関して共通の足し算関数を使いたかったら、

Levity1.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
import GHC.Exts (TYPE, Int#, (+#))

class Additive (a :: TYPE r) where
  add :: a -> a -> a

instance Additive Int where
  add = (+)

instance Additive Int# where
  add = (+#)

と定義すれば良い。

さて、「足し算」だけではなくて、「足し算に関するゼロ元」も型クラスで抽象化したい場合はどうすれば良いか。

普通（lifted型のことだけを考える）であれば

class Additive a => AdditiveWithZero a where
  zero :: a

instance AdditiveWithZero Int where
  zero = 0

とすれば良いのだが、これはunlifed型に対してうまくいかない：

instance AdditiveWithZero Int# where  -- エラー！
  zero = 0#

Levity1.hs:21:27: error:
    • Expecting a lifted type, but ‘Int#’ is unlifted
    • In the first argument of ‘AdditiveWithZero’, namely ‘Int#’
      In the instance declaration for ‘AdditiveWithZero Int#’
   |
21 | instance AdditiveWithZero Int# where
   |                           ^^^^

型クラスの定義にカインド注釈をつけてlevity polymorphismに対応させようとしても、

class Additive a => AdditiveWithZero (a :: TYPE r) where
  zero :: a  -- エラー！

Levity1.hs:16:11: error:
    • Expected a type, but ‘a’ has kind ‘TYPE r’
    • In the type signature: zero :: a
      In the class declaration for ‘AdditiveWithZero’
   |
16 |   zero :: a
   |           ^

という風にエラーが出る。

（標準の型クラスでこういう風にlevity polymorphismに対応できないものとしては、 Bounded や Monoid などがある）

ダミーの引数を追加する（→美しくなくなる）

型クラス辞書のフィールドにunliftedな型が入ってくるのが問題なので、ダミーの引数を追加して

Levity2.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE ExplicitForAll #-}
import GHC.Exts (TYPE, Int#, (+#), Proxy#, proxy#)

class Additive (a :: TYPE r) where
  add :: a -> a -> a

instance Additive Int where ...
instance Additive Int# where ...

class Additive a => AdditiveWithZero (a :: TYPE r) where
  zeroP# :: Proxy# a -> a

instance AdditiveWithZero Int where
  zeroP# _ = 0  -- 美しくない

instance AdditiveWithZero Int# where
  zeroP# _ = 0#

zero :: forall (a :: TYPE r). AdditiveWithZero a => a
zero = zeroP# proxy#

と定義すればうまくいくが、通常の Int みたいな型に関するインスタンスを定義する側でダミーの引数を受け取らなければならない（levity polymorphismを意識しないといけない）のが美しくない。なんとか、 AdditiveWithZero Int の定義は

instance AdditiveWithZero Int where
  zero = 0

のままで済ませることはできないだろうか。

ダミーの制約を追加する（→簡潔！）

型クラスの定義に zero :: a と書いてしまうと型クラス辞書にunliftedな型が入り込むのが問題なので、ダミーの引数を追加しようという発想自体は間違っていない。ダミーの引数を値レベル（() や Proxy# a）で追加しようとするとインスタンスでのメソッド定義が美しくなくなるのが問題なので、ダミーの引数は型制約として追加すれば良い。

つまり、 ConstrainedClassMethods を使い、以下のように書けば問題は解消される。

class (...) => AdditiveWithZero (a :: TYPE r) where
  zero :: (r ~ r) => a

こうすると、型クラス辞書に入るのは a という型ではなくて、何かしらの関数になる¹ので、unliftedな型に対しても通用するようになる。つまり、下記のコードはコンパイルが通る：

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstrainedClassMethods #-}
import GHC.Exts (TYPE, Int#, (+#))

class Additive (a :: TYPE r) where
  add :: a -> a -> a
instance Additive Int where ...
instance Additive Int# where ...

class Additive a => AdditiveWithZero (a :: TYPE r) where
  zero :: (r ~ r) => a

instance AdditiveWithZero Int where
  zero = 0

instance AdditiveWithZero Int# where
  zero = 0#

（筆者は当初

class Additive a => AdditiveWithZero (a :: TYPE r) where
  {-# MINIMAL zero | zeroP# #-}
  zero :: (r ~ 'LiftedRep) => a
  zero = zeroP# proxy#

  zeroP# :: Proxy# a -> a
  default zeroP# :: (r ~ 'LiftedRep) => Proxy# a -> a
  zeroP# _ = zero

を試していたが、 zero の定義で何かしらの制約が課されていることが重要なので、 r ~ 'LiftedRep を課す必要は別になかった）

潜在的な問題点

Proxy# a -> a にせよ r ~ r => a にせよ、型クラス辞書に入るのが値ではなくて関数になるので、それに伴う問題が発生する可能性がある。

つまり、各インスタンスにおける zero の定義で複雑な計算をしていた場合、それが複数回実行される可能性がある。例えば、

class Additive a => AdditiveWithZero a where
  zero :: a

instance AdditiveWithZero Int where
  zero = trace "hoge" 0

という定義の場合、GHCiで試すと zero :: Int を複数回叩いても hoge は一回しか印字されないのに対し、

class Additive a => AdditiveWithZero (a :: TYPE r) where
  zero :: (r ~ r) => a

instance AdditiveWithZero Int where
  zero = trace "hoge" 0

という定義だと zero :: Int を評価するたびに hoge が表示される。

まあこの辺はGHCの最適化で変わるかもしれないし、

zeroInt :: Int
zeroInt = trace "hoge" 0
instance AdditiveWithZero Int where
  zero = zeroInt

とすれば回避できるし、そもそも zero とか mempty とか maxBound, minBound という定数の定義で複雑な計算を行うことはない気がするので、大きな問題ではないだろう。

雑感

これ（ダミーの型制約の追加）、人間ではなくGHCがやるべきでは？

GHCにおいて型クラスは辞書渡しとして表現されるので、型クラス制約を持つ定数というのは実行時には辞書を取る関数となる。同様のことは型クラスだけでなく、equality制約にも言えるようだ（GHC 8.6.3で確認）。 ↩