type families と fundeps の、単一化に関する微妙な差異

Haskell

昨日の記事に関連するのだけど、 fundeps と type families で一見 同じように見えるが 微妙に異なる挙動を見つけた。ずいぶん込み入った例だけれど、さしあたりの理解のためにこの記事を書く。

ストーリー

例のごとく、私は full-sessionsにおいて 繰り返しを含むプロトコルを表現した型を表現するため、 Haskellで「見かけ上、構造的な再帰型」が欲しいのである(こういう表現が正しいかどうかわからないけれど…)。
例えば

data F u = F u
data G u = G u

という型があるとき、

x = F (G x)

と定義された x の型をうまくHaskellの型検査器に推論させたい。 もちろんHaskellでそんなことはできない *1が、例えばこれを

x = rec (F (G x))

のように、ちょっとした仕掛けを入れてやることで、

x :: Rec (F (G Var))

のように、「いかにも再帰型っぽい」型をHaskellに推論させたいのだ(簡単のため、相互再帰や二重再帰を考えないことにする)。ここで Rec (f Var) は なんとなく µx. f x という再帰型を表していると考えてほしい。 OCamlっぽく書くと ('a f as 'a) みたいな感じか。

追記：ここでは再帰型っぽく見えるようにする事しか考えていない。実際には x は Rec (F (G Var)) という再帰的でない構造のデータであることに注意．

関数依存(fundeps)を使う

これは関数依存で実現できる。

class RecFold u u' | u -> u'
instance RecFold u u' => RecFold (F u) (F u')
instance RecFold u u' => RecFold (G u) (G u')
instance RecFold (Rec u) Var

rec :: RecFold u u' => u -> Rec u'
rec = undefined

のように、Recに対してVar を割り当ててくれる型関数っぽいものを fundepsで作ればよい(undefinedを含まないバージョンは後で貼ります)。
これで十分にうまくいく。

*Main> :t x
x :: Rec (F (G Var))

型族 (type families) を使った方法 ()

最近の型レハッカーの間ではきっと type families が流行のはずなので、上のfundepsの実装をそのまま type families で実装してみた。

type family RecFoldT u :: *
type instance RecFoldT (F u) = F (RecFoldT u)
type instance RecFoldT (G u) = G (RecFoldT u)
type instance RecFoldT (Rec u) = Var

rec :: u -> Rec (RecFoldT u)
rec = undefined

やってることは fundepsのバージョンと同じだ。がしかし、これで x = rec (F (G x)) の型を調べると、次の型エラーが出る：

*Main> :t let x = rec (F (G x)) in x

<interactive>:1:4:
    Couldn't match expected type `u'
           against inferred type `Rec (RecFoldT (F (G u)))'
    In the expression: rec (F (G x))
    In the definition of `x': x = rec (F (G x))
    In the expression: let x = rec (F (G x)) in x

おわかりだろうか。

  • fundeps バージョンでは
    • 式の右辺に出現するxの型(これをuとしよう) と xの式全体から推論される型 RecFold u u' => Rec (F (G u')) がある。
      • u と Rec (F (G u')) を単一化することで context reduction が働き、 Rec (F (G Var)) という型が推論される
  • いっぽう type families バージョンでは、
    • xの型u と、xの右辺式全体の型 Rec (RecFoldT (F (G u))) を単一化して欲しいところだが、
      • この単一化が許可されていないのか 型エラーになっている。

考えたこと

  • これはエラーか？ コンパイラのバグか？ 未定義(または実装者に予想外)の挙動か？
    • エラーなら、どういう条件を破ったためエラーなのか？ その条件がないとどうなるのか？(停止しなくなる？)
    • バグなら報告
    • 未定義なら報告

コード

{-# LANGUAGE TypeOperators, KindSignatures, ScopedTypeVariables, EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

data F u = F u
data G u = G u
data Rec u = Rec u
data Var = Var

{-
-- エラーになる
class RecFold u where
  type RecFoldT u :: *
  recfold :: u -> RecFoldT u
instance RecFold u => RecFold (F u) where
  type RecFoldT (F u) = F (RecFoldT u)
  recfold (F u) = F (recfold u)
instance RecFold u => RecFold (G u) where
  type RecFoldT (G u) = G (RecFoldT u)
  recfold (G u) = G (recfold u)
instance RecFold (Rec u) where
  type RecFoldT (Rec u) = Var
  recfold (Rec _) = Var
-}

class RecFold u u' | u -> u' where
  recfold :: u -> u'
instance RecFold u u' => RecFold (F u) (F u') where
  recfold (F u) = F (recfold u)
instance RecFold u u' => RecFold (G u) (G u') where
  recfold (G u) = G (recfold u)
instance RecFold (Rec u) Var where
  recfold (Rec u) = Var

rec x = Rec (recfold x)

-- recursive structure
x = rec (F (G x))

*1:Occurs check: cannot construct the infinite type: u = F (G u) となる