"Недопустимый полиморфный или квалифицированный тип" в объявлении экземпляра (деревья стиля System-F)

Question

Я экспериментирую с реализацией структур данных в стиле System-F в Haskell.

Я буду использовать A <B> означать применение термина A к типу B просто, чтобы сделать это однозначным (также используя заглавные буквы для типов).

Скажем Tree <T> тип бинарных деревьев со значениями типа T, Мы хотим найти тип, который может действовать как Tree <T>, Есть три конструктора:

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

Так что, по некоторым соображениям, я думаю, благодаря Жирару, мы можем использовать следующее

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:

{-# 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)'

Я (думаю, я) понимаю необходимость TypeSynonymInstances а также FlexibleInstances и прагматические причины их существования, но я не понимаю, почему мой тип T t до сих пор не может быть объявлен экземпляром Show, Есть ли способ сделать это, и какое свойство T t означает, что это в настоящее время проблематично в моем коде?

Answer 1

Во-первых, есть хитрость, которая позволяет вам написать несколько экземпляров для универсально квантифицированных типов: мы удаляем forall -s из главы экземпляра, и ввести ограничения на равенство типов для любых типов, которые мы хотим создать для переменных. В нашем случае:

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

instance (a ~ String, Show t) => Show (a -> (t -> a) -> (a -> a -> a) -> a) where
  show t = t "nil" show (\l r -> "(" ++ l ++ ", " ++ r ++ ")")

-- show (fork empty (fork (leaf ()) empty)) == "(nil, ((), nil))"

Это работает, потому что глава экземпляра неявно количественно определяет переменную для нас. Конечно, если мы хотим создать полиморфный тип для нескольких различных типов, этот прием может быть неприменим.

С другой стороны, если бы GHC допускал полиморфные типы в экземплярах, это было бы бесполезно, потому что GHC не поддерживает неумышленную реализацию (и ImpredicativeTypes прагма на самом деле не работает). Например, Show (forall a. t) не подразумевает Show [forall a. t], так как [forall a. t] не действует с самого начала. Кроме того, ограничения классов создаются в той же системе, что и обычные конструкторы типов (за исключением того, что они возвращаются в виде Constraint), так Show (forall a. t) аналогичным образом недействительным без неумышленного создания.