Jeff wrote:
> 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
> 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).
It seems likely that you have the uses for the inferred type of the above
expression other than displaying it. You probably want to statically enforce
certain constraints when applying these Lam expressions. That is, you
want to apply Lam expressions only to the arguments that satisfy the
inferred HasField constraints. Why not to enforce the constraints at
that time then? The enclosed is a bit simplified version of the
code that demonstrates the idea. It is the typed evaluator statically
enforcing the HasField constraints. It does not use GADTs though as
they don't add to expressiveness. It would be great if we could delay
the more detailed discussion past the first week of Jan.
> and TypeEq doesn't work on uninstantiated type vars; correct me if I'm
> wrong about these.
TypeEq may work on uninstantiated type vars; please see
http://pobox.com/~oleg/ftp/Haskell/de-typechecker.lhs
and the paragraph containing the phrase ``The ability to operate on
and compare *unground* types with *uninstantiated* type variables is
often sought but rarely attained. The contribution of this message is
the set of primitives for nominal equality comparison and
deconstruction of unground types.''
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
module J where
data Lam f = Lam f
data App f x = App f x
data Proj l e = Proj l e
data Rec1 = Rec1 (Int->Int) -- simplified
data Rec2 = Rec2 Int -- simplified
{- well-formednedd (well-typeness) rules
class Exp a t | a -> t
instance (Exp ea a, Exp eb b) => Exp (Lam (ea -> eb)) (a->b)
instance (Exp f (a->b), Exp x a) => Exp (App f x) b
instance (Exp e r, HasField l r v) => Exp (Proj l e) v
instance Exp Rec1 Rec1
instance Exp Rec2 Rec2
-}
data L1 = L1
data L2 = L2
class HasField l r v | l r -> v where
flookup :: l -> r -> v
instance HasField L1 Rec1 (Int->Int) where
flookup _ (Rec1 x) = x
instance HasField L2 Rec2 Int where
flookup _ (Rec2 x) = x
t1 = Lam $ \x -> App (Proj L1 x) (Proj L2 x)
t2 = Lam $ \x -> App (Lam (\x -> x)) (Proj L2 x)
class Eval e v | e -> v where
eval :: e -> v
-- big step, CBN semantics
instance (Eval f (Lam (x->e2)), Eval e2 v) => Eval (App f x) v where
eval (App f x) = let Lam f' = eval f in eval $ f' x
instance (Eval e r, HasField l r v) => Eval (Proj l e) v where
eval (Proj _ e) = flookup (undefined::l) $ eval e
-- Those are values already
instance Eval (Lam e) (Lam e) where
eval = id
instance Eval Rec1 Rec1 where
eval = id
instance Eval Rec2 Rec2 where
eval = id
t3 = eval $ App t2 (Rec2 1)
-- The following gives the expected type error: Rec1 has no field L2
-- t4 = eval $ App t2 (Rec1 succ)