用限制类型写GADT记录 [英] Write GADT record with constrained type

问题描述

我的程序中编译了以下代码：

I have the following code that compiles in my program:

{-# 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弃用的数据类型上下文，所以我试图避免它们）：

Since the number of arguments for the Foo contructor can be many, I would like to write the code using record syntax, but I cannot figure out how to do this with GADT syntax (GHC deprecated datatype contexts, so I'm trying to avoid them):

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

我需要约束 a 在 Foo 的构造函数中，就像我上面没有记录语法所做的那样。我怎么做到这一点？

I need to constrain a in Foo's constructor just like I did above without record syntax. How can I do this?

推荐答案

您可以通过在构造函数的类型中声明记录析构函数来实现此目的： / b>

You can achieve this by declaring the record destructors within the type of the constructor as follows:

{-# 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 的方式做一些比看起来更狡猾的事情。这是坚持显示数据的一种简单方法：

but I suspect there's an easier way of achieving what you intend to do, unless you're doing something more cunning with the type a than it seems. Here's a simpler way to insist on showable data:

{-# 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 class就是为了让事情变得可见。你可能有一些更深层的目的，我没有看到。

This way has the benefit of working for arbitrary Showable data, without making instances of the HasData class nor using all those compiler pragmas, but that's only of help to you if your HasData class was just there to make things Showable. You might have some deeper purpose I'm not seeing.

（你可以考虑将 Show 对于你实际使用它的地方，简化更多的事情，并允许你创建Functor实例，这会更简单，并且根本不需要任何编译器编译指示。多年来，我越来越喜欢保持一般性，并且使Functor实例。）

(You might consider dropping the Show context altogether except for where you actually use it, to simplify things more and allow you to make Functor instances. That would be simpler and wouldn't require any compiler pragmas at all. Over the years I've become fonder of keeping things general and making Functor instances.)

这篇关于用限制类型写GADT记录的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！