Elegant way to do associated "data items"-CodePudding

I am trying to have associated "data items" of ContentType of and its content:

data ContentType = MyInt | MyBool deriving ( Show )

data Encoding'
  = EncodingInt  [Int]
  | EncodingBool [Bool]

chooseContentType :: IO ContentType
chooseContentType = undefined

How do I make something like this, but type-checked?

data Encoding a =
  Encoding { contentType :: ContentType
           , content :: [a]
           }

CodePudding user response：

The feature you're looking for is called generalized algebraic data types (or GADTs, for short). It's a GHC extension, so you'll have to put a pragma at the top of your file to use them. (I'm also including StandaloneDeriving, because we'll use that to get your Show instance in a minute)

{-# LANGUAGE GADTs, StandaloneDeriving #-}

Now you can define your ContentType type fully. The idea is that ContentType is parameterized by the (eventual) type of its argument, so ContentType will have kind * -> * (i.e. it will take a type argument).

Now we're going to write it with a bit of a funny syntax.

data ContentType a where
  MyInt :: ContentType Int
  MyBool :: ContentType Bool

This says that MyInt isn't just a ContentType; it's a ContentType Int. We're keeping the type information alive in ContentType itself.

Now Encoding can be written basically the way you have it.

data Encoding a =
  Encoding { contentType :: ContentType a
           , content :: [a]
           }

Encoding also takes a type parameter a. Its content must be a list of a, and its content type must be a content type that supports the type a. Since our example has only defined two content types, that means it must be MyInt for integers or MyBool for Booleans, and no other encoding will be supported.

We can recover your deriving (Show) on ContentType with a StandaloneDeriving clause (this is the second GHC extension we turned on in the above pragma)

deriving instance Show (ContentType a)

This is equivalent to your deriving clause, except that it sits on its own line since the GADT syntax doesn't really have a good place to put one in the same line.