Creating a list of valid constructors

Question

Consider the following:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data T = T1 | T2

data D (t :: T) where
  D1 :: D T1
  D2 :: D T2
  D3 :: D d
  D4 :: D T1

x1 :: [D T1]
x1 = [D1, D3, D4]

x2 :: [D T2]
x2 = [D2, D3]

Basically x1 is the list of all valid constructors for D T1, and x2 is the list of all valid constructors for D T2.

However, I want both this lists to reflect any additional constructors added to D, I don't want to hard code these lists like they are currently.

Is there a way to define x1 and x2 such that they are automatically generated from D?

Answer 1

Disclaimer - my TemplateHaskell-fu is almost non-existent - but I've investigated a bit which should give you a starting point to work with:

For those who don't know Template Haskell is a kind of meta-programming (language) that allows to write programs that run at compile time - it is type checked so it is safe (for some definition of safe, I think you can write programs that take infinite time to compile).

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}

import Language.Haskell.TH

data T = T1 | T2

data D (t :: T) where
  D1 :: D T1
  D2 :: D T2
  D3 :: D d
  D4 :: D T1

You can start by loading the file into GHCi (don't forget to :set -XTemplateHaskell there)

> typeInfo = reify ''D
> $(stringE . show =<< typeInfo)

typeInfo is a Q Info that allows you to extract information from a type (escaped by '') - the $(..) works like print.

This gives you the template haskell Expression that constructs your (G)ADT:

TyConI (
    DataD [] TMP.D [KindedTV t_6989586621679027167 (ConT TMP.T)] Nothing 
        [GadtC [TMP.D1] [] (AppT (ConT TMP.D) (ConT TMP.T1))
        ,GadtC [TMP.D2] [] (AppT (ConT TMP.D) (ConT TMP.T2))
        ,ForallC [KindedTV d_6989586621679027168 (ConT TMP.T)] [] (GadtC [TMP.D3] [] (AppT (ConT TMP.D) (VarT d_6989586621679027168)))
        ,GadtC [TMP.D4] [] (AppT (ConT TMP.D) (ConT TMP.T1))] [])

I with a bit of pattern matching - you can find the constructors that have either no restriction (ForallC) or a certain type (TMP.T1/TMP.T2) and then write some expression - to create a new type from those.

Right now I don't have enough time to supply that - but I will update this answer tonight.

EDIT

I looked some more at constructing types, but I have to admit I am a bit stuck myself - I deconstructed the type info kind of successfully.

d = reify ''D

dataName :: Info -> Maybe [Name]
dataName (TyConI (DataD _ _ _ _ x _) )= Just [t | NormalC t _ <- x]
dataName _ = Nothing

gadtDataUnsafe :: Info -> Q Exp
gadtDataUnsafe (TyConI (DataD _ _ _ _ cons _)) = return $ head $ concat [t | GadtC t _ _ <- cons]

I think it is doable to filter the T1/T2/forall d from here, tedious but doable to construct the lists.

What I failed at, is constructing the type - if I load the file into ghci I can execute

> f = $(gadtDataUnsafe =<< d)
>:t f
f :: D 'T1

but if I call that within the file I get the following error

error:
    • GHC stage restriction:
        ‘gadtData’ is used in a top-level splice, quasi-quote, or annotation,
        and must be imported, not defined locally
    • In the untyped splice: $(gadtData =<< d)

I know that for example Edward Kmett makes some th-magic creating lenses for stuff and there it works inside the same file, but the splice is not assigned to a variable - so maybe you need to construct the names for your lists inside the Q Exp - I guess mkName would be something you need there.

This concludes everything I found out - I hope it helps, I at least learnt a few things - for a full answer maybe someone smarter/more experienced with template haskell can supply some of his/her knowledge in a second answer.