[Haskell-cafe] th-kinds v0.0.0

[Ryan Ingram]

On Mon, Mar 15, 2010 at 5:31 PM, Louis Wasserman
<wasserman.louis at gmail.com> wrote:
> GADT types that cannot be reified by TH.  Essentially, I think this is "the
> set of GADT data types that actually couldn't be implemented without GADTs."
>  Not sure, though.  In any event, at the moment, I don't think there's any
> hope of handling GADTs in TH at this point, so I don't really object to this
> problem.

Actually, with existential types and type equality constraints, GADTs
are redundant.  Here's a couple examples:

data GEqType a b where
    GRefl :: EqTypeGADT a a

data DEqType a b =
    (a ~ b) => DRefl

data Expr t where
   Lam :: (Expr a -> Expr b) -> Expr (a -> b)
   App :: Expr (a->b) -> Expr a -> Expr b
   Prim :: Show a => a -> Expr a
   Gt :: Expr Int -> Expr Int -> Expr Bool

data DExpr t =
   forall a b. (t ~ (a -> b)) => DLam (DExpr a -> DExpr b)
   | forall a. DApp (DExpr (a -> t)) (DExpr a)
   | Show t => DPrim t
   | (t ~ Bool) => Gt (DExpr Int) (DExpr Int)

The algorithm is pretty simple:
- existentially quantify over all type variables mentioned in the GADT
constructor
- add a type equality constraint to match the result type
- (optional) simplify

  -- ryan