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