Hi again Actually, things are a little weirder than I first thought... Me:
The latter also means that the existential type encoding of 'some good term' doesn't give you a runnable term. There is thus no useful future-proof way of reflecting back from the type level to the term level. Any existential packaging fixes in advance the functionality which the hidden data can be given: you lose the generic functionality which real first-order data possesses, namely case analysis.
Ashley:
If I understand you correctly, without GADTs/datatype families, you cannot create Expression as a type-constructor without Oleg's auxiliary "t" argument that in fact encodes the structure of the expression. Is that right? I certainly can't see any way of getting rid of it: if, as you say, you existentially package it, the compiler can't deduce runnability.
It is possible to quantify the t existentially. It's even possible to quantify the t existentially and the env universally. Here's a cut down version, without the operational semantics: module Fam where data Top = Top data Pop i = Pop i data Var i = Var i data Lam s e = Lam e data App {-s-} e1 e2 = App e1 e2 {- I was wrong: instance inference is quite happy without the s, but... -} class GoodVar i env t | i env -> t where {} instance GoodVar Top (env, t) t where {} instance GoodVar i env t => GoodVar (Pop i) (env, s) t where {} class GoodExp e env t | e env -> t where {} instance GoodVar i env t => GoodExp (Var i) env t where {} instance GoodExp e (env, s) t => GoodExp (Lam s e) env (s -> t) where {} instance (GoodExp e1 env (s -> t), GoodExp e2 env s) => GoodExp (App {-s-} e1 e2) env t {- ...nothing works without the fundeps, so you need the argument type on Lam, which I suppose isn't surprising -} {- This does suggest that this recipe may not always be usable, or may require a lot of hand-annotation, where there is no fundep to be had. -} {- hiding the witness, leaving just a type family with the original indices -} data Exp env t = forall e. GoodExp e env t => MkExp e {- demanding, moreover, arbitrariness of environment -} data UExp t = forall e. MkUExp (forall env. GoodExp e env t => e) {- the usual suspects -} s :: Exp env ((r -> s -> t) -> (r -> s) -> r -> t) s = MkExp (Lam (Lam (Lam (App (App (Var (Pop (Pop Top))) (Var Top)) (App (Var (Pop Top)) (Var Top)))))) k :: Exp env (x -> r -> x) k = MkExp (Lam (Lam (Var (Pop Top)))) us :: UExp ((r -> s -> t) -> (r -> s) -> r -> t) us = MkUExp (Lam (Lam (Lam (App (App (Var (Pop (Pop Top))) (Var Top)) (App (Var (Pop Top)) (Var Top)))))) uk :: UExp (x -> r -> x) uk = MkUExp (Lam (Lam (Var (Pop Top)))) However, the point remains that having an Exp env t does you no good, because you can't deduce any functionality from mere goodness. It's just the usual problem with abstract datatypes, really. I wonder if there's some awful half-baked discriminator-selector interface to these things. Cheers Conor -- http://www.cs.nott.ac.uk/~ctm