Записи 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 «s так же, как я сделал або без синтаксиса записи. Как я могу это сделать?

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 чем кажется. Вот простой способ настоять на showable данных:

{-# 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.)