Hello,
I'm beginning to think what I'm after is not possible...
I figure I should try to explain exactly what it is I'm after...
Basically I'm trying to mix type hackery with HOAS. More specifically,
here is a data type which I would like to use:
data Exp a where
Lam :: (Exp a -> Exp b) -> Exp (a -> b)
App :: Exp (a -> b) -> Exp a -> Exp b
Rcd :: (IsRecord (HCons (F l (Exp v)) r) =>
F l (Exp v) -> Exp r -> Exp (HCons (F l (Exp v)) r)
Proj :: (HasLabel l r v) => l -> Exp r -> Exp v
where F is a datatype constructor for record fields (as in the HList
paper), IsRecord checks that the argument is an HList of F l v and has
unique labels (also as in the HList paper); and HasLabel fishes the
appropriate type out of a HList of fields. The catch is that I want
GHC to infer my types, as well as check ascribed types. Thus I would
like to be able to successfully infer a type for:
Lam $ \x -> App (Proj l1 x) (Proj l2 x)
for some given labels l1 and l2. However, I cannot figure out how to
write HasLabel (or if it's even possible).
Anyone have any thoughts on this?
thanks,
Jeff
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
