型変数の比較

もっと簡単な例で追記しました

Haskellの型レでは型変数同士の比較ができないぜーというお話をしたんですが、OlegさんのReversing Haskell typechecker: converting from undefined to defined のTypeEqを試したらば、できちゃいました。

Haskell型レのバイブルであるHListの論文には、

So, TypeEq is total for ground types, and partial for unground types.

とか、

TypeEq cannot establish equality for ungrounded types;

とあるのでできないと思い込んでいたのだけど、その後のGHCの型検査器の変更でできるようになってしまった、ということなんだろうか？

GHC 6.6でもオッケーです。6.4は手元にないのでわからない(けど記事の日時からして多分できるんだろう)。

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-incoherent-instances #-}
{-# OPTIONS -fno-monomorphism-restriction #-} -- 無くしてみると…

-- GHC 6.8 or later
-- {-# LANGUAGE UndecidableInstances, OverlappingInstances, IncoherentInstances #-}
-- {-# LANGUAGE NoMonomorphismRestriction #-}

-- HList
data s :|: ss = s :|: ss
data Nil = Nil

infixr 7 :|:

-- 型変数を生成する
gen :: (a -> ss) -> ss
gen = undefined

-- 最初に見つけた型変数tを 型Helloに置き換える
data Hello
update :: Update t Hello ls ls' => t -> ls -> ls'
update = undefined

-- 次のリストの型変数 a1 を…
-- orig :: (Num t) => a :|: (Char :|: (t :|: (a1 :|: Nil))) 
orig = gen (\a -> gen (\b -> a :|: 'x' :|: 1 :|: b :|: Nil))

-- Helloに置き換える．
-- test :: (Num t) => a :|: (Char :|: (t :|: (Hello :|: Nil))) -- on GHC 6.8 or later
test = gen (\a -> gen (\b -> update b $ a :|: 'x' :|: 1 :|: b :|: Nil))


-- 型レ
class Update t t' ls ls' | t t' ls -> ls'
instance (TypeEq t l b, Update' b t t' (l:|:ls) ls') => Update t t' (l:|:ls) ls'

class Update' b t t' ls ls' | b t t' ls -> ls'
instance Update' HTrue t t' (l:|:ls) (t':|:ls)
instance Update t t' ls ls' => Update' HFalse t t' (l:|:ls) (l:|:ls')



-- from http://okmij.org/ftp/Haskell/types.html#de-typechecker

data HTrue 
data HFalse 

-- literally lifted from the HList library
class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x  = x


class TypeEq' () x y b => TypeEq x y b | x y -> b
    where type'eq :: x -> y -> b
          type'eq _ _ = undefined::b
class TypeEq' q x y b | q x y -> b
class TypeEq'' q x y b | q x y -> b
instance TypeEq' () x y b => TypeEq x y b
instance TypeCast b HTrue => TypeEq' () x x b
instance TypeEq'' q x y b => TypeEq' q x y b
instance TypeEq'' () x y HFalse