[Haskell-cafe] th-kinds v0.0.0
Ryan Ingram
ryani.spam at gmail.com
Tue Mar 16 14:28:08 EDT 2010
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
More information about the Haskell-Cafe
mailing list