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

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

{-# 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。

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

最佳答案

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

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一起使用，如果要实际拆包，则必须始终在构造函数上进行模式匹配）。

关于haskell - 我可以概括Haskell中的类约束吗？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/58011063/