3

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

我将使用A <B>to 表示将术语A应用于类型B只是为了使其明确（也使用大写字母表示类型）。

假设Tree <T>是具有 type 值的二叉树的类型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)

到目前为止，所有这些都可以编译并且似乎可以工作。当我尝试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意味着这在我的代码中目前存在问题？

4

1 回答 1

3

首先，有一个技巧可以让您为通用量化类型编写一些实例：我们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 不支持命令式实例化（并且ImpredicativeTypespragma 实际上不起作用）。例如，Show (forall a. t)不暗示Show [forall a. t]，因为[forall a. t]一开始就无效。此外，类约束在与常规类型构造函数相同的系统中定义（除了它们以 kind 形式返回Constraint），因此Show (forall a. t)在没有指示性实例化的情况下同样无效。

于 2015-11-23T20:34:40.367 回答