haskell - 我可以概括 Haskell 中的类约束吗？

Question

在我的应用程序中，我有一个如下所示的类型定义:

{-# LANGUAGE ExistentialQuantification #-}

class C a where

data A = forall a. C a => A { unA :: a }

我绝对想要善意的签名A::Type。

我想概括类约束，如下所示:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE ScopedTypeVariables       #-}

import Data.Kind (Type, Constraint)

class C a where

data A' (c :: Type -> Constraint) where
  A' :: forall a. c a => { unA :: a } -> A' c

type A = A' C

请注意，A 应该与开头定义的 A 同构。

但是 GHC (8.6.5) 拒绝广义定义:

generalize.hs:11:19: error: Not in scope: type variable ‘c’
   |
11 |   A' :: forall a. c a => { unA :: a } -> A' c
   |                   ^

generalize.hs:11:45: error: Not in scope: type variable ‘c’
   |
11 |   A' :: forall a. c a => { unA :: a } -> A' c
   |                                             ^

我不明白这个错误，因为我确实启用了 ScopedTypeVariables。

我是否遗漏了一些明显的东西，或者我想要做的事情是不可能的？如果是这样，为什么不呢？

Answer 1

你说得差不多了，你想要的是

data HasConstraint (c :: Type -> Constraint) where
  Pack :: forall (c :: Type -> Constraint) a . c a => { unPack :: a } -> HasConstraint c

因此您还必须在构造函数类型签名中包含 c，因为它与 GADT 的数据声明完全分开。

我想你会想这样使用它:

instance Show (HasConstraint Show) where show (Pack x) = show x
show (Pack 10 :: HasConstraint Show) -- => "10"

你也可以这样写

withPacked :: forall (c :: Type -> Constraint) b. (forall a. c a => a -> b) -> HasConstraint c -> b
withPacked f (Pack x) = f x
withPacked @Show show (Pack 10) -- => "10"

不过，我不确定您是否还可以用它做很多其他事情。

<小时/>

(请注意，这里的“getter”unPack 实际上也不能与 GADT 一起使用，如果您想实际解压内容，则始终必须在构造函数上进行模式匹配)。