How to represent a variable-typed constructor list with GADTs?

Question

I'm implementing a small DSL for a research project I'm involved with. Since this is the example for almost literally every explanation of GADTs out there, I decided that this would be a good time to really get started on using them. The obvious expressions (arithmetic, etc) worked out fine, but my DSL needs to support user-defined functions, which is where I ran into an issue.

With no GADTs, the structure of my expression type looked somewhat like this (condensed to a minimal example):

data Expr = IntConst Int
          | BoolConst Bool
          | Plus Expr Expr
          | Times Expr Expr -- etc
          | AndAlso Expr Expr -- etc
          | Call String [Expr] -- function call!

Converted to GADTs, how can I express the Call rule?

data Expr a where
     IntConst :: Int -> Expr Int
     BoolConst :: Bool -> Expr Bool
     Plus :: Expr Int -> Expr Int -> Expr Int
     Times :: Expr Int -> Expr Int -> Expr Int
     AndAlso :: Expr Bool -> Expr Bool -> Expr Bool
     Call :: ???

My first thought was that this is impossible without some super fancy dependent types, because there's no way to know what types a given user function will accept (also the return type, but I can fix that by making Call return Expr a and specializing at the construction site). I can force it to typecheck by "erasing" the type, by adding rules

     EraseInt :: Expr Int -> Expr a
     EraseBool :: Expr Bool -> Expr a

but then it seems that I lose the benefit of having GADTs in the first place. I was also thinking there might be some other rankN polymorphism I could use in Call (something something existential types?), but nothing I came up with seemed to work.

Help?

Answer 1

You can make another GADT with represent argument lists using type-level lists like this:

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

data ArgList (as :: [*]) where
  NilArgList :: ArgList '[]
  ConsArg    :: Expr a -> ArgList as -> ArgList (a ': as)

data Expr a where
  IntConst  :: Int -> Expr Int
  BoolConst :: Bool -> Expr Bool
  Plus      :: Expr Int -> Expr Int -> Expr Int
  Times     :: Expr Int -> Expr Int -> Expr Int
  AndAlso   :: Expr Bool -> Expr Bool -> Expr Bool
  Call      :: String -> ArgList as -> Expr b

pattern x :^ y = ConsArg x y
infixr :^

example :: Expr Int
example =
  Call "exampleFn" (IntConst 1 :^ BoolConst True :^ NilArgList
                        :: ArgList [Int, Bool])

You will need to give some explicit type signatures for argument lists (like in example). Also, the result type of Call (forall b. Expr b) is a bit awkward, but I'm not sure that can be avoided unless you have more type information than String for the function it takes in. If you had more information there, you could also potentially relate the argument types (as) to the expected argument types for the function. I think we need more details about the specific situation you have to go any further with that part though.