北海道苫小牧市出身の初老PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

式と型と値

JavaHaskellも静的型付けの言語だけど、Javaをやっている人とHaskellをやっている人で、「静的型付け」という言葉で頭に描くイメージはだいぶ違うと思う。

じゃあどう違うのかってのを説明すると小難しい話になりがちなのだけど、Haskell 2010 Language Reportにそれを簡潔に示したいい一文を見つけたので記しておく。

An expression evaluates to a value and has a static type. https://www.haskell.org/onlinereport/haskell2010/haskellch1.html#x6-120001.3

Haskellの式に対して、2つの操作が可能である。1つが式を評価して値を求めること。もう1つが、式を型付けして型を求めること。この観点に立つと、型を持っているのは値ではなく式である。そして、評価と型付けが互いに完全に独立した操作であるからこそ、型付けが一種のプログラムのバリデーションとして機能するのである*1。まったく別の操作であるはずの評価と型付けについて、きちんと互いに矛盾の起きない結果が得られるかどうかは、言語設計者の責任に委ねられる。例えば、評価して True となる式は、型付けすると Bool 型になるように評価と型付けが設計されていなければならない。

こういう話は型システム入門にしっかりと(しっかりすぎるほど)書かれている。

が、それをこの1文で簡潔に表しているのはいいなあと思う。Haskell 2010 Language ReportはHaskellの基本的な部分についてどういう仕様なのか、なぜそうなっているのか、きちんと書かれている原典なので、たまに読むと得られるものが多い。GHCの拡張がないとコードが書けないという人であればなおのこと。

*1:依存型が入ってくると互いに密接に関係するようになるけど