LoginSignup
14
4

More than 3 years have passed since last update.

@mod_poppo

リテラルにTypeApplicationsを使えない理由とその対策、あるいはTypeApplicationsの注意点

Last updated at Posted at 2020-04-25

最近のGHCにはTypeApplicationsという拡張があります。これを使うと show @Int 42 というふうに多相関数の型を明示的に指定できます（型適用）。

ところで、Haskellの数値リテラルや、OverloadedStrings拡張下での文字列リテラルはオーバーロードされた型を持ちます。オーバーロードは便利ですが、状況によっては型が曖昧となってしまいます。

曖昧さを解決するには、型を明示すれば良いですね。しかし、通常の型注釈で 42 :: Int とは書けても、型適用を使って 42 @Int とは書けません。

通常の型注釈 :: には、優先順位が低いという問題があります。そのため、例えば「xの3乗」を型の曖昧さを排除して書こうとしたら x ^ (3 :: Int) となってしまいます。

型適用は結合の優先順位が高いので、型適用が使えれば x ^ 3 @Int と書けそうなものですが、残念ながらそれはできません。

どうしてもカッコを書きたくない場合は id を使って id @Int 3 と書くこともできますが、タイプ数が増えてしまいます。

この記事では、TypeApplicationsについて解説し、なぜリテラルに型適用できないかを説明します。そして、適切に状況を設定すればリテラルにも型適用を使えるようになることを見ていきます。

TypeApplicationsの挙動

まずは多相関数の型注釈について確認し、それがTypeApplicationsとどう関わるか見ていきます。

多相関数と型注釈

Haskellでは

bar :: a -> b -> (a, b)
bar x y = (x, y)

という風な型変数を含む関数を書くと、 a と b は暗黙に全称量化されます。つまり、 bar は a と b に任意の型を当てはめられる、多相的な関数となります。

同じ関数を型注釈を使わずに

foo x y = (x, y)

と書いても、型推論により最も一般的な型である a -> b -> (a, b) が推論されます。

さて、 ExplicitForAll 拡張を使うと、 forall キーワードを使って型変数を明示的に全称量化できます。

bar :: forall a b. a -> b -> (a, b)

型変数の順番を変えて、次のようにしても良いでしょう。

bar' :: forall b a. a -> b -> (a, b)

一方、 RankNTypes 拡張を使うと、関数の型の途中に forall を書くことができるようになります。

baz :: forall a. a -> forall b. b -> (a, b)

通常のHaskellでは、 foo と bar, それに bar' と baz のいずれも全く同じように振舞います。実際、 apply :: (forall a b. a -> b -> (a, b)) -> (Int, Double) という関数には foo, bar, bar', baz のいずれも渡すことができます。

例：

{-# LANGUAGE RankNTypes #-}

-- Inferred type: a -> b -> (a, b)
foo x y = (x, y)

-- Rank-1 type (ExplicitForAll)
bar :: forall a b. a -> b -> (a, b)
bar x y = (x, y)

-- Rank-1 type (ExplicitForAll)
bar' :: forall b a. a -> b -> (a, b)
bar' x y = (x, y)

-- Rank-1 type (requires RankNTypes)
baz :: forall a. a -> forall b. b -> (a, b)
baz x y = (x, y)

-- Rank-2 type (requires RankNTypes)
apply :: (forall b. Int -> b -> (Int, b)) -> (Int, Double)
apply f = f 42 3.14

-- Rank-2 type (requires RankNTypes)
apply' :: (Int -> forall b. b -> (Int, b)) -> (Int, Double)
apply' f = f 42 3.14

main = do
  print $ apply foo -- OK
  print $ apply bar -- OK
  print $ apply bar' -- OK
  print $ apply baz -- OK
  print $ apply' foo -- OK
  print $ apply' bar -- OK
  print $ apply' bar' -- OK
  print $ apply' baz -- OK

TypeApplications

先ほど「通常のHaskellでは、 foo と bar と bar' と baz は全く同じように振舞います。」と書きましたが、よく考えるとGHC拡張を使っている時点で「通常のHaskell」と呼べるかは怪しいですね。より正確にいうと、「TypeApplications拡張を使わないHaskellでは」というところでしょうか。

実は、TypeApplications拡張の下では、 foo と bar と bar' と baz に違いが生まれます。

先ほどのコードを次のように変えてみましょう：

{-# LANGUAGE TypeApplications #-}

...

main = do
  print $ foo @Int @Double 42 3.14
  print $ bar @Int @Double 42 3.14
  print $ bar' @Int @Double 42 3.14
  print $ baz @Int @Double 42 3.14

この中でコンパイルが通るのは bar @Int @Double だけで、残りの3つは型エラーとなります。

まず、 bar' :: forall b a. a -> b -> (a, b) に対して bar' @Int @Double が型エラーとなるのはなんとなく納得できますよね。型変数の順番的に b = Int, a = Double となるはずなので、 Int 型の引数に 3.14 を渡すことになってしまうのでエラーとなります。

一方、 foo は型注釈を書きませんでした。型注釈が書かれていない場合、型変数の順番は「曖昧」と判断され、型適用は使えません。推論された型に含まれる型変数の個数が1個でも同じです。

最後に、 baz ですが、値レベルの引数と型引数 (forall b.) の順番が一致していないと型適用は失敗します。

というわけで、TypeApplications以後のHaskellでは型注釈の有無や型引数の順番が重要となります。

GHCiでの確認方法

GHCiで「どの型変数に型適用できるのか」を確認するには、 :set -fprint-explicit-foralls を実行して :type +v （または :t +v）を使います。

通常の状態で型を確認しても違いはわかりませんが、

GHCi
*Main> :type foo
foo :: a -> b -> (a, b)
*Main> :type bar
bar :: a -> b -> (a, b)
*Main> :type bar'
bar' :: a -> b -> (a, b)
*Main> :type baz
baz :: a -> b -> (a, b)

:set -fprint-explicit-foralls を実行して :t +v を使うと「どの型変数にどの順番で型適用できるのか」がわかるようになります。具体的には、型適用できない型変数は波括弧で表示されます。

GHCi
*Main> :set -fprint-explicit-foralls 
*Main> :type +v foo
foo :: forall {a} {b}. a -> b -> (a, b)
*Main> :type +v bar
bar :: forall a b. a -> b -> (a, b)
*Main> :type +v bar'
bar' :: forall b a. a -> b -> (a, b)
*Main> :type +v baz
baz :: forall a. a -> forall b. b -> (a, b)

詳しくはGHC User's Guideを読んでください：

リテラルの脱糖

TypeApplicationsについて勉強したので、リテラルに型適用を使えない理由が説明できます。

まず、 42 というリテラルは fromInteger <Integer型の42> に脱糖されます。なので、 42 @Int と書くと fromInteger <Integer型の42> @Int と同じ意味になります。

42 @Int ~~(脱糖)~> fromInteger 42 @Int

これに対し、 fromInteger の型は forall a. Num a => Integer -> a なので、「値レベルの引数と型引数の順番が一致しない」ためにエラーとなる、というわけです。

-- fromInteger の型
fromInteger :: forall a. Num a => Integer -> a

42 @Int ~~(脱糖)~> fromInteger 42 @Int -- エラー！型引数の順番が違う
fromInteger @Int 42 -- これなら動く

ちなみにリテラルの型をGHCiで前述の方法で確認すると

GHCi
*Main> :type +v 42
42 :: forall {p}. Num p => p
*Main> :type +v 3.1415
3.1415 :: forall {p}. Fractional p => p

となって、型適用が使えないことがわかります。

リテラルにTypeApplicationsを使う方法

こうなると解決法も見えてきます。リテラルの脱糖に使われる fromInteger の型を fromInteger :: Integer -> forall a. Num a => a にすればリテラルに型適用できるはずです。

リテラルの脱糖に使われる fromInteger を自前のものに差し替えるには RebindableSyntax を使います。

というわけで、次のコードはコンパイルが通ります。

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE RankNTypes #-}
import Prelude hiding (fromInteger)
import qualified Prelude

fromInteger :: Integer -> forall a. Num a => a
fromInteger = Prelude.fromInteger

main :: IO ()
main = do
  let x = 123 @Integer -- リテラルに
  print (x ^ 2 @Int)   -- 型適用が
                       -- できている
                       -- (575)

ちなみに、GHC Proposalsには「リテラルにTypeApplicationsできるようにしようぜ！」という提案があったようなのですが、却下されています。

おまけ：TypeApplicationsの罠

TypeApplicationsについて説明したついでに、TypeApplicationsの罠っぽいものにも触れておきます。わざわざ別の記事を書くのが面倒なので…。

こういう「型名を表示する」関数があったとします：

{-# LANGUAGE ExplicitForAll #-}
import Data.Typeable

typeName :: forall a. Typeable a => Proxy a -> String
typeName proxy = show (typeRep proxy)

この typeName 関数は Type カインドにしか使えません。つまり、DataKinds下で typeName (Proxy :: Proxy 123) とするとコンパイルエラーとなります。

そこで、コードを次のように変えてみましょう：

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ExplicitForAll #-}
import Data.Typeable

typeName :: forall a. Typeable a => Proxy a -> String
typeName proxy = show (typeRep proxy)

typeName' :: forall (a :: k). Typeable a => Proxy a -> String
typeName' proxy = show (typeRep proxy)

新しく作った typeName' にはDataKinds下で typeName' (Proxy :: Proxy 123) とすることができます。

実はこの場合はカインド注釈を書かなくてもPolyKindsのおかげで元の typeName の a のカインドも一般化されます。

さて、 typeName と typeName' はほとんど同等です。ですが、例によってTypeApplicationsの下では違いが生まれます。GHCiで確認してみましょう。

GHCi
*Main> :set -fprint-explicit-foralls 
*Main> :type +v typeName
typeName :: forall {k} (a :: k). Typeable a => Proxy a -> String
*Main> :type +v typeName'
typeName' :: forall k (a :: k). Typeable a => Proxy a -> String

元の typeName 関数はカインド変数 k が暗黙であり型適用できませんが、コード中に (a :: k) と書いた typeName' はカインド変数 k にも型適用できます。

教訓としては、「型や関数をカインド多相にしようとして迂闊にカインド変数を足すとTypeApplicationsを使ったコードが壊れる可能性があるぞ」ということです。

一般論として、関数の型を一般化するとTypeApplicationsを使ったコードは壊れがちです。筆者がハマった例としては、 sum 関数

sum :: Num a => [a] -> a

に sum @Int と型適用したところコンパイルエラーが起こりました。GHCの sum 関数の型がリストじゃなくて Foldable に一般化されているせいです。あ〜あ

筆者に言わせれば、型推論を前提に設計された言語に対するTypeApplicationsというのは異質な拡張なのです。したがって、TypeApplicationsの使用は最小限に控えるべきだと個人的には思っています。Proxy 引数を排するために AllowAmbiguousTypes と組み合わせるやつも個人的には好きではありません。便利で簡潔なのはわかるけどさ……。

筆者の感覚的に、TypeApplicationsを使っても良いかなと思えるのは、以下の状況です。

  • read 系（使えないと辛い）
  • Proxy（タイプ数節約のため）
  • 型クラスのメソッド
    • メソッドについた型注釈にかかわらず、型クラスの型が最初の型引数となります。
    • GNDみたいなことを手動でやりたくなった時に method = coerce (method @BaseType) と書くと楽です。
14
4
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
14
4