Haskell の型システム、その拡張メモ

Haskell でPolymorphism をふと調べてみたら、ちょっと面白いことを発見。

Haskell では、たとえば、リストの長さを返す関数を書くときに以下のように書く。

  length :: [a] -> Int

これは Polymorphic 函数で、a であらわされる型にはさまざまな異なる型が入る。こういう型を表す変数を型変数という。（ちなみにHaskellでは、型変数は常に小文字の文字で始まる文字列で表現され、具体的な型（例えば、Int や String）は常に大文字から始まる。）

しかし、Haskell には、この型変数がいかなる型にもなれるというのをより明示的に示す方法が用意されている。そしてそれは以下のとおりである。

 length :: forall a. [a] -> Int

これは、「すべての型 a に関して、この函数Length その型aの要素のリストを受け取り、Integerを返す」ということを示している。古い型署名はこの新しいものの省略気泡とみなすこともできるだろう。つまり、コンパイラは内部でこの書かれていないforallを自動的に挿入している。

これを実際にHaskell で試してみるには少し注意が必要。

この foall 記述を用いる場合は ghc 拡張（RankNTypes）を使う必要がある。そして、 ghc 拡張を使うには、コマンドオプションで指定する方法と、ソースコード内に記述する方法の2種類がある。

コマンドオプション

ghc コマンドや ghci コマンドに、-X拡張名というコマンドオプションを付ける。RankNTypes 格調を用いる場合は以下のとおり

ghc -XRankNTypes

ソースコード内に記述する方法

ソースコードの先頭行で、使用する拡張を指定する。ほとんどの場合こちらのほうがお勧め。記述によりこのファイルが要求していることが一目で分かるし、コンパイル時は ghc とだけ打てば済む。

-- hoge.hs
{-# LANGUAGE RankNTypes #-}

length :: forall a. [a] -> Int
length = undefined

以下は参考にしたページ

おまけ：このHaskellの明示的な型変数記述はAgdaではデフォルトになっている。Agda でlength函数は以下のように記述する。

module hoge where

open import Data.List
open import Data.Nat

postulate myLength : {A : Set} -> List A -> &#8469;

Haskell の forall a. が Agda では {A : Set} として表現されている。簡単に言うと一般に型は集合として表現されるのだが、AgdaでSetは型の型である。つまり、これにより A はany types（どんな型でも）を表現するのだ。とここまで書きつつ、多分これだけではわからないと思うから、興味のある方はAgdaを勉強してみてください。