Haskell data type that represents valid types

Question

Is there a library that defines a data type that defines valid Haskell types (presumably this would be a GADT).

To explain, let me suggest what this might look like:

data A
data B

class Free t
instance Free A
instance Free B

x = Forall A (Forall B (Constraint (NumConstraint A) 
      (Constructor Function A (Constructor Function B A))))

This would represent:

forall a b. Num a => a -> b -> a

I'm not saying what I've suggested is a good implementation, I'm just trying to show what I mean.

Surely, if you can define the grammar of a type definition, you can create a GADT to represent it. Is there anything that already does this?

Answer 1

You are looking for the type-related ADTs in template-haskell. Note that Type is an instance of Ppr, which has the ppr pretty-print function.

ghci> import Language.Haskell.TH
ghci> :{
ghci> x <- runQ $ do
ghci|        a <- newName "a"
ghci|        b <- newName "b"
ghci|        pure $ ForallT [PlainTV a,PlainTV b] [AppT (ConT (mkName "Num")) (VarT a)] (AppT (AppT ArrowT (VarT a)) (AppT (AppT ArrowT (VarT b)) (VarT a)))
ghci| :}
ghci> x
ForallT [PlainTV a_4,PlainTV b_5] [AppT (ConT Num) (VarT a_4)] (AppT (AppT ArrowT (VarT a_4)) (AppT (AppT ArrowT (VarT b_5)) (VarT a_4)))
ghci> ppr x
forall a_0 b_1 . Num a_0 => a_0 -> b_1 -> a_0

In fact, the TemplateHaskell language extension GHC has will make playing with this surprisingly easy. Instead of having to write out the ForallT ... stuff, I can just "quote" the type I am looking for

ghci> :set -XTemplateHaskell -XExplicitForall
ghci> x' <- runQ [t| forall a b. Num a => a -> b -> a |]

And x' is the same as x (well maybe a and b end up being slightly different Names, but still)!