GHC 7.0.2 RC1及び、GHC 6.12.3をもてあそぶコード

まずHaskellはSystem Fωをベースにして(厳密にはSystem FC http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/FC#Newtypesarecoercedtypes とからしいですが)いるので、型を取って型を返す関数を書く事が出来ます。

type Id a = a
type Pair a b = (a , b)
type X a = Pair a a

ただし、次のようなコードを書く事は出来ません。

type F x = x (F x)

    Cycle in type synonym declarations:
      blog.hs:1:1-18: type F x = x (F x)

結果からの話になってしまうのですが、System Fωでは型に対するリダクションの性質として強正規化性定理(正しくリダクションするならばどうリダクションしていっても正規形 つまりそれ以上リダクション出来ない形になる)を持っています。上記F x = x (F x)が定義出来てしまうとfixed point combinator的な意味を含めて嫌な予感がします。

もっと単純に

type Ty = Ty


    Cycle in type synonym declarations: blog.hs:1:1-12: type Ty = Ty

これもダメデス。

ではtype familiesを使ってTy相当を定義しなおしてみましょう。

{-# LANGUAGE TypeFamilies , UndecidableInstances , FlexibleContexts#-}

type family Ty :: *
type instance Ty = Ty

これは7.0.2 RC1でも6.12.3でも型チェックをパスします。実際にこれが定義出来ると強正規化定理が破れる例としては

{-# LANGUAGE TypeFamilies , UndecidableInstances , FlexibleContexts#-}
module NonTerminate where

type family Ty
type instance Ty = Ty

f :: (Ty ~ Int) => Ty
f _ = undefined

Ty ~ IntでTyで正規形を得る所までreductionしていくので、ここで止まらない筈です。(正規形が在れば1つに定まる事を利用してnormal form同士を比較するようにしている筈なので、多分Tyに関するreductionが起こるだろうとふんでこのコードを書きました。)

//6.12.3
/Users/ranha/Event/GHCCrash% ghc-6.12.3 -c blog.hs 
...(計算は終わらない)

//7.0.2 RC 1
    Context reduction stack overflow; size = 21
    Use -fcontext-stack=N to increase stack size to N

となり、6.12.3では論外で、7.0.2 RC1ではループが検出出来ていないのが嬉しく無いという話になります。保持すべき性質を破っているのでコレは良く無いなーという、そういう話でした。

参考 :
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/FC#Newtypesarecoercedtypes
http://www.doc.ic.ac.uk/~svb/CLaC06/Papers/df153893661da0e2531ef16d95e4.pdf
Type and Programming LanguagesのSystem Fωの所