使用约束类型写入 GADT 记录

Question

SO是一场狗屎秀。感谢您的搭车。

Answer 1

您可以通过在构造函数的类型中声明记录析构函数来实现此目的，如下所示：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}

data Foo :: * -> * where
    Foo :: HasData a => { -- look - the context declared upfront
        getStr :: String, -- wow - function declaration in type sig!
        getData :: Data a, -- only allowed with a HasData instance
        getInt :: Int
    } -> Foo a 

但我怀疑有一种更简单的方法可以实现您想要做的事情，除非您正在使用

a

类型做一些比看起来更狡猾的事情。这是坚持显示数据的更简单方法：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

data Bar a where
    Bar :: Show a => {
        getStr' :: String,
        getData' :: a, -- can Show 
        getInt' :: Int
    } -> Bar a -- have (Show a)
deriving instance Show (Bar a)

这种方式的优点是可以处理任意 Showable 数据，无需创建

HasData

类的实例，也无需使用所有这些编译器编译指示，但如果您的

HasData

类只是为了使内容可显示，那么这对您才有帮助。你可能有一些我没有看到的更深层次的目的。

（除了实际使用它的地方之外，您可能会考虑完全删除

Show

上下文，以进一步简化事情并允许您创建 Functor 实例。这会更简单，根本不需要任何编译器编译指示。多年来我变得更喜欢保持通用性并创建 Functor 实例。）