GHC 9.10.1 にて、 “RequiredTypeArguments” なる言語拡張が実装された。この拡張は、Haskell に依存型を追加するという計画の一環であるらしい。

これを有効化すると、項の位置に型を置けるようになる。この記事では、この言語拡張を用いて長さ付きリストを実装し、遊んでみることにする。

基本的な使い方

“RequiredTypeArguments” 言語拡張を有効化すると、具体的には以下のコードが書けるようになる。

{-# LANGUAGE RequiredTypeArguments #-}

id :: forall a -> a -> a
id _ x = x

我々がよく知っている関数 id :: forall a. a -> a とは型が少し異なっていることがわかると思う。この forall a -> の部分が “RequiredTypeArguments” により追加された構文で、「可視な forall 」とも呼ばれる。

そして、これを GHCi で実行すると以下のようになる。

ghci> id Int 40
40
ghci> id String 40
<interactive>:11:11: error: [GHC-39999]
    * No instance for `Num String' arising from the literal `40'
    * In the second argument of `id', namely `40'
      In the expression: id String 40
      In an equation for `it': it = id String 40

ghci> id _ "aaa"
"aaa"

型を明示的に与えるだけでなく、 GHC に推論させることもできるようだ。また、 id String 40 のように、与えた型と値の型が異なるとエラーになるらしい。

基本的な使い方等は把握できたと思うので、これを使って遊んでみる。

長さ付きリストを実装してみる

ここからは、“RequiredTypeArguments” 言語拡張を使用して、長さ付きリストやそれを使用した型安全な関数を実装していく。

ここからのコードでは、暗黙のうちに次の言語拡張を有効化している。

RequiredTypeArguments
ExplicitNamespaces
GADTs
DataKinds
NoStarIsType
StandaloneDeriving
ScopedTypeVariables
RankNTypes
TypeOperators
TypeApplications
KindSignatures

長さ付きリストを以下のように定義してみる。

data Vector (n :: Natural) a where
    Nil :: Vector 0 a
    Cons :: a -> Vector n a -> Vector (n + 1) a

これを使って、関数 head を型安全にすることができる。

head :: Vector (n + 1) a -> a
head (Cons x _) = x

これを GHCi で実行してみる。

ghci> head $ Cons 1 Nil
1
ghci> head $ Cons "a" $ Cons "b" Nil
"a"
ghci> head Nil
<interactive>:4:6: error: [GHC-83865]
    • Couldn't match type ‘1’ with ‘0’
      Expected: Vector (0 + 1) a
        Actual: Vector 0 a
    • In the first argument of ‘head’, namely ‘Nil’
      In the expression: head Nil
      In an equation for ‘it’: it = head Nil

Nil を head に適用しようとするとエラーを起こすことがわかる。

関数 tail も同様に定義できると思うかも知れない。

tail :: Vector (n + 1) a -> Vector n a
tail (Cons _ xs) = xs

しかし、 GHC 9.10.1 では以下のようなエラーが発生する。

error: [GHC-25897]
    • Could not deduce ‘n1 ~ n’
      from the context: (n + 1) ~ (n1 + 1)
        bound by a pattern with constructor:
                   Cons :: forall a (n :: Natural).
                           a -> Vector n a -> Vector (n + 1) a,
                 in an equation for ‘tail’
        at sized-list.hs:27:7-15
      Expected: Vector n a
        Actual: Vector n1 a
      ‘n1’ is a rigid type variable bound by
        a pattern with constructor:
          Cons :: forall a (n :: Natural).
                  a -> Vector n a -> Vector (n + 1) a,
        in an equation for ‘tail’
        at sized-list.hs:27:7-15
      ‘n’ is a rigid type variable bound by
        the type signature for:
          tail :: forall (n :: Natural) a. Vector (n + 1) a -> Vector n a
        at sized-list.hs:26:1-38
    • In the expression: xs
      In an equation for ‘tail’: tail (Cons _ xs) = xs
    • Relevant bindings include
        xs :: Vector n1 a (bound at sized-list.hs:27:14)
        tail :: Vector (n + 1) a -> Vector n a
          (bound at sized-list.hs:27:1)
   |
27 | tail (Cons _ xs) = xs
   |                    ^^

これは、GHC が $ n + 1 = m + 1 $ から $ n = m $ を帰結することができないことによる。一方で、これは自然数の上の関数 $ f(x) = x + 1 $　が単射であることから容易にわかる。

このようなミスマッチを解消する方法はいくつかあるが、今回は、パッケージ ghc-typelits-natnormalise にて提供されているコンパイラプラグインを使用することにする。このとき、パッケージ ghc-typelits-knownnat も一緒にインストールしておくと良いことがあるかも知れない。これを用いることで、 tail をエラーなく定義することができる。

tail :: Vector (n + 1) a -> Vector n a
tail (Cons _ xs) = xs

ghci> tail (Cons 1 Nil)
Nil
ghci> tail (Cons 1 $ Cons 2 Nil)
Cons 2 Nil
ghci> tail Nil
<interactive>:1:6: error: [GHC-83865]
    * Couldn't match type `1' with `0'
      Expected: Vector (0 + 1) a
        Actual: Vector 0 a
    * In the first argument of `tail', namely `Nil'
      In the expression: tail Nil
      In an equation for `it': it = tail Nil

関数 `generate` を実装してみる

この長さ付きリストを使って、関数 generate を実装してみる。さて、パッケージ vector にて提供されている関数 generate のシグネチャは以下である。

generate :: Int -> (Int -> a) -> Vector a

これの長さ付きリスト版を考えてみる。これは以下のようになる。

generate :: forall (n :: Natural) -> (Natural -> a) -> (KnownNat n) => Vector n a

ここで、カインド Natural を持つ型から、型 Natural を持つ値を得る必要があるため、 KnownNat 制約を追加している。また、以下のような補助関数 generate' も実装する必要がある。

generate' :: forall (i :: Natural) -> forall (n :: Natural) -> (Natural -> a) -> (KnownNat n, KnownNat i, i <= n) => Vector (n - i) a

これを用いることで、 generate は以下のように書ける。

generate n f = generate' 0 n f

この generate' を素直に実装してみると以下のようになると思う。

generate' :: forall (i :: Natural) -> forall (n :: Natural) -> (Natural -> a) -> (KnownNat n, KnownNat i, i <= n) => Vector (n - i) a
generate' i n f =
    case sameNat (SNat @i) (SNat @n) of
        Just Refl -> Nil
        Nothing   -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)

しかし、実際には以下のようなエラーが発生し、定義できない。

sized-list.hs:61:22: error: [GHC-64725]
    * Cannot satisfy: i + 1 <= n
    * In the expression:
        Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
      In a case alternative:
          Nothing
            -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
      In the expression:
        case sameNat (SNat @i) (SNat @n) of
          Just Refl -> Nil
          Nothing
            -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
   |
61 |         Nothing   -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
   |

これは一見するとおかしい。なぜなら、 sameNat (SNat @i) (SNat @n) にて $ i = n $ かどうかを判定しており、この関数は $ i = n $ のときのみ Just Refl を返す。したがって、 Nothing の右辺では $ i \le n \land i \ne n $ より $ i \lt n $ と結論して良いはずだ。また、 $ i, n \in \mathbb{N} $ より $ i \lt n \Rightarrow i + 1 \le n $ である。そのため、このエラーは起こり得ないように思われる。

しかし、 GHC には、「 sameNat が Just Refl を返すならば $ i = n $ である。」ということは分かっても、「 sameNat が Nothing を返すならば $ i \ne n $ である。」ということは分からない。そのため、こちらでそれを教えてやる必要がある。

他のやり方を見つけることができなかったため、以下のコードは少し冗長である可能性がある。

まず、以下のパッケージを依存関係に追加する。

type-natural
equational-reasoning

そして、関数 generate' 内の case 式をひとまず以下のように変更する。

case leqToCmp (SNat @i) (SNat @n) Witness of
    Left  Refl -> Nil
    Right Refl -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)

ここで、 leqToCmp は以下のシグネチャを持つ関数である。

leqToCmp :: SNat a -> SNat b -> IsTrue (a <=? b) -> Either (a :~: b) (CmpNat a b :~: 'LT)

これは、$ \forall a, b \in \mathbb{N} : a \le b \Rightarrow (a = b \lor a \lt b) $ ということを表している。これをパターンマッチすることで、「 leqToCmp が Left を返すならば $ a = b $ であり、 Right を返すならば $ a \lt b $ である。」ということを GHC に知らせることができる。

では、 case 式をこれに変えるとそれで良いのかといえば、実はまだ十分ではない。

sized-list.hs:61:23: error: [GHC-64725]
    * Cannot satisfy: i + 1 <= n
    * In the expression:
        Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
      In a case alternative:
          Right Refl
            -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
      In the expression:
        case leqToCmp (SNat @i) (SNat @n) Witness of
          Left Refl -> Nil
          Right Refl
            -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
   |
61 |         Right Refl -> Cons (f (natVal (Proxy @i))) (generate' (type (i + 1)) n f)
   |

先ほどと全く変わらないエラーが発生する。どうやら、「 $ i \lt n $ ならば $ i + 1 \le n $ である。」ということも GHC に教えてやる必要があるらしい。幸い、以下の関数が提供されており、そのまま使えば良い。

ltToSuccLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)

これは、 $ \forall a, b \in \mathbb{N} : a \lt b \Rightarrow a + 1 \le b $ ということを表している。これを使用して、最終的に関数 generate' は以下のようになった。

generate' :: forall (i :: Natural) -> forall (n :: Natural) -> (Natural -> a) -> (KnownNat i, KnownNat n, i <= n) => Vector (n - i) a
generate' i n f =
    case leqToCmp sNati sNatn Witness of
        Left  Refl -> Nil
        Right Refl -> withWitness (ltToSuccLeq sNati sNatn Refl) $
                            Cons (f $ natVal sNati) $ generate' (type (i + 1)) n f
  where
    sNati = SNat @i
    sNatn = SNat @n

これを GHCi で実行してみる。

ghci> generate 0 id
Nil
ghci> generate 10 (* 1)
Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 (Cons 6 (Cons 7 (Cons 8 (Cons 9 Nil)))))))))
ghci> generate 10 (negate . fromIntegral)
Cons 0 (Cons (-1) (Cons (-2) (Cons (-3) (Cons (-4) (Cons (-5) (Cons (-6) (Cons (-7) (Cons (-8) (Cons (-9) Nil)))))))))
ghci> generate (type (3 - 5)) id
<interactive>:29:1: error: [GHC-39999]
    * No instance for `KnownNat (3 - 5)'
        arising from a use of `generate'
    * In the expression: generate (type (3 - 5)) id
      In an equation for `it': it = generate (type (3 - 5)) id

ghci> generate (type (3 * 5)) (const 3)
Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 Nil))))))))))))))
ghci> :t generate (type (3 * 5)) (const 3)
generate (type (3 * 5)) (const 3)
  :: (Num a, KnownNat (3 * 5)) => Vector (3 * 5) a
ghci> head $  generate (type (3 * 5)) (const 3)
3
ghci> tail $  generate (type (3 * 5)) (const 3)
Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 (Cons 3 Nil)))))))))))))

さいごに

GHC 9.10.1 にて実装された言語拡張 “RequiredTypeArguments” を使用して少し遊んでみた。定理証明のあたりがまだ勉強不足なため、少し冗長な書き方になってしまった気がする。とはいえ、簡単な関数を実装してみることができたので良かった。

また、ところどころシングルトンが必要になる場面があったため、それを完全に取り除くことができるのかどうかは気になるところである。

本当は型安全な (!!) も実装してみたかったが、引き算のあたりで躓いて断念してしまった。いつか再挑戦したい。

完全なソースコードはここに置いてある。

雑記帳

GHC 言語拡張の “RequiredTypeArguments” で遊ぶ

基本的な使い方

長さ付きリストを実装してみる

関数 `generate` を実装してみる

さいごに

GHC 言語拡張の “RequiredTypeArguments” で遊ぶ

基本的な使い方

長さ付きリストを実装してみる

関数 generate を実装してみる

さいごに

関数 `generate` を実装してみる