🌝

Haskell の依存型に入門する

2024/06/29に公開

Haskell

依存型

tech

Haskell で依存型を扱う方法について勉強したのでメモを残しておきます。

承前

この記事では要素数つきリスト Vect の実装を例に Haskell で依存型を扱うために必要な知識のごく基礎的な部分についてまとめます。ただし、目指すのは Vect を ある程度 開発できる体制を整えることで、十分に開発できる体制は目指しません。というのは、依存型に関わる知識はそれなりに広大で、全てを収めると記事が非常に長くなってしまい、私の精神衛生上良くないことが起こるためです。

この記事では、Haskell での依存型の開発において必要な知識のうち、証明に関するもの以外を一通り揃えることを目指しますが、個人がひっそりと勉強しながら書き進めたもののため、完全な情報となるかは甚だ疑問です。そのため、誤りや欠落等を発見した場合はご指摘いただけると助かります。

なお、この記事が想定する読者は、Haskell の基本文法は理解しているが、言語拡張などについてはほとんど知識がない開発者（つまり私）です。ちなみにこの記事を読むにあたってモナドの知識などは必要ありません。

そもそも依存型とは

依存型は「定義が値に依存する型」のことですが、ここではおさらいも兼ねて「値に依存する値」「型に依存する値」「型に依存する型」の Haskell での姿を順に見ていこうと思います。

値に依存する値

感触を掴むために、まずは「値に依存する値」について考えてみます。

ここで用いられている「依存する」という言葉は、与えられた対象に応じて内容が定まることを意味します。つまり「値に依存する値」は「与えられた値に応じて内容が定まる値」のことで、要するに関数のことです。

Haskell での実例を以下に示します。

increment :: Int -> Int
increment n = n + 1

言葉の意味さえわかれば簡単ですね。

型に依存する値

先ほどの定義に準ずると「与えられた型に応じて内容が定まる値」ということになりますが、これは結構イメージしずらいのではないでしょうか。少なくとも筆者は初見で具体例を挙げることができませんでした。

しかし、実際には以下のような例を挙げることができます。

maxBound :: Int   -- 9223372036854775807
maxBound :: Word  -- 18446744073709551615

言われてみればなるほどという感じですね。

型に依存する型

先ほど「値に依存する値」は関数に対応すると述べましたが、正確には値レベルの関数が「値に依存する値」に対応し、型レベルの関数は「型に依存する型」に対応します。

型レベルの関数の一番身近な例は型コンストラクタでしょう。例えば Maybe は型 a から Maybe a という型を生成する型コンストラクタです。

Nothing :: Maybe Int
Nothing :: Maybe Bool

型エイリアスも型レベルの関数を定義するのに利用できます。例として、型エイリアスで定義した型レベル関数版の const を示します。

type Const a b = a

somethingInt :: Const Int Bool  -- i.e. Int
somethingInt = 1

こちらも言われてみればという感じですね。

値に依存する型

これまで見てきた「値に依存する値」「型に依存する値」「型に依存する型」は Haskell の標準機能で全て実現されていましたが、標準機能だけで実現できない最後の砦が「値に依存する型」こと依存型です。Haskell で依存型を実現するためには言語拡張が必要です。

「値に依存する型」をこれまでの例に則って述べれば「与えられた値に応じて内容が定まる型」ということになります。ここでは依存型の使用例として有名な要素数付きリストを紹介します。

通常のリストは格納する要素数についての情報を持たず、これがしばしば開発者の悩みの種になります。この文脈で悪名高いのが head で、型は [a] -> a となっており、どんなリストに対しても適用可能に見えるにも関わらず、空のリストに適用すると実行時例外が発生するため、要素数の検証が暗黙的に要求されます。

head []  -- will cause a runtime exception!

これはまさにリストの型が要素数についての情報を持たないが故に生じた不整合性です。従って、もしも要素付きリストが定義できれば、この問題は型レベルで解決できます。

依存型を持つ Haskell と呼ばれる Idris では Vect という名前で要素数付きリストが用意されています。

Idris

zero : Vect 0 Int
zero = []

one : Vect 1 Int
one = [1]

two : Vect 2 Int
two = [1, 2]

Idris の Vect では Haskell のリストにおける head の問題は発生せず、空の Vect に対して head を適用した時点でコンパイルエラーとなります。

Idris

head zero  -- will cause a compile error (instead of a runtime error!)

依存型、素敵ですね。

前置きが長くなりましたが、これと同じことを Haskell でやるにはどうするか、というのが今回の話です。

Haskell で `Vect` を定義する

最初に結論を掲載しておきます。この定義を見て内容を理解できる方は、この章を読む必要はありません。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
import GHC.TypeNats

data Vect (n :: Nat) a where
    Nil :: Vect 0 a
    Cons :: a -> Vect n a -> Vect (n + 1) a

言語拡張を導入して色々やっているので、順を追って説明していきたいと思います。

カインド

Haskell の型レベルプログラミングに着手する際に避けては通れない概念、カインドの説明から始めます。

カインドは型を分類するための集合で、いわば型の型のような役割を果たします。Int や Bool のように単体で成立する型のカインドは * で表現され、Maybe や Either のように型引数を取る型の場合は、型引数の数に応じて * -> * や * -> * -> * などと表現されます。

GHCI では :kind というコマンドを使用することで型のカインドを確認できます。

ghci> :kind Int
Int :: *
ghci> :kind Maybe
Maybe :: * -> *
ghci> :kind Either
Either :: * -> * -> *

Haskell の依存型においてカインドは重要な役割を果たします。というのは、Haskell の依存型は「型のカインドへの昇格」を通じて実現されるためです。

イメージを述べると、値・型・カインドには以下のような序列関係がありますが、

値 :: 型 :: カインド

上記の型をカインドとしても扱えるようにすることで、型がカインドに並置されます。これによって値も型と並置され、型レベルで値が扱えるようになるというのが Haskell での依存型のイメージです。

値 :: 型 :: カインド
　 :: 値 :: 型

なお、２行目の最左が空になっていますが、これは昇格した値を型に持つ値が存在しないためです。型に昇格した値は専ら型レベルでの演算のためにのみ使用されます。

DataKinds

Haskell での依存型は型のカインドへの昇格によって実現されますが、DataKinds はまさにそれを行うための言語拡張です。Haskell の依存型においては最も重要な言語拡張と言えるかもしません。

GHCI での実例を示します。まずは DataKinds を利用していない状態で、値に対して :kind を実行してみます。ここでは Bool 型の値である True を例に実行してみます。

ghci> :kind True

<interactive>:1:1: error: [GHC-76037]
    Not in scope: type constructor or class ‘True’
    Suggested fix:
      Perhaps you intended to use DataKinds
      to refer to the data constructor of that name?

:kind は型を指定してカインドを得るコマンドのため、値である True を指定すると当然エラーになります。

今度は DataKinds を指定した状態で実行してみます。

ghci> :set -XDataKinds
ghci> :kind True
True :: Bool

今度はエラーにならず、True が型として認識され、そのカインドが Bool になっていることが確認できました。カインドの節で挙げたイメージに沿って書けば、

True :: Bool :: *
     :: True :: Bool

という構成になっているのがわかります。これで依存型への第一歩を踏み出すことができました。

なお、DataKinds で値を型に昇格した場合、その型にはコンストラクタの先頭に ' が付与された名前が与えられます。従って、型に昇格された True は 'True という名前になります。しかし、この ' は特に混乱がない限り省略することが可能なため、上記ではエラーにならずに済んでいます。

'True を指定した場合の出力も確かめてみましょう。

ghci> :set -XDataKinds
ghci> :kind 'True
'True :: Bool

ちゃんと 'True という名前が型として認識されていますね。

記述の簡単のため、以降に示す GHCI の実行例では暗黙的に DataKinds を利用することとします。

KindSignatures

DataKinds によって型がカインドに昇格しましたが、これらのカインドは型引数に対して明示的に指定することができます。ただし、カインドの指定には KindSignatures という言語拡張が必要です。

カインドの指定には通常の型注釈と同様に :: を使用します。例として Bool カインドの型引数をとる型コンストラクタ SomethingBool を定義してみます。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data SomethingBool (a :: Bool)

ghci> :kind SomethingBool
SomethingBool :: Bool -> *

型引数 a に Bool カインドを指定したことで、a は True と False 以外の型を受け付けないようになっています。実際に確認してみましょう。

ghci> :kind SomethingBool True
SomethingBool True :: *
ghci> :kind SomethingBool False
SomethingBool False :: *
ghci> :kind SomethingBool Bool

<interactive>:1:15: error: [GHC-83865]
    • Expected kind ‘Bool’, but ‘Bool’ has kind ‘*’
    • In the first argument of ‘SomethingBool’, namely ‘Bool’
      In the type ‘SomethingBool Bool’

ちゃんと想定通りの動作になっていますね。

TypeOperators

DataKinds によって値が型に昇格したため、現時点で数値リテラルも型として扱うことができます。

ghci> :kind 1
1 :: GHC.Num.Natural.Natural

数値リテラルは Natural というカインドに属することがわかります。

数値リテラルが扱えるとなると + をはじめとする算術演算子も扱いたくなりますが、実際に試してみるとコンパイルエラーが発生します。例えば、以下の型エイリアスの宣言はエラーになります。

{-# LANGUAGE DataKinds #-}
type Two = 1 + 1

エラーの原因は２つあります：

Prelude に型レベルの算術演算子の定義が含まれていない
Haskell の標準機能では型レベルの演算子の利用が許可されていない

前者は純粋にパッケージ不足による問題です。型レベルの算術演算子は GHC.TypeNats に含まれているため、こちらをインポートすれば解消されます。^[1]

後者は言語拡張の不足による問題です。型レベルでの演算子の定義と利用を行うには TypeOperators という言語拡張を導入する必要があります。こちらは導入するだけで有効になる機能で、特別な構文等によるプログラムの書き換えは必要ありません。

これらを導入する形で修正した定義が以下になります。こちらはちゃんとコンパイルできます。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeNats

type Two = 1 + 1

ちなみに TypeNats には Natural のエイリアスである Nat の宣言も含まれています。名前が短くて便利なので、以降、数値リテラルのカインドの宣言には Nat を利用します。

GADTs

課題の洗い出しのため、ここまでの知識でどの程度 Idris の Vect の真似ができるかを試してみます。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeNats

data Vect (n :: Nat) a
    = Nil
    | Cons a (Vect (n - 1) a)

上記の定義で Vect 3 Int のような型を作ることが可能になります。少なくとも外観上はそれっぽくなっていますね。

上記の定義の問題点は Nil に対して任意の n を与えることが可能な点です。例えば以下のような用法が許されてしまいます。

Nil :: Vect 1 Int
Nil :: Vect 2 Int
Nil :: Vect 3 Int

n が要素数であり、かつ Nil が空の状態を表すならば、Nil の型は Vect 0 a に限定されるべきです。しかし、Haskell の data 構文は全てのコンストラクタを定義の左辺で宣言された型として扱う仕様のため、Nil に対して独立した型を与えることはできません。

一応、以下のようなラッパー関数を提供することで、この問題は回避可能です。

nil :: Vect 0 a
nil = Nil

しかし、コンストラクタ Nil を直接使用せずにラッパー関数 nil を使用するというお作法をプログラマが自身の注意力によって守らなければならないという問題は残ってしまいます。やはり各コンストラクタに対して個別に型宣言を行う手段が欲しいところです。

この問題をうまく解消してくれるのが GADTs という言語拡張です。GADTs を使用すると、まさに各コンストラクタに対して個別に型宣言を行うことが可能になります。

GADTs を用いて定義した Vect は以下のようになります。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
import GHC.TypeNats

data Vect (n :: Nat) a where
    Nil :: Vect 0 a
    Cons :: a -> Vect n a -> Vect (n + 1) a

GADTs では data の宣言の後に where を続け、さらに各コンストラクタの型の定義が続きます。Cons の型の可視性も上がって、非常によい感じですね。

この定義では Nil に対する先ほどのような用法は許されません。

ghci> Nil :: Vect 1 Int

<interactive>:7:1: error: [GHC-83865]
    • Couldn't match type ‘0’ with ‘1’
      Expected: Vect 1 Int
        Actual: Vect 0 Int
    • In the expression: Nil :: Vect 1 Int
      In an equation for ‘it’: it = Nil :: Vect 1 Int

実は先ほどの定義がこの章の冒頭で示した Vect の定義の完全版です。やったね。

`Vect` のための `length` を書く

Vect の定義は用意できたので、ここから関数ユーティリティを書いていきます。最初は Vect の要素数を返す関数 length から始めます。

ナイーブに実装すると以下のような感じですね。

import Prelude hiding (length)
import GHC.TypeNats

length :: Vect n a -> Nat
length Nil = 0
length (Cons _ v) = 1 + length v

リストの場合と同じ方法で定義しています。動作確認もしておきましょう。

ghci> Vect.length Nil
0
ghci> Vect.length $ Cons True Nil
1
ghci> Vect.length $ Cons True $ Cons True Nil
2

簡単でしたね。

と、ここで終わってもよいのですが、せっかく型に n という要素数を表す情報があるのに、わざわざ再帰で要素数を計算するのは、少し残念な実装という感じがします。

実は TypeNats には natVal という Nat カインドの型情報から値を得るための関数が用意してあり、そちらを利用することで再帰が不要になります。

natVal の型注釈は以下のようになっています。

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural

なんかごちゃごちゃしているので、以下の項で１つずつ読み解いていきます。

ExplicitForAll

まずは冒頭の forall から始めます。これは型宣言の中に登場する型変数を明示的に宣言するための記法と考えてもらえば大丈夫です。

例えば以下のような関数の型を考えてみます。

id :: a -> a

普段よく見かける型注釈ですね。上記のように、Haskell では型注釈上の小文字から始まる名前の対象は暗黙的に型変数として扱われるため、通常、我々が明示的に型変数を宣言することはありません。

しかし ExplicitForAll という言語拡張を使用すれば、forall キーワードを利用して、明示的に型変数を宣言することができます。以下は上記のものと全く同等な型注釈になります。

{-# LANGUAGE ExplicitForAll #-}
id :: forall a. a -> a

半角空白区切りで指定することで複数の型変数を宣言することもできます。

zip :: forall a b. [a] -> [b] -> [(a, b)]

なぜ暗黙的に解釈されるものをわざわざ明示的に宣言するのかというと、カインドの指定を明示的に行う際などに必要になるためで、つまり記法上の都合です。例えば natVal の定義では n に Nat カインドを指定するために forall が利用されています。

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural

他にも型注釈中で使用した型変数を関数本体に持ち込む際などにも利用しますが、こちらについては後ほど詳述します。

Proxy

natVal の型注釈を再掲します。

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural

proxy という型変数が登場しますが、これは Proxy という型を意識して書かれている型変数です。そのため、通常の Proxy の役割が理解できれば、自ずと proxy という型変数の役割も理解できます。

Data.Proxy では Proxy について以下のように書かれています。

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

要約すると、Proxy は値としては意味を持たず、型ないしカインドの情報を運ぶために使用されるという旨が書いてあります。

Proxy の実際の定義は以下のようになっています。

data Proxy t = Proxy

何のこっちゃという感じですが、実際の用法を見ればすぐにわかります。

以下のように定義された asProxyTypeOf' について考えてみます。

import Data.Proxy

asProxyTypeOf' :: a -> Proxy a -> a
asProxyTypeOf' x _ = x

asProxyTypeOf' は x を Proxy で指定した型で返します。以下のように使います。

ghci> import Data.Proxy
ghci> asProxyTypeOf' 123 (Proxy :: Proxy Int)
123
ghci> asProxyTypeOf' 123 (Proxy :: Proxy Double)
123.0

asProxyTypeOf' の型引数 a が Proxy の型注釈の内容で固定され、結果として返却される値の型が確定する、という仕組みです。実際の型も確認してみましょう。

ghci> :type asProxyTypeOf' 123 (Proxy :: Proxy Int)
asProxyTypeOf' 123 (Proxy :: Proxy Int) :: Int
ghci> :type asProxyTypeOf' 123 (Proxy :: Proxy Double)
asProxyTypeOf' 123 (Proxy :: Proxy Double) :: Double

戻り値の型がちゃんと指定した型になっていますね。

上述の通り、Proxy は型引数を使って型の情報を関数に渡しますが、この仕組みの本質は型引数を使ったテクニックに過ぎず、型引数を取る型であれば Proxy 以外の型でも同じことが可能です。

つまりasProxyTypeOf' で Proxy a としていた型注釈から一段階抽象化を進めて、型注釈を proxy a とすることができます。実際、この抽象化を施した asProxyTypeOf が Data.Proxy には定義されています。

例として Maybe を使って asProxyTypeOf を利用してみます。

ghci> asProxyTypeOf 123 (Nothing :: Maybe Int)
123
ghci> asProxyTypeOf 123 (Nothing :: Maybe Double)
123.0

戻り値の型も確認しておきます。

ghci> :type asProxyTypeOf 123 (Nothing :: Maybe Int)
asProxyTypeOf 123 (Nothing :: Maybe Int) :: Int
ghci> :type asProxyTypeOf 123 (Nothing :: Maybe Double)
asProxyTypeOf 123 (Nothing :: Maybe Double) :: Double

想定通りの動作ですね。これで natVal の proxy n についても理解できました。

KnownNat

natVal の型注釈を再掲します。

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural

ここまでの内容から、あとは KnownNat についてわかれば利用方法が理解できそうです。

KnownNat については TypeNats のドキュメントに以下のように書かれています。

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

数値リテラルに対応する型クラスというほどの意味合いのようです。Nat カインドの型を Proxy 経由で与えれば、自然に KnownNat の条件は満たすことができそうです。これで値が取得できそうですね。

早速 GHCI で試してみます。

ghci> import Data.Proxy
ghci> import GHC.TypeNats
ghci> natVal (Proxy :: Proxy 1)
1
ghci> natVal (Proxy :: Proxy 10)
10
ghci> natVal (Proxy :: Proxy 100)
100

これを使って Vect のための length を定義していきます。

ScopedTypeVariables

natVal を使って length を定義しようとすると、以下の定義が含む問題にぶつかります。

length :: KnownNat n => Vect n a -> Nat
length _ = natVal (Proxy :: Proxy n)

上記の定義はコンパイルエラーになります。

/path/to/src/Vect.hs:XX:20: error: [GHC-18872]
    • Couldn't match kind ‘*’ with ‘Natural’
      When matching types
        proxy0 :: Nat -> *
        Proxy :: * -> *
      Expected: proxy0 n1
        Actual: Proxy n0
    • In the first argument of ‘natVal’, namely ‘(Proxy :: Proxy n)’
      In the expression: natVal (Proxy :: Proxy n)
      In an equation for ‘length’: length _ = natVal (Proxy :: Proxy n)
   |
XX | length _ = natVal (Proxy :: Proxy n)
   |                    ^^^^^^^^^^^^^^^^

エラーが示す内容からは微妙にわかりづらいのですが、このエラーの本質的な原因は関数本体で参照されている型変数 n にあります。というのは、Haskell では型注釈と関数定義が分離しているため、型注釈で使用した型変数を関数定義で参照することができないのです。

これを解決するには ScopedTypeVariables という言語拡張を使用します。ScopedTypeVariables を導入することで、forall で明示的に指定した型変数を関数本体でも参照することが可能になります。なお、forall の利用が前提となっているため、ScopedTypeVariables を有効にすると ExplicitForAll も自動的に有効になります。

ScopedTypeVariables を使って length の定義を修正したものが以下になります。

{-# LANGUAGE ScopedTypeVariables #-}
import GHC.TypeNats
import Data.Proxy

length :: forall n a. KnownNat n => Vect n a -> Nat
length _ = natVal (Proxy :: Proxy n)

型変数 n が関数本体から参照可能になったため、こちらの定義は問題なくコンパイルできます。

早速 GHCI で試してみます。

ghci> length Nil
0
ghci> length $ Cons True Nil
1
ghci> length $ Cons True $ Cons True Nil
2

動作の方も問題なさそうですね。

`Vect` のための `head` を書く

続いて head を書いていきます。

head を書く際の一番の関心事は Nil の扱いでしょう。当然ですが、引数に Nil が指定された場合はコンパイルエラーとなるように設計する必要があります。

普段のノリで Nil か Cons かをパターンマッチングで判定したくなりますが、関数定義におけるパターンマッチングは値レベルの機能のため、それに頼った時点で Nil をコンパイルエラーで排除することが不可能になってしまいます。従って、今回はパターンマッチングではなく、型レベルの情報を使って head の定義から Nil を排除する必要があります。

`<=`

TypeNats には Nat カインドの型の大小関係を表す型制約を生成するための <= という演算子が定義されています。これを使えば型レベルで Nil の可能性を排除できます。蛇足ですが、定義されているのは <= のみで、< や >= などは定義されていないのでご注意ください。

<= の実際の用法を見てみましょう。

{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
import GHC.TypeNats

head :: (1 <= n) => Vect n a -> a
head (Cons x _) = x

型注釈の冒頭に 1 <= n という型制約が付与されています。これにより n が 1 以上の時にしかこの関数は呼ぶことができなくなり、n が 0 になり得る状況でこの関数を使用した場合はコンパイルエラーが発生します。従って、もはや head の引数に Nil を指定することは不可能になります。

なお、GHC は 1 <= n と関数の安全性の間の関係を理解できず、1 <= n が無用な型制約であると見なして警告を出力してくるので、コード冒頭に警告抑制のためのオプションを指定しています。

定義した head を GHCI で試してみます。

ghci> head $ Cons True Nil
True
ghci> head $ Cons False Nil
False
ghci> head Nil

<interactive>:20:1: error: [GHC-64725]
    • Cannot satisfy: 1 <= 0
    • In the expression: head Nil
      In an equation for ‘it’: it = head Nil

Nil を指定した場合にコンパイルエラーとなっていることがわかります。良い感じですね。

`Vect` のための `tail` を書く

head の対になる tail を書いていきます。

リストの tail は空リストを渡された場合に空リストを返すという仕様になっていますが、Vect の場合はそうはいきません。これは tail の型を考えてみるとわかります。

tail は Vect の先頭の要素以外の要素全てを返す関数です。従って、戻り値の Vect は元のものよりも要素数が１つ少ない状態になります。これをナイーブに型注釈で表現すると以下のようになります。

tail :: Vect n a -> Vect (n - 1) a

この型注釈から Nil を渡された場合に Nil を返すことが不可能であることがわかります。Nil を渡すと n が 0 になるため、戻り値として負の要素数を持つ Vect を返さなければならなくなってしまいます。当然ですが、そのような Vect は作成できません。

従って、ここでは Nil を引き受けることを諦めて、

tail :: (1 <= n) => Vect n a -> Vect (n - 1) a

とする方が合理的です。

次項で関数本体を実装していきます。

`GHC.TypeLits.Normalise`

tail の関数本体を実装します。

{-# LANGUAGE TypeOperators #-}
import GHC.TypeNats

tail :: (1 <= n) => Vect n a -> Vect (n - 1) a
tail (Cons _ xs) = xs

簡単でしたね。ガハハ。

と言いたいところですが、上記の定義はコンパイルエラーになります。エラーの内容は以下の通りです。

/path/to/src/Vect.hs:XX:20: error: [GHC-25897]
    • Could not deduce ‘(n - 1) ~ n1’
      from the context: 1 <= n
        bound by the type signature for:
                   Vect.tail :: forall (n :: Natural) a.
                                (1 <= n) =>
                                Vect n a -> Vect (n - 1) a
        at src/Vect.hs:XX:1-46
      or from: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   Cons :: forall a (n :: Natural). a -> Vect n a -> Vect (n + 1) a,
                 in an equation for ‘tail’
        at src/Vect.hs:XX:7-15
      Expected: Vect (n - 1) a
        Actual: Vect n1 a
      ‘n1’ is a rigid type variable bound by
        a pattern with constructor:
          Cons :: forall a (n :: Natural). a -> Vect n a -> Vect (n + 1) a,
        in an equation for ‘tail’
        at src/Vect.hs:XX:7-15
    • In the expression: xs
      In an equation for ‘Vect.tail’: Vect.tail (Cons _ xs) = xs
    • Relevant bindings include
        xs :: Vect n1 a (bound at src/Vect.hs:XX:14)
        tail :: Vect n a -> Vect (n - 1) a (bound at src/Vect.hs:XX:1)
   |
XX | tail (Cons _ xs) = xs
   |                    ^^

長いエラーですが、要約すると、戻り値に使われている xs の要素数が n - 1 であることが推論できない旨が書いてあります。人の目には Cons の定義から xs の要素数が n - 1 であることは明らかなのですが、GHC からすると Cons はあくまで Vect n a から Vect (n + 1) a を生成するという情報しか持たないため、この前提から n - 1 を推論することはできないということのようです。

これが依存型の難しいポイントで、基本的に GHC は型に昇格した値が元々持っている常識的な性質を演繹できないため、人間にとっては自明に思える事柄に対してエラーを発してくることがしばしばあります。

例えば、以下の定義はコンパイルエラーになります。

{-# LANGUAGE TypeOperators #-}
import GHC.TypeNats

id' :: Vect n a -> Vect (n + 1 - 1) a
id' Nil = Nil
id' (Cons x xs) = Cons x xs

これは n + 1 - 1 という型が n に等しいということが GHC にとって明らかでないことによって生じる問題です。実際のところ、GHC にとっての n + 1 - 1 は、+ という型コンストラクタに n と 1 を適用して得た型 n + 1 に対して、さらに - という型コンストラクタを 1 と共に適用して得た型というだけに過ぎません。その型を代数式として見た時に n に一致するというのは数学的な性質の話であって、その演繹をコンパイラが行ってくれるかどうかとは別の問題になります。

幸いなことに、GHC にはこの演繹を行ってくれるようにするための GHC.TypeLits.Normalise というプラグインが用意されています。これを使うと、型で表現された代数式を正規化して同等かどうかを判定してくれるようになります。

GHC.TypeLits.Normalise を利用するには依存関係の追加が必要です。

package.yaml

dependencies:
- base >= 4.7 && < 5
- ghc-typelits-natnormalise

あとはプログラム側で以下のようにプラグインの使用を明示すれば OK です。

{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
import GHC.TypeNats

id' :: Vect n a -> Vect (n + 1 - 1) a
id' Nil = Nil
id' (Cons x xs) = Cons x xs

GHC.TypeLits.Normalise では代数式を正規化してくれるため、もはや n と n + 1 - 1 が等しいことは GHC に検証可能な事柄になりました。従って、上記の id' はコンパイル可能です。

実は GHC.TypeLits.Normalise の導入によって tail で発生していた問題も解消可能です。実際に試してみましょう。

{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
import GHC.TypeNats

tail :: (1 <= n) => Vect n a -> Vect (n - 1) a
tail (Cons _ xs) = xs

上記はコンパイル可能です。GHC.TypeLits.Normalise の謎の作用により Cons の定義から xs の戻り値が n - 1 であることも推論できるようです。GHC.TypeLits.Normalise　についてはよくわかっていない部分も多いのですが、調べ出すと少し長くなりそうだったので、別の機会に詳しく扱おうと思います。

`Vect` のための `concat` を書く

リストの concat はリストのリストを受け取って、それらを１つのリストにまとめる関数でした。

ghci> concat [[1, 2], [3, 4], [5, 6]] :: [Integer]
[1,2,3,4,5,6]

これの Vect 版を実装します。型は以下のようになりそうです。

{-# LANGUAGE TypeOperators #-}
import GHC.TypeNats

concat :: Vect n (Vect m a) -> Vect (n * m) a

一見何の問題もなさそうですが、これはコンパイルエラーを誘発します。これは型に現れる演算子 * とカインドの * を GHC が混同してしまうために発生します。実際のエラーは以下の通りです。

/path/to/src/Vect.hs:XX:38: error: [GHC-83865]
    • Expected kind ‘* -> Nat -> Nat’, but ‘n’ has kind ‘Natural’
    • In the first argument of ‘Vect’, namely ‘(n (*) m)’
      In the type signature:
        concat :: Vect n (Vect m a) -> Vect (n (*) m) a
   |
XX | concat :: Vect n (Vect m a) -> Vect (n * m) a
   |                                      ^^^^^

GHC が n * m を n という型レベルの関数への * と m の適用と判断しています。これにより n が Nat と * -> Nat -> Nat という２つのカインドを前提した状態になり、矛盾が生じた旨が出力されています。

NoStarIsType

このような問題を避けるために GHC には NoStarIsType という言語拡張が用意されています。読んで字の如く、NoStarIsType ではカインドの指定に使用される * を廃止し、代わりに Type を使用するようになります。

GHCI で確認してみます。

ghci> :set -XNoStarIsType
ghci> :kind Int
Int :: Type
ghci> :kind Maybe
Maybe :: Type -> Type

これまで * や * -> * で表現されていたカインドが Type や Type -> Type に変わっていることがわかります。

NoStarIsType により以下の型注釈は問題なくコンパイルできるようになります。

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
import GHC.TypeNats

concat :: Vect n (Vect m a) -> Vect (n * m) a

というわけで、あとは実装していくだけですね。

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
import Prelude hiding ((++), concat)
import GHC.TypeNats

(++) :: Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil v = v
(++) (Cons x xs) v = Cons x $ xs ++ v

concat :: Vect n (Vect m a) -> Vect (n * m) a
concat Nil = Nil
concat (Cons Nil _) = Nil
concat (Cons xs ys) = xs ++ concat ys

ついでに (++) も実装できてハッピー（？）ですね。

この記事で紹介した知識ではできないこと

ここまでに紹介した知識だけでもそれなりのことができます。以下に挙げる Data.List の関数群の Vect 版は現時点の知識で実装可能です。

last
init
uncons
unsnoc
singleton
null
map
reverse
intersperse
intercalate
transpose
foldl
foldl1
foldr
foldr1
...

上で紹介したのは実装可能な関数の一部で、実際にはもっと実装可能です。

ここまでくると「もはや何でもできるのでは？」という気持ちになってきますが、無論、そんなことはありません。できないことの例として replicate の実装を試みてみましょう。

{-# LANGUAGE ScopedTypeVariables #-}
import GHC.TypeNats
import Data.Proxy

replicate :: forall a n. Proxy n -> a -> Vect n a
replicate p x = case natVal p of
    0 -> Nil
    _ -> Cons x $ replicate (Proxy :: Proxy (n - 1)) x

表面上はそれっぽく見えなくもないですが、上記はコンパイルエラーになります。

/path/to/src/Vect.hs:XX:10: error: [GHC-25897]
    • Couldn't match type ‘n’ with ‘0’
      Expected: Vect n a
        Actual: Vect 0 a
      ‘n’ is a rigid type variable bound by
        the type signature for:
          replicate :: forall a (n :: Nat). Proxy n -> a -> Vect n a
        at src/Vect.hs:XX:1-49
    • In the expression: Nil
      In a case alternative: 0 -> Nil
      In the expression:
        case natVal p of
          0 -> Nil
          _ -> Cons x $ replicate (Proxy :: Proxy (n - 1)) x
    • Relevant bindings include
        p :: Proxy n (bound at src/Vect.hs:XX:11)
        replicate :: Proxy n -> a -> Vect n a (bound at src/Vect.hs:XX:1)
   |
XX |     0 -> Nil
   |          ^^^

上記の定義では natVal p で得た値が 0 の場合に Nil を返していますが、これがエラーになっています。要求されている型はあくまで Vect n a であって Vect 0 a ではない、というのが GHC の主張です。

natVal で得た値が 0 なのに n が 0 と見なされないのは不思議に思えますが、これは natVal で得た値と n の間の関係性を GHC が知らないことによって生じます。natVal が行うのはあくまで値レベルの処理であり、型レベル変数 n に対して影響を及ぼすことはありません。型レベル変数 n に対して情報を付与するには、やはり型レベルの情報が必要になります。

ここで必要になってくるのが証明です。証明とは a :~: b のような形の型のことで、a と b が型システムの規則上同等であることを表します。これにより、例えば n :~: 0 という証明を構築できれば n と 0 が等しいということを GHC に伝えることができます。

証明を扱う実際の関数の例として TypeNats の sameNat という関数の型注釈を見てみます。

sameNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

sameNat は２つの Proxy を受け取り、それらが持つ Nat の値が等しいかどうかを判定します。値が等しい場合には証明を提供してくれます。

sameNat を使って replicate を書いてみます。

import GHC.TypeNats
import Data.Proxy
import Data.Type.Equality

replicate :: forall a n. KnownNat n => Proxy n -> a -> Vect n a
replicate p x = case sameNat p (Proxy :: Proxy 0) of
    Just Refl -> Nil
    Nothing   -> undefined

上記はコンパイル可能です。ただし、さしあたり先ほど発生していたエラーが解消しているかどうかを確認したいので、sameNat が Nothing を返した場合については、一旦 undefined としています。

Just によって Refl という値が返されていますが、これが証明の値です。この値が与えられた時点で型システムは n :~: 0 が成り立つことを認識するようになります。これにより、この分岐で Nil を返すことが可能になります。

実は Nothing が返された場合も実装しようとすると、また別の証明が必要になってきて色々大変です。この例が示す通り、依存型を扱うにはしばしば証明が必要になります。しかし、この記事の重心はあくまで Haskell で依存型を扱うための言語拡張の知識にあるので、ここでは証明の細かい話は扱いません。

証明についてはまた別の記事に書こうと思います。

参考文献

脚注

TypeNats と似たパッケージに GHC.TypeLits がありますが、歴史的には TypeNats の方が新しく、中身を見る限り TypeLits の改良版のような立ち位置のようです。natVal の戻り値が Integer から Natural に変更されるなどの細かな修正が加えられており、あえて TypeLits を使うメリットは特になさそうなため、この記事では TypeNats を利用します。 ↩︎

承前