3

Haskell で System-F スタイルのデータ構造を実装して実験しています。

型へA <B>の用語の適用を意味するために使用します(型には大文字も使用します)。AB

Tree <T>は type の値を持つ二分木の型だとしましょうT。として機能できるタイプを見つけたいと考えていますTree <T>。次の 3 つのコンストラクターがあります。

EmptyTree <T> : (Tree <T>)
Leaf <T> : T → (Tree <T>)
Branch <T> : (Tree <T>) → (Tree <T>) → (Tree <T>)

したがって、Girard のおかげで、次のように使用できると思います。

Tree T = ∀ A. A → (T → A) → (A → A → A) → A

そこから

Empty <T>
        = ΛA.λa:A.λf:(T → A).λg:(A → A → A).
            a

Leaf <T> (x:T)
        = ΛA.λa:A.λf:(T → A).λg:(A → A → A).
            f x

Branch <T> (t1:Tree <T>) (t2:Tree <T>)
        = ΛA.λa:A.λf:(T → A).λg:(A → A → A).
            g (t1 <A> a f g) (t2 <A> a f g)

Haskell でこれらのことを行うために必要なディレクティブを見つけました。欠落しているとは思いません。したがって、Haskell では次のようになります。

{-# LANGUAGE RankNTypes #-}
type T t = forall a.a -> (t -> a) -> (a -> a -> a) -> a

empty :: T t
empty = \a _ _ -> a
leaf :: t -> T t
leaf x = \_ f _ -> f x
fork :: T t -> T t -> T t
fork t1 t2 = \a f g -> g (t1 a f g) (t2 a f g)

これまでのところ、これはすべてコンパイルされ、機能しているようです。Show自分のT tタイプのインスタンスを作成しようとすると、問題が発生します。さらにディレクティブを追加しました:

{-# LANGUAGE RankNTypes, TypeSynonymInstances, FlexibleInstances #-}

およびツリーを印刷する関数

displayTree :: Show t => T t -> String
displayTree t = t displayEmpty show displayFork

適切なヘルパーdisplayEmpty :: StringとdisplayFork :: String -> String -> String. これもコンパイルして動作します（かわいらしさまで）。T tのインスタンスとしてインスタンス化しようとするとShow

instance Show t => Show (T t) where
    show = displayTree

コンパイルしようとすると、次のエラーが発生します。

    Illegal polymorphic or qualified type: T t
    In the instance declaration for 'Show (T t)'

andの必要性TypeSynonymInstancesとFlexibleInstances、それらが存在する実用的な理由は理解していますが、なぜ私の型T t がまだのインスタンスとして宣言できないのか理解できませんShow。これを行う方法はありT tますか?また、これが現在私のコードで問題になっていることを意味するのはどのプロパティですか?

4

1 に答える 1