Creating a List of Valid Constructors

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 a list of all valid constructors for D T1 , and x2 is a list of all valid constructors for D T2 .

However, I want both of these lists to display any additional constructors added to D , I don’t want to hardcode these lists as they are at present.

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

+8
haskell gadt
source share
1 answer

Disclaimer - my TemplateHaskell-fu almost does not exist - but I did a little research, which should give you a starting point for working with:

For those who don’t know, Template Haskell is a kind of meta-programming (language) that allows you to write programs that run at compile time β€” it is a type that is checked to be safe (for some definition of safe, I think you 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 uploading the file to GHCi (don't forget :set -XTemplateHaskell there)

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

typeInfo is Q Info , which allows you to retrieve information from a type (escaped by '' ). $(..) works like print.

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

 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 am with a little pattern matching - you can find constructors that either have no restrictions ( ForallC ) or a specific type ( TMP.T1 / TMP.T2 ), and then write some expression - to create a new type from them.

Now I don’t have enough time to provide this, but today I will update this answer.

EDIT

I looked a little more at building types, but I have to admit that I got a little stuck myself - I successfully deconstructed the type of type information.

 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 that it is possible to filter T1 / T2 / forall d from here, tedious, but doable for building lists.

What am I wrong with building the type - if I upload a file to ghci, I can execute

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

but if I name it in a 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 Kemet creates some magic lenses for creating things, and there he works inside the same file, but splice is not assigned to a variable - so maybe you need to create names for your lists inside Q Exp - I think mkName will be where you need it.

This completes everything that I learned - I hope this helps, I at least learned a few things - for a complete answer, maybe someone smarter / more experienced with the haskell template can provide some of his / her knowledge second answer.

+2
source share

All Articles