用约束类型写GADT记录

Question

我有以下代码编译在我的程序中:

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

class (Show (Data a)) => HasData (a :: *) where
    type Data a :: *

data Foo :: * -> * where
    Foo :: (HasData a) => String -> Data a -> Int -> Foo a -- bunch of args

deriving instance Show (Foo a)

由于Foo构造函数的参数数量可以很多,我想使用记录语法编写代码,但我无法弄清楚如何使用GADT语法(GHC弃用的数据类型上下文,所以我试图避免它们) :

data Foo :: * -> * where
    Foo {
        getStr :: String,
        getData :: Data a, -- want (HasData a)
        getInt :: Int
    } :: Foo a -- want (HasData a)

我需要限制a在Foo的就像我上面没有记录语法构造.我怎样才能做到这一点？

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)

这种方式有利于处理任意可显示数据,不需要创建HasData类的实例,也不使用所有这些编译器编译指示,但如果你的HasData类只是为了让事物显示,那对你只有帮助.你可能有一些我没有看到的更深层的目的.

(您可以考虑Show完全删除上下文,除了您实际使用它的位置,更简化更多内容并允许您创建Functor实例.这将更简单,并且根本不需要任何编译器实用程序.多年来我已成为保持一般性并制作Functor实例的想法.)