Haskell - 构造一个使用存在量化的类型

Question

在下面的代码中，我使用存在量化定义了数据类型 F。我希望 F 类型的值保存接受单个参数并产生例如 Int 作为结果的函数。该参数需要实现一个我称之为 C 的类型类，但现在留空。

这是我第一次尝试存在类型。我显然做错了什么，因为我似乎无法创建 F 类型的值。

{-# LANGUAGE ExistentialQuantification #-}

class C a where

data F = forall a. C a => F (a->Int)

makeF :: F
makeF = F $ const 1

如何解决这个编译错误？

No instance for (C a0) arising from a use of `F'
In the expression: F
In the expression: F $ const 1
In an equation for `makeF': makeF = F $ const 1

Answer 1

问题在于const 1 的类型为forall a . C a => a -> Int。当您将其传递给 F 时，我们将失去再次讨论 a 类型的机会，除非它是 C 类型的元素。

很遗憾，我们从未确定a 必须是什么！

特别是，GHC 通过为类型类 C 传入 dictionary 来处理此类存在，该类型类 C 对应于实际最终出现在存在中的任何类型。由于我们从未向 GHC 提供足够的信息来查找该字典，因此它给了我们一个类型错误。

所以要解决这个问题，我们必须在某处实例化 C

instance C Int

然后传递一个函数，该函数确定被遗忘的类型a实际上是C的一个实例

let x = F (const 1 :: Int -> Int)

Answer 2

如果你重写你的F 定义，它会起作用：

{-# LANGUAGE RankNTypes #-}

class C a where

data F = F (forall a. C a => a -> Int)

makeF :: F
makeF = F $ const 1

我正在尝试自己理解为什么：

您的原始类型说“存在a，它是C 的实例，我们有函数a -> Int”。 所以要构造存在类型，我们必须说明我们有哪个a：

{-# LANGUAGE ExistentialQuantification #-}

class C a where

data F = forall a. C a => F (a -> Int)

-- Implement class for Unit
instance C () where

makeF :: F
makeF = F $ (const 1 :: () -> Int)

---

这些定义并不完全相同：

data G = forall a . C a => G {
  value :: a         -- is a value! could be e.g. `1` or `()`
  toInt :: a -> Int, -- Might be `id`
}

data G' = G' {
  value' :: C a => a          -- will be something for every type of instance `C`
  toInt' :: C a => a -> Int, -- again, by parametericity uses only `C` stuff
}