C language AST using GADTs and constructor subsets

Question

I would like to define type level safe C language AST. So far, I come up with with something like this:

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

data Defn
  = Func String [Block]

type Block = forall a. BlockItem a
type Stmt = BlockItem StmtType

data BlockItemKind = StmtType

data BlockItem :: BlockItemKind -> * where
  Var :: String -> Expr -> BlockItem a
  SideEff :: Expr -> BlockItem StmtType
  Return :: Expr -> BlockItem StmtType

data Expr
  = Lit Int

The key point is the BlockItem data type. In C standard, there are two very similar structures – block and statements. Block is basically just list of statements that can also contain variable declaration. In this code, I'm trying to declare statement as subset of block items constructors (as SideEff and Return).

However, this code does not work as expected. Consider following code which is printing this AST:

showDefn :: Defn -> String
showDefn (Func name block) = "func " ++ name ++ " . " ++ show (showBlock <$> block)

showBlock :: Block -> String
showBlock (Var name e) = name ++ " = " ++ showExpr e ++ ";"
showBlock e = showStmt e

showStmt :: Stmt -> String
showStmt (SideEff e) = showExpr e ++ ";"
showStmt (Return e) = "return " ++ showExpr e ++ ";"

showExpr :: Expr -> String
showExpr (Lit x) = show x

When I'm evaluating showDefn with [Block], everything works well. This code however not work when I'm using Stmt type:

main :: IO ()
main = do
  -- FOLLOWING WORK
  print $ showDefn (Func "foo" [Var "a" (Lit 2), Var "b" (Lit 3)])

  -- FOLLOWING DOES NOT WORK
  print $ showDefn (Func "foo" [Return (Lit 0)])
  print $ showDefn (Func "foo" [Var "a" (Lit 1), SideEff (Lit 2)])

You can run the code here.

Where is the problem? I'm not even sure, if this is the right design.

user_7203016 · Answer

(Haskell pro-tip: If you ever find yourself having to use the ImpredicativeTypes extension, take your hands off the keyboard and back away from the computer.)

Anyway, to elaborate on @luqui's comment, the type Defn is equivalent to:

data Defn = Func String [forall a. BlockItem a]

This is a product type of a String and a list. The elements of the list have type forall a. BlockItem a, which is the type of things that can be BlockItem a for any a (as chosen by the caller/user of the value). As @luqui points out, Var "a" (Lit 2) has this type -- it can be a BlockItem a for any possible a, but your other block items can't. For example, Return (Lit 0) can only be BlockItem a when a is a StmtType, so it can't be put in a [forall a. BlockItem a] list -- the type is too general for it.

It's analogous to the following type, which allows storage of things that can be any kind of Num:

data NumList = NL [forall a. Num a => a]

Because 3 and 18 - 1 can be any kind of Num, we can put them in the list:

mylist = NL [3, 18-1]

Later, we can extract one of the element of this list:

NL [_,x] = mylist

and treat it as any kind of Num we want:

> x :: Integer
17
> x :: Double
17.0

But we can't put a specific Num type (e.g., an Int) into the list:

badlist = NL [length "hello"]  -- type error

If we could, then we could write:

> let NL [x] = badlist in sqrt x

to take the sqrt of an Int, and all "type hell" would break loose.

So, that's what you're doing wrong. It's hard to tell how you should do it right. Why doesn't the following work for you, without GADTs and DataKinds?

data Defn = Func String [BlockItem]

data BlockItem
  = Var String Expr
  | Stmt Statement

data Statement
  = SideEff Expr
  | Return Expr

data Expr
  = Lit Int

C language AST using GADTs and constructor subsets

1 Answers