实例声明中的“非法多态或限定类型”（System-F 样式树）

Posted 2023-03-05

【中文标题】实例声明中的“非法多态或限定类型”（System-F 样式树）

【英文标题】："Illegal polymorphic or qualified type" in instance declaration (System-F style trees)

【发布时间】：2015-11-23 19:42:20

【问题描述】：

我正在尝试在 Haskell 中实现 System-F 风格的数据结构。

我将使用 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>)

因此，由于 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)

到目前为止，所有这些都可以编译并且似乎可以工作。当我尝试为我的T t 类型创建Show 的实例时，就会出现问题。我添加了更多指令：

-# 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 的什么属性意味着这在我的代码中目前存在问题？

【问题讨论】：

GHC 就是它所说的。实例头中根本不允许多态类型。如果您将Tree 定义为新类型，那么您可以为其创建实例。

也许我应该补充一点，如果是这样的话，我也很感兴趣，为什么需要或被选择成为该语言的工作方式。

多类型和类型推断的隐式实例化使得这样的实例很麻烦。例如。假设 class C a where foo::a -> Int -- foo id 是否调用 instance C (Int -> Int) 或 instance C (forall a. a->a) ？如果我们有像 System F 中那样的显式类型参数，那将是第二个。使用隐式类型参数，就不太清楚了。现在，假设我们有一个复杂的表达式而不是id：它开始变得太复杂了。目前的机制是由类型构造函数驱动的，forall 被隐式实例化，不能算是大亨。

作为替代方法，请查看 Agda 的 implicit instance arguments。

【参考方案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 pragma 实际上不起作用）。例如，Show (forall a. t) 并不暗示Show [forall a. t]，因为[forall a. t] 一开始就无效。此外，类约束在与常规类型构造函数相同的系统中定义（除了它们以Constraint 的形式返回），因此Show (forall a. t) 在没有指示性实例化的情况下同样无效。