Haskell

Question

在下面的代码中，我使用存在量化定义了一个数据类型 F。我希望 F 类型的值包含接受单个参数并产生例如 Int 作为结果的函数。该参数需要实现一个类型 class ，我称之为 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

如果您重写您的 F 定义，它将起作用：

{-# LANGUAGE RankNTypes #-}

class C a where

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

makeF :: F
makeF = F $ const 1

我自己也在努力理解为什么：

您的原始类型显示 "there exists a which is instance of C, and we have function 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
}

Answer 2

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

的元素

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

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

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

instance C Int

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

的一个实例

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

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

Haskell - constructing a type that uses existential quantification

existential-type