[WIP] Haskellで型でカタカタ〜あんまりカタカタしない編〜

WIP Haskellで型でカタカタ〜あんまりカタカタしない編〜

突然ですが！いい感じに長さ付きベクトルを扱いたい！

例えば，行列とベクトルをかけるときに，次元の整合性がとれているかをコンパイル時に検査したいみたいな気持ちになることは5億回ある．以下GHC8.8.2

型を変える

コンパイル時に検査されるのは型なので，長さごとにベクトルの型を変えればよいのでは！という天才的な発想を思いついたので以下のようにした．

code: vec1.hs

newtype ZeroVector a = ZeroVector (Vector a)

newtype OneVector a = OneVector (Vector a)

newtype TwoVector a = TwoVector (Vector a)

...

流石にVector書きまくって大変なので改善しよう！

code: vec2.hs

newtype V n a = V (Vector a)

data Zero

data One

data Two

data Three

...

こうすると，例えばV Zero a とV One a の型は異なるので，長さによって各ベクトルを区別できるようになる．この時，n×mの行列はVを使ってV n (V m a) のように書ける．

では掛け算の実装をしてみよう．

code: vec3.hs

(*|) :: V n (V m a) -> V m a -> V n

xs *| ys = ...

実装の詳細は余談になるので省略する(おまけに書いとく)．これで型によって行列とベクトルの掛け算の次元の整合性が取れていることが，コンパイル時に検証できるようになった．完璧！これにて一見落着！

型レベル自然数を使う

前述の方法には実は致命的な弱点が存在する．使う自然数全部の型を用意する必要があるのだ．自分で使うだけなら使う自然数が増えるたびに奇声を上げながら自然数の型を追加するだけでよいが，ライブラリとして公開する場合はそうもいかない．依存型を使える場合，何も考えずにV に自然数を食わせることができるが，GHC 8.8現在，GHCはフルの依存型をサポートしていない．なんとか自然数の型を扱ううまい方法はないだろうか？

実はGHCは型レベル自然数をサポートしており，DataKinds 拡張を有効にすれば，型の部分に書いた数値リテラルが型レベル自然数として解釈される．この自然数は，当然型なので，1 と 2は異なる型であるから，V 1 aとV 2 a は異なるので，これらの次元の整合性をコンパイル時に検証できる．型レベル自然数の種はNat であり， Type ではないので，Vの定義を以下のように変更する必要がある．

code: vec4.hs

{-# LANGUAGE DataKinds, KindSignatures #-}

import Data.Kind (Type)

import GHC.TypeLits (Nat)

import qualified Data.Vector as V

newtype V (n :: Nat) (a :: Type) = V (V.Vector a)

なお，種注釈をするには KindSignatures 拡張を有効にする必要がある．これで無限に自然数の型を作らなくて良くなった．今度こそ完璧！

長さ付きベクトルへの変換

今度こそ完璧かと思いきやまだこのプログラムには問題が存在する．値コンストラクタであるVを使ってVの型を作ると，型レベルの次元の情報と食い違ったベクトルを作れてしまう．例えば，以下のコードは合法である．

code: vec5.hs

-- 4次元のベクトル(要素が4つあるとは言ってない)

xs :: V 4 Double

xs = V $ fromList 1

ということでスマートコンストラクタを用意する．

code: vec6.hs

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}

import GHC.TypeLits

import qualified Data.Vector as V

import Data.Proxy (Proxy(..))

fromVector :: forall n a. KnownNat n => Vector a -> Maybe (V n a)

fromVector v

| length v == fromIntegral (natVal (Proxy :: Proxy n)) = Just (V v)

| otherwise = Nothing

少しコードの解説をする．KnownNat はnatSing という型レベル自然数と一対一に対応するデータ型を返すメソッドを持つ型クラスであり，これを用いて型レベル自然数を値に引き戻すことができる．昇格した値コンストラクタと一対一に対応するデータ型をsingleton typeといい，これを用いて型レベルに昇格した値を値レベルに引き戻せるようにするのをsingletonパターン(not OOP)といったりする．natSing はそのままだと使いづらいので，たいてい，natValという関数を使ってInteger に引き戻すことになる．

natVal の引数である Proxy n は，型変数n を natVal に渡すためのものであり，このような，型を教えてやるような用途で使われる．Proxy 自体の定義は data Proxy t = Proxy であり，Proxy 型を受け取ることを想定しているnatValのような関数に渡すときに，Proxy :: Proxy n といったように型を明示して渡す．

ここで注意すべきは，型変数n の扱いである．このnは当然，fromVector の型シグネチャに現れるものと，Proxy :: Poxy n のもので同じになる必要があるが，通常，GHCはこれは別のものとして扱う．端的に言うと，型変数のスコープはシグネチャの部分で閉じている．この型変数のスコープをレキシカルスコープと同じようにする拡張が，ScopedTypeVariablesである．詳細はGHCドキュメント(古いものだが，翻訳はこのScrapboxにも存在する)を参照してほしいが，使い方はシグネチャの最初にforall a b c ... .といった形で使う型変数を列挙すればよい．vec7.hs では n と a があるため，forall n a.となっている．これで，Proxy の n と fromVector の n が同じものであることが保証される．

fromVector のおかげで，Vを使った場合と異なり，vectorの長さがVの次元と同じであれば，V 型の値が作られ，異なればNothing が変えるようになり，V の持つ不変条件が値の作成時にも守られるようになった．勝ったな風呂入ってくる．

長さわからんベクトルの扱い

WIP: 存在型を使うかRankNTypesを使っていい感じにする