In article <41D808C3.7010408@cs.nott.ac.uk>, Conor McBride wrote:

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.

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. -- Ashley Yakeley, Seattle WA

In article , karczma@info.unicaen.fr wrote: GHCi is correct to complain:

class Vspace a v | v -> a

OK, the first parameter ("a") depends on the second ("v").

instance Vspace a a where

And this determines it: the first parameter must always be the same as the second.

instance (Vspace a v) => Vspace a (c->v) where

This is incompatible with the previous instance declaration, since "a" is not the same as "c -> v". And any instance decl that were permitted by the fundep would in any case overlap. -- Ashley Yakeley, Seattle WA

karczma@info.unicaen.fr writes:

This is what I want. For a given set of vectors, the associated scalars are unique, otherwise I would have problems with norm.

In the instance Vspace a a the compiler doesn't know that "a" is supposed to be a scalar only. It matches vector types (functions) too. And adding a context won't help. An instance of the form instance Ctx a => Cls (T a) means "T a can always be used as an instance of Cls, and such usage will yield a further requirement of Ctx a which must be fulfilled" rather than "T a can be used as an instance of Cls as long as Ctx a holds". In particular it will overlap with any other instance whose head can be unified with Cls (T a). Instance overlapping doesn't take instance contexts into account, only instance heads. The problem can be "solved" by enumerating concrete scalar types instead of using a generic instance Vspace a a. I'm afraid Haskell classes are not expressive enough for a generic instance in this case. -- __("< Marcin Kowalczyk \__/ qrczak@knm.org.pl ^^ http://qrnik.knm.org.pl/~qrczak/

I would suggest defining types for unit and functions... data Scalar a = Scalar a data Function c v = Function c v instance VSpace a (Scalar a) ... -- replaces 'a' instance VSpace a (Function c a) ... -- replaces c -> a instance VSpace a v => a (Function c v) ... -- replaces c -> v Here Scalar is just a 'special' identity, and 'Function' is a 'special' arrow (->) ... Keean. karczma@info.unicaen.fr wrote:

Ashley Yakeley writes:

...

GHCi is correct to complain:

...

class Vspace a v | v -> a

OK, the first parameter ("a") depends on the second ("v").

This is what I want. For a given set of vectors, the associated scalars are unique, otherwise I would have problems with norm. But I have problems anyway...

...

...

instance Vspace a a where

And this determines it: the first parameter must always be the same as the second.

...

instance (Vspace a v) => Vspace a (c->v) where

This is incompatible with the previous instance declaration, since "a" is not the same as "c -> v".

Why "always the same"? This is just *this* instance. If I eliminate Vspace a a, and I write instance (Num a)=>Vspace a (c->a) where (f <+> g) x = f x + g x (a *> f) x = a * f x and then I tried to generalize, by instance (Vspace a v) => Vspace a (c->v) where (f <+> g) x = f x <+> g x -- ... I get another error, even less understandable. Can you guess it without testing?... I permitted all extensions, overlapping instances, etc.

Jerzy Karczmarczuk _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Henning Thielemann cites myself

...

I am afraid that something is wrong with my understanding of multi- param classes with dependencies. I tried to generalize one of my old packages for quantum *abstract* computations, where state vectors are defined as functional objects,...

class Vspace a v | v -> a where (<+>) :: v -> v -> v (*>) :: a -> v -> v -- etc.

instance Vspace a a where (<+>) = (+) (*>) = (*) -- etc. No problem.

instance (Vspace a v) => Vspace a (c->v) where f <+> g = \x -> f x <+> g x (a *> f) x = a *> (f x) -- ...

I had the same problem with the same class http://www.haskell.org//pipermail/haskell-cafe/2004-March/005979.html and thus Dylan Thurston advised me to drop functional dependencies.

I can't... Otherwise I am killed by ambiguities, later.

Here are two implementations using multi-type classes without functional dependencies. (They wait for unification, yet, sorry.) http://cvs.haskell.org/darcs/numericprelude/VectorSpace.lhs http://cvs.haskell.org/darcs/numericprelude/physunit/VectorSpace.hs

I followed this discussion, and I know your and DT DARC project. Unfortunately my ambitions are Gargantuan, I want to have vector spaces which encompass functions over ADT (the config. specification for a quantum system), functions over functions (duals and operators), and also functional tensors, which makes it possible to construct binary functions as a 'product' of two unary functions; extensible. And all this over all kind of scalars. Principally complex, but also some differential scalars (elements of a differential algebra, permitting to do the 'automatic differentiation' of Dirac brackets and also kets, which would permit to use constructively the differential recurrential definitions of states (Hermite functions, etc.) For the moment I am obliged to FIX the field of scalars, this *partly* solves my mathematical troubles. I believe in almost all what Ashley Yakeley (and Marcin QK) say, but in

...

...

instance (Num a)=>Vspace a (c->a) where instance (Vspace a v) => Vspace a (c->v) where

These are also incompatible. ...

the word 'incompatible' should be understood as 'incompatible with current Haskell', *not* with common sense. Pity. It is obvious that both: a function any -> scalar, and (any->scalar)->any->scalar with good arithmetic scalars permit to establish the vector structure. Actually, the instances as quoted above produces bizarrily an error which says that something is less polymorphic than expected; the overlapping is accepted (apparently). Sigh. Jerzy Karczmarczuk

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

Keean Schupke wrote:

Conor,

I thought you might like this... It shows how to do this without phantom types! (we just use scoped type variables to help the typechecker sort things out)... What do you think? Does this overcome all the problems with Olegs approach? (the only slight problem I have found is that you must give the parameters explicitly for definitions like test3)

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. Meanwhile, Oleg wrote:

class OpenExpression t env r | t env -> r where efold :: t -> env -> (forall r. r -> c r) -- Constant -> (forall r. r -> c r) -- Symbol -> (forall a r. (a -> c r) -> c (a->r)) -- Lambda -> (forall a r. c (a->r) -> c a -> c r) -- Application -> c r

Funny you should say that. That's rather close to the traditional way inductive datatype families have been presented for lord knows how long: a bunch of constructors and an elimination operator, aka an induction principle. Except that a fold (otherwise known as a weak rule-induction principle) isn't enough for programming with these things, because it throws away information: look, you can't tell the difference between the constant case and the symbol case! It's ok for running expressions, for which you only need the type index, but what if your program's result type depended on the expression? I'm halfway through an example (based on something a bit simpler than lambda-terms), which I'll send off in a bit... But anyway, it's an interesting question. Do you think it might be possible to translate programs written in a pattern matching style into applications of this sort of elimination operator? Perhaps someone should do a PhD about it... Cheers Conor -- http://www.cs.nott.ac.uk/~ctm

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

G'day all. Quoting Conor McBride :

Where now? Well, counterexample fiends who want to provoke Oleg into inventing a new recipe had better write down a higher-order example. I just did, then deleted it. Discretion is the better part of valour.

Thankfully, I'm the sort of person who doesn't know when to stop. Is this the sort of thing you had in mind? << -- WARNING: This code is untested under GHC HEAD data State s a = Bind :: State s a -> (a -> State s b) -> State s b | Return :: a -> State s a | Get :: State s s | Put :: s -> State s () instance Monad (State s) where (>>=) = Bind return = Return instance MonadState s (State s) where get = Get put = Put runState :: State s a -> s -> (s,a) runState (Return a) s = (s,a) runState Get s = (s,s) runState (Put s) _ = (s,()) runState (Bind (Return a) k) s = runState (k a) s runState (Bind Get k) s = runState (k s) s runState (Bind (Puts) k) _ = runState (k ()) s runState (Bind (Bind m k1) k2) s = runState m (\x -> Bind (k1 x) k2) s

...

Cheers, Andrew Bromage

Conor McBride has pointed out a really interesting issue with macro-expressing GADT in typeclasses, outlined in the previous message. Suppose we have a GADT "OpenExpression env r" for lambda-expressions, and we define newtype Expression r = MkExpression (forall env. OpenExpression env r) to abstract over the environment, and we then write a function runExpression to ``compile'' a lambda-expression to a native Haskell expression. The typeclass encoding translated GADT "OpenExpression env r" into a class "OpenExpression t env r" and each GADT data constructor into a regular data constructor (with the appropriate arity plus some phantom stuff). The class OpenExpression was merely a constraint on the well-formedness of lambda-terms. We need another class, RunOpenExpression, to define the ``compiler'' function. So, "newtype Expression" had a type newtype Expression t r = MkExpression (forall env. RunOpenExpression t env r => t) which is not very satisfactory: the encapsulated constraint is RunOpenExpression rather than OpenExpression. That means, if we wish to do something else with the Expression (e.g., compute its size or depth, or print it), we need to add the corresponding class constraint to "newtype Expression" declaration. That is not modular. We don't want to go back and change data declarations just because we thought up a new way of handling our data. It should be noted first that this problem arises only when we have to explicitly state the constraints (as in instance declarations and signatures of higher-ranked functions). If it is possible to let the compiler figure out the types, then the approach in the previous message seems preferable -- it seems neater, at least to me. I must also note that when it comes to typeclass constraints, GADT too have some modularity issues (which are outside of the scope of this message). The scope of this message is the recipe for translating GADT into typeclasses that _can_ deal with local quantification and similar issues. As one may see in the code below, we define newtype Expression t r = MkExpression (forall env. OpenExpression t env r => t) Note the OpenExpression constraint. The compiler is defined as runExpression (MkExpression e) = openRun e () If we'd rather compute the depth or the size of the expression, we define depth (MkExpression e) = compute_depth e () where <see below> size (MkExpression e) = compute_size e () where <see below> That is, we can handle the expression in arbitrary ways, and we don't need to modify the OpenExpression constraint. The key is to realize that the GADT declaration introduces both the constructors and the deconstructor. So, to match GADT, our typeclass translation must also introduce the deconstructor. The second insight is that a catamorphism makes a good deconstructor. In our case, the fold must be polymorphic -- like the gfold in ``Boilerplate scrapping''. I bow to Ralf Laemmel for the type of gfold. The drawback of the approach is that the class OpenExpression becomes not-extensible. We no longer can easily add more 'instances' to the class. OTH, if we place the handlers in a HList, and use the OOHaskell encoding, we can probably arrive at open (extensible) GADT. The complete new code is included.

Where now? Well, counterexample fiends who want to provoke Oleg into inventing a new recipe had better write down a higher-order example. I just did, then deleted it. Discretion is the better part of valour.

It is possible to undelete that example? {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} module Expression where -- data Sym env r where -- FirstSym :: Sym (r,xx) r -- NextSym :: Sym env r -> Sym (a,env) r class SymT t env r data FirstSym = FirstSym deriving Show data NextSym t = NextSym t deriving Show instance SymT FirstSym (r,xx) r instance SymT t env r => SymT (NextSym t) (a,env) r class SymT t env r => RunSym t env r | t env -> r where runSym :: t -> env -> r -- runSym FirstSym (r,xx) = r; instance RunSym FirstSym (r,xx) r where runSym _ (r,xx) = r instance RunSym var env r => RunSym (NextSym var) (a,env) r where runSym (NextSym var) (a,env) = runSym var env -- the code literally -- data OpenExpression env r where -- Lambda :: OpenExpression (a,env) r -> OpenExpression env (a -> r); -- Symbol :: Sym env r -> OpenExpression env r; -- Constant :: r -> OpenExpression env r; -- Application :: OpenExpression env (a -> r) -> OpenExpression env a -> -- OpenExpression env r -- Note that the types of the efold alternatives are essentially -- the "inversion of arrows" in the GADT declaration above class OpenExpression t env r | t env -> r where efold :: t -> env -> (forall r. r -> c r) -- Constant -> (forall r. r -> c r) -- Symbol -> (forall a r. (a -> c r) -> c (a->r)) -- Lambda -> (forall a r. c (a->r) -> c a -> c r) -- Application -> c r data Lambda a t = Lambda t deriving Show data Symbol t = Symbol t deriving Show data Constant r = Constant r deriving Show data Application a t1 t2 = Application t1 t2 deriving Show instance OpenExpression t (a,env) r => OpenExpression (Lambda a t) env (a->r) where efold (Lambda t) env on_const on_symbol on_lambda on_app = on_lambda (\a -> efold t (a,env) on_const on_symbol on_lambda on_app) instance RunSym t env r => OpenExpression (Symbol t) env r where efold (Symbol t) env on_const on_symbol on_lambda on_app = on_symbol (runSym t env) instance OpenExpression (Constant r) env r where efold (Constant t) env on_const on_symbol on_lambda on_app = on_const t instance (OpenExpression t1 env (a->r), OpenExpression t2 env a) => OpenExpression (Application a t1 t2) env r where efold (Application t1 t2) env on_const on_symbol on_lambda on_app = on_app (efold t1 env on_const on_symbol on_lambda on_app) (efold t2 env on_const on_symbol on_lambda on_app) newtype ID a = ID a unID (ID a) = a openRun t env = unID $ efold t env ID ID on_lambda on_app where on_lambda f = ID $ \a -> unID (f a) on_app (ID f) (ID x) = ID (f x) newtype Expression t r = MkExpression (forall env. OpenExpression t env r => t) runExpression (MkExpression e) = openRun e () sym0 = Symbol FirstSym sym1 = Symbol (NextSym FirstSym) sym2 = Symbol (NextSym (NextSym FirstSym)) -- k = \x.\y -> x = \.\.1 k = MkExpression (Lambda (Lambda sym1)) -- s :: Expression ((a -> b -> c) -> (a -> b) -> a -> c); -- -- s = \x.\y.\z -> x z (y z) = \.\.\.2 0 (1 0) s = MkExpression (Lambda (Lambda (Lambda (Application (Application sym2 sym0) (Application sym1 sym0))))) test1 = (runExpression k) sym0 sym2 test2 = (runExpression k) sym2 sym0 test3 = (runExpression s) (runExpression k) (runExpression k) -- Note: That can only be the identity! -- :t test3: -- test3 :: forall r. r -> r test3' = test3 "It's the identity!!! Look at the type!!!" newtype WInt a = WInt Int unWInt (WInt v) = v depth (MkExpression e) = compute_depth e () where compute_depth t env = unWInt $ efold t env w0 w0 on_lambda on_app w0 _ = WInt 0 on_lambda f = WInt $ unWInt (f undefined) + 1 on_app (WInt x) (WInt y) = WInt $ 1 + max x y size (MkExpression e) = compute_size e () where compute_size t env = unWInt $ efold t env w0 w0 on_lambda on_app w0 _ = WInt 1 on_lambda f = WInt $ unWInt (f undefined) + 1 on_app (WInt x) (WInt y) = WInt $ 1 + x + y -- depth k ==> 2 -- depth s ==> 5 -- size k ==> 3 -- size s ==> 10