Hello again Keean Schupke wrote:
Conor McBride wrote:
Yeah, that's nice. Scoped type variables are really handy for this sort of thing. You've got rid of the annotation on application (hey, what are typecheckers for?) but it's not so easy to lose it on the lambda: you need that for the fundep. To have a good story here, we need to show either how to get rid of the fundep or how to ensure we always have one.
However I don't understand what you meed by 'ensuring you always have one'... As far as I understand it we are lifting a value level operation (a type with several constructors) to the type level (a class containing several types) in this case each 'class' models a function.
I'm not sure that's quite the picture. We're using classes as predicates here, to define when a type-level proxy stands for a well-indexed piece of data. The fundep asserts that the proxy determines an index. In the expression example, an expression proxy is supposed to determine the type index (but not the environment index), hence the Lambda proxy must carry the argument type. The whole thing seems to fall apart without this fundep, although I don't see precisely why just now. But I think it's always possible and usually sensible to add enough phantom arguments to ensure that the fundep is available. Here's another variation: this time, the open expressions are equipped with a dependent case analysis operator. As Oleg has pointed out, you don't need to go that far to write eval, but I did anyway. data Top = Top data Pop i = Pop i data Var i = Var i data Lam s e = Lam e data App e1 e2 = App e1 e2 data Inx env t = forall i . GoodInx i env t => Inx i class GoodInx i env t | i env -> t where inxCase :: i -> (forall env'. p Top (env', t) t) -> (forall env' i' s' t'. GoodInx i' env' t => i' -> p (Pop i') (env', s') t) -> p i env t instance GoodInx Top (env, t) t where inxCase Top mTop mPop = mTop instance GoodInx i env t => GoodInx (Pop i) (env, s) t where inxCase (Pop i) mTop mPop = mPop i data Exp env t = forall e. GoodExp e env t => Exp e class GoodExp e env t | e env -> t where expCase :: e -> (forall i' env' t'. GoodInx i' env' t' => i' -> p (Var i') env' t') -> (forall i' env' e' s' t'. GoodExp e' (env', s') t' => e' -> p (Lam s' e') env' (s' -> t')) -> (forall i' env' e1' e2' s' t'. (GoodExp e1' env' (s' -> t'), GoodExp e2' env' s') => e1' -> e2' -> p (App e1' e2') env' t') -> p e env t instance GoodInx i env t => GoodExp (Var i) env t where expCase (Var i) mVar mLam mApp = mVar i instance GoodExp e (env, s) t => GoodExp (Lam s e) env (s -> t) where expCase (Lam e) mVar mLam mApp = mLam e instance (GoodExp e1 env (s -> t), GoodExp e2 env s) => GoodExp (App {-s-} e1 e2) env t where expCase (App e1 e2) mVar mLam mApp = mApp e1 e2 data Sem x env t = Sem {sem :: env -> t} evalInx :: GoodInx i env t => i -> Sem i env t evalInx i = inxCase i (Sem (\ (_, t) -> t)) (\ i -> Sem (\ (env, _) -> sem (evalInx i) env)) evalExp :: GoodExp e env t => e -> Sem e env t evalExp e = expCase e (\ i -> Sem (\env -> sem (evalInx i) env)) (\ e -> Sem (\ env arg -> sem (evalExp e) (env, arg))) (\ e1 e2 -> Sem (\ env -> sem (evalExp e1) env (sem (evalExp e2) env))) Meanwhile, I thought I'd write some more dependent programs, with the ubiquitous finite set family. {- We need natural numbers, equipped with case analysis -} data Nat = forall n. (GoodNat n) => Nat n class GoodNat n where natCase :: n -> (p Zero) -> (forall n'. GoodNat n' => n' -> p (Suc n')) -> p n data Zero = Zero instance GoodNat Zero where natCase Zero mZero mSuc = mZero zero :: Nat zero = Nat Zero data Suc n = Suc n instance GoodNat n => GoodNat (Suc n) where natCase (Suc n) mZero mSuc = mSuc n suc :: Nat -> Nat suc (Nat n) = Nat (Suc n) {- Now we can develop a family of sized finite types -} data Fin n = forall i. (GoodFin i n) => Fin i class GoodNat n => GoodFin i n | i -> n where finCase :: i -> (forall n'. GoodNat n' => p (FZ n') (Suc n')) -> (forall n' i'. GoodFin i' n' => i' -> p (FS i') (Suc n')) -> p i n data FZ n = FZ {- phantom for the fundep -} instance GoodNat n => GoodFin (FZ n) (Suc n) where finCase FZ mFZ mFS = mFZ fz :: GoodNat n => Fin (Suc n) fz = Fin FZ data FS i = FS i deriving instance GoodFin i n => GoodFin (FS i) (Suc n) where finCase (FS i) mFZ mFS = mFS i fs :: GoodNat n => Fin n -> Fin (Suc n) fs (Fin i) = Fin (FS i) {- Every nonempty finite set has a largest element. Here we must really do dependent case analysis on the number. -} data PMax n = PMax {pMax :: Fin (Suc n)} fmax :: GoodNat n => n -> Fin (Suc n) fmax n = pMax (natCase n (PMax fz) (\n -> PMax (fs (fmax n)))) {- There's a constructor-preserving embedding from each finite set to the next. -} data PWeak i n = PWeak {pWeak :: Fin (Suc n)} fweak :: GoodNat n => Fin n -> Fin (Suc n) fweak (Fin i) = pWeak (finCase i (PWeak fz) (\j -> PWeak (fs (fweak (Fin j))))) Now, before we get too excited about having some sort of case analysis principle, observe that all of these examples involve computing with unconstrained data: an expression of any type, an element of any finite set, etc. There's more to case analysis on datatype familes than that. You need to be able to handle constrained data too: an expression of type Int (which can't be Lambda), an element of the set of size two (which is FZ or FS FZ, but nothing larger). That's where the fun starts, and having unification in the typing rules is really rather handy. First test: to write lift :: forall n. (GoodNat m, GoodNat n) => (Fin m -> Fin n) -> Fin (Suc m) -> Fin (Suc n) -- as it were, -- lift f fz = fz -- lift f (fs i) = fs (f i) But I've plenty more where that came from. The old ones are the best... Cheers Conor -- http://www.cs.nott.ac.uk/~ctm