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

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

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

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

```haskell: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型のことだけを考える）であれば

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

instance AdditiveWithZero Int where
  zero = 0
```

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

```haskell
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に対応させようとしても、

```haskell
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な型が入ってくるのが問題なので、ダミーの引数を追加して

```haskell: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` の定義は

```haskell
instance AdditiveWithZero Int where
  zero = 0
```

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

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

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

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

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

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

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

```haskell
{-# 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#
```

（筆者は当初

```haskell
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` の定義で複雑な計算をしていた場合、それが複数回実行される可能性がある。例えば、

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

instance AdditiveWithZero Int where
  zero = trace "hoge" 0
```

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

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

instance AdditiveWithZero Int where
  zero = trace "hoge" 0
```

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

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

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

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

## 雑感

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