Scoped type variablesが必要になるとき
whereの中の局所定義に型シグネチャを付けると
Couldn't match type `a' with `a1' ...
といわれて型検査を通らない!という経験はありませんか?これを直すには字句的スコープを持つ型変数が必要です。この機能はScopedTypeVariablesという言語拡張によって有効になります。
局所定義された式に型シグネチャを付けられない
たとえばこんな単純な例を考えましょう。
rev :: [a] -> [a] rev xs = ys where ys = reverse xs
関数revは単にreverseの別名です。reverse xsの結果をwhereでysに束縛し、それを返しているだけです。このysの型はもちろん[a]な訳ですが、どういうわけか型シグネチャを書くと型検査で弾かれます。
rev :: [a] -> [a] rev xs = ys where ys :: [a] ys = reverse xs
こんなエラーメッセージに見覚えのある方もいるのではないでしょうか。
/Users/maoe/coding/haskell/ScopeTyVars.hs:5:18: Couldn't match type `a' with `a1' `a' is a rigid type variable bound by the type signature for rev :: [a] -> [a] at /Users/maoe/coding/haskell/ScopeTyVars.hs:2:1 `a1' is a rigid type variable bound by the type signature for ys :: [a1] at /Users/maoe/coding/haskell/ScopeTyVars.hs:5:5 Expected type: [a1] Actual type: [a] In the first argument of `reverse', namely `xs' In the expression: reverse xs
暗黙のforall
何故、型検査に失敗するのでしょうか。HaskellではHaskellの型シグネチャは暗黙に量化されます。つまり先の例はこのように型がつきます。
{-# LANGUAGE ExplicitForAll #-} rev :: forall a. [a] -> [a] rev xs = ys where ys :: forall a. [a] ys = reverse xs
revにもysにもforall a.がついていることがポイントです。forall a.のように量化された変数は、任意の変数に書き換えることができます(α変換)。つまりこういうことです。
rev :: forall a. [a] -> [a] rev xs = ys where ys :: forall b. [b] -- 全く別の型b ys = reverse xs
xsとysが全く別の型になってしまいました。上のエラーメッセージでExpected type: [a1]でActual type: [a]と出力されているのはこういうことです。
ScopedTypeVariablesで解決する
問題はysの型が量化されてしまうことでした。これを回避するためにScopedTypeVariablesという言語拡張があります。この拡張を有効にすると、型変数のスコープが字句通りになります。つまり、revの型シグネチャに使った型変数を局所定義された式のシグネチャでも使い回すことができるようになります。
{-# LANGUAGE ScopedTypeVariables #-} rev :: forall a. [a] -> [a] rev xs = ys where ys :: [a] ys = reverse xs
ScopedTypeVariablesが有効になるためには
- 言語拡張のプラグマを指定する
- forall a.を明示する
必要があります。これでysの型にはforall a.がつかなくなりました。
ScopedTypeVariablesが必要な例とasTypeOfを使った回避策
上の例では型を書かなくても問題ありませんでしたが、型を書かないと困る例もあります。
下のgistはBoundedなクラス制約がかかった型のminBoundsとmaxBoundsを文字列で返すという、少々恣意的な例です。この例ではminBoundsとmaxBoundsの型を指定しないと曖昧な型となり、型検査に失敗します。
また、bounds'はScoped type variables言語拡張を持たないコンパイラでの回避策です。Preludeに含まれるasTypeOfはこういうときに使えるんですね。
Monomorphic local bindingsの影響
GHC 7になって型推論エンジンが書き直された影響で、ローカルの束縛に型を書かないと型検査に失敗する例があります。詳細はBlog: Let generalisation in GHC 7.0 – GHCに書かれています。
例を抜粋したgistがこれです。
GADTsやTypeFamiliesを有効にするとMonoLocalBindsという拡張が有効になり、局所定義の推論される型が単相的になります。つまり、gの型シグネチャをコメントアウトすると、g 'v'とg Trueからgの型が
- g :: Char -> (a, Char)
- g :: Bool -> (a, Bool)
と二通りに解釈できるため、型検査に失敗します。
解決策は2つあって
- 型シグネチャを書く。この場合はScopedTypeVariablesを有効にする必要がある。
- NoMonoLocalBinds言語拡張を有効にする
というものです。基本的には型はよいドキュメントになるのでScopedTypeVariablesを使って型シグネチャを書くのがよいでしょう。
参考リンク
- Scoped type variables
- Monomorphic local bindings