これは Haskell Advent Calendar 2025 の 14 日目の記事である（予約機能など無いためややフライング気味）。

はじめに

せっかくブログを立てたのだし、アドベントカレンダーというものを書いてみようと思い、卒業論文が間近に迫る中記事を書くことにした。そこで必要になってくるのがテーマなのだが、そういえば 前回 、関数 (!!) :: [a] -> Int -> a の長さ付きリスト版を実装するのに詰まってしまい、断念してしまったことを思い出した。そこで、 (!!) の実装に再挑戦し、それを記事にしようと思ったのだが、思いの外簡単に実装できてしまった。ということでこの記事では (!!) の他に、リストに対して定義されているいくつかの関数の長さ付きリスト版を実装していこうと思う。

なお、実装したコードはどれも “RequiredTypeArguments” を利用したものとなっているが、 forall a -> ... の箇所をすべて Proxy a -> ... にしてもほとんどの場合で問題なく動作する。しかし、Prelude と同じようなインタフェースを提供できることを確認したり、来る Dependent Haskell に思いを馳せたりするために “RequiredTypeArguments” を利用した。

また、記事中の Haskell ソースコードはすべて CC0-1.0 ライセンスのもとで公開している。

使用したライブラリとプラグインなど

この記事では GHC 9.12 を使用している。この記事の要である “RequiredTypeArguments” 拡張は GHC 9.10 で実装されたものであるため、 GHC 9.10 でも問題なく動作するものと思われる。また、素の GHC では組み込みの型レベル自然数の型計算が貧弱なため、コンパイラプラグインをいくつか利用した。利用したプラグインとライブラリは以下である。

• equational-reasoning
• ghc-typelits-natnormalise
• ghc-typelits-knownnat
• type-natural

また、ソースコードは GHC2024 のもとで書かれている。

実装

今回使用する長さ付きリストは以下のように定義されている。いろいろなところでよく目にする形だろうと思う。

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

これを使って head :: [a] -> a や tail :: [a] -> [a] 、generate :: Int -> (Int -> a) -> [a] の長さ付きリスト版を実装したのが 前回 だった。ここでは generate 関数のみ抜粋しておく。

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

leqToCmp や ltToSuccLeq といった関数を利用することで自然数についての性質を証明している。これらの関数の戻り値をパターンマッチすることで、それぞれの節の右辺で GHC はその性質を仮定できるようになる。したがって Haskell で定理証明をしながらプログラムを書くときは case 式を多用することになると思う。

例えば leqToCmp の場合、この関数の戻り値は Either (a :~: b) (CmpNat a b :~: 'LT) である。このとき GHC は、 Left Refl -> <expr> の右辺で
a :~: b すなわち $a = b$ を仮定することができ、 Right Refl -> <expr> の右辺で CmpNat a b :~: LT すなわち $a < b$ を仮定することができる。ちなみにこの関数は

$$ \forall a, b \in \mathbb{N} : a \le b \Rightarrow (a = b \lor a \lt b) $$

という定理を表している。もう一つちなむと、 ltToSuccLeq は $$ \forall a, b \in \mathbb{N} : a \lt b \Rightarrow a + 1 \le b $$ という定理を表している。

さて、ここからが本題である。 (!!) の実装は以下のようになった。

(!!) :: forall n a. Vector n a -> forall i -> (KnownNat i, KnownNat n, i + 1 <= n) => a
v !! i = case leqToLT sNati sNatn Witness of
    Refl -> case zeroOrSucc sNati of
        IsZero -> case v of
            Cons x _ -> x
        IsSucc sNatim1 -> withWitness (lneqZero sNatim1) $
            case cmpSucc sZero sNatim1 of
                Refl -> withWitness (leqTrans sOne sNati sNatn Witness Witness) $
                    case v of
                        Cons _ xs -> xs !! (type (i - 1))
  where
    sNati = SNat @i
    sNatn = SNat @n

この関数は i < length v のときに定義され、 i == 0 なら v -> (x:xs) であるため x を返し、そうでないときは xs !! (i - 1) を返すという流れの合間に定理証明をちょくちょく挟んでいる形になっている。使っている関数と対応する定理を以下の表に示した。

次に take の実装を示す。

take :: forall m -> (KnownNat m) => Vector (m + n) a -> Vector m a
take m xs = case zeroOrSucc (SNat @m) of
    IsZero -> Nil
    IsSucc sNatnm1 -> withWitness (lneqZero sNatnm1) $
        case xs of
            Cons y ys -> Cons y $ take (type (m - 1)) ys

こちらは先程よりも短く済み、なおかつより読みやすくなっていることと思う。この関数は以下の Haskell コードをほとんどそのまま書き下したものになっている。

take' :: Int -> [a] -> [a]
take' m xs
    | m == 0 = []
    | m > 0  = case xs of
        y : ys -> y : take' (m - 1) ys

splitAt も同様だ。

splitAt :: forall i -> (KnownNat i) => Vector (i + n) a -> (Vector i a, Vector n a)
splitAt i v = case zeroOrSucc (SNat @i) of
    IsZero -> (Nil, v)
    IsSucc sNatim1 -> withWitness (lneqZero sNatim1) $
        case v of
            Cons x xs ->
                let (ys, zs) = splitAt (type (i - 1)) xs
                in
                    (Cons x ys, zs)

これら 2 つの関数が (!!) と比べて対応がわかりやすいことに理由はあるのだろうか。単純にコンパイラプラグインの力を借りやすい型になっているからという可能性はあるが、よく分からない。もしかしたら、 (!!) の方にもより簡単に実装できるような型の書き方があるのかもしれない。

使ってみる

さて、実装した関数を GHCi で雑に使ってみる。

ghci> v = generate 10 id
ghci> v
Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 (Cons 6 (Cons 7 (Cons 8 (Cons 9 Nil)))))))))
ghci> v !! 4
4
ghci> v !! 10
<interactive>:8:3: error: [GHC-64725]
    • Cannot satisfy: 11 <= 10
    • In the expression: v !! 10
      In an equation for ‘it’: it = v !! 10

ghci> take 5 v
Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))
ghci> take 15 v
<interactive>:11:9: error: [GHC-83865]
    • Couldn't match type ‘15 + n0’ with ‘10’
      Expected: Vector (15 + n0) Natural
        Actual: Vector 10 Natural
      The type variable ‘n0’ is ambiguous
    • In the second argument of ‘take’, namely ‘v’
      In the expression: take 15 v
      In an equation for ‘it’: it = take 15 v

ghci> splitAt 7 v
(Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 (Cons 6 Nil)))))),Cons 7 (Cons 8 (Cons 9 Nil)))
ghci> splitAt 100 v
<interactive>:14:1: error: [GHC-18872]
    • Couldn't match type ‘100 + n0’ with ‘10’
        arising from a use of ‘it’
      The type variable ‘n0’ is ambiguous
    • In the first argument of ‘print’, namely ‘it’
      In a stmt of an interactive GHCi command: print it

ghci> ghci> splitAt 10 v
(Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 (Cons 6 (Cons 7 (Cons 8 (Cons 9 Nil))))))))),Nil)

take や splitAt の方が簡単なコードになった反面、エラーメッセージは (!!) の方がわかりやすい印象がある。もしかしたらこの辺りはトレードオフなのかもしれない。

さいごに

前回 実装したときは定理証明に詰まり、かなり面倒だったという印象が残っていたが、今回はさほど時間をかけずに関数を実装することができた。

また、例によってソースコードは公開されており、 ここ にある。