On Wednesday 24 April 2013, 10:35:34, gs wrote:

Daniel Fischer writes:

...

Use a GADT,

{-# LANGUAGE GADTs #-}

data Source x y where

Source :: Variable v => { bindings :: v [Binding a], var :: v a }

-> Source v a

I tried this, but every place that I remove the restriction Variable v => from something using Source, I get an error No instance for (Variable v) ...

Sounds like you're not pattern-matching on the `Source` constructor. Can you post some example code?

On Wednesday 24 April 2013, 12:27:23, gs wrote:

Daniel Fischer writes:

...

Can you post some example code?

http://code.accursoft.com/binding/src/c13ccbbec0ba8e326369ff2252863f20a891ef 76/binding-core/src/Data/Binding/Simple.hs

http://code.accursoft.com/binding/src/c13ccbbec0ba8e326369ff2252863f20a891ef 76/binding-core/src/Data/Binding/List.hs

I meant example code using a GADT for Source, and not DatatypeContexts; and some function where you still need the context.

On Wednesday 24 April 2013, 13:25:01, gs wrote:

Daniel Fischer writes:

...

I meant example code using a GADT for Source, and not DatatypeContexts; and some function where you still need the context.

OK, here are some truncated instances/functions:

data Source v a where Source :: Variable v => {bindings :: v [Binding a] ,var :: v a} -> Source v a

instance Variable v => Variable (Source v) where newVar a = do bindings <- newVar [] v <- newVar a return $ Source bindings v

instance Variable v => Bindable (Source v) where bind (Source bindings var) extract target apply = do let binding = Binding extract target apply --update the new binding a <- readVar var

Removing the `Variable v` context from instance declarations is at least tricky. I don't think you can do it at all here. For the context to become available, you need to pattern-match, but in `newVar`, the `Source` appears only as the result. Therefore you need the `Variable v` context to be able to write v <- newVar a Consequently, you can't have an instance Variable (Source v) where ... without context, and since `Variable b` is a superclass constraint on `Bindable b`, you need something that guarantees that `Source x` (resp. `BindingList x`) has a `Variable` instance.

data BindingList v a where BindingList :: Variable v => {source :: Source v a, list :: v [v a],pos

:: v Int} -> BindingList v a

fromBindingList :: Variable v => BindingList v a -> IO [a] fromBindingList b = do update b readVar (list b) >>= mapM readVar

You're not pattern-matching on the constructor. I wrote that you have to do that to make the context available:

...

The `Variable v` context becomes available by pattern-matching on the constructor `Source` (but not by using the field names to deconstruct a value of type `Source v a`!).

Pattern-matching, fromBindingList :: BindingList v a -> IO [a] fromBindingList b@(BindingList s l p) = do update b readVar l >>= mapM readVar removes the need to mention the `Variable v` context.

On Wednesday 24 April 2013, 14:19:35, gs wrote:

So as far as removing redundant code is concerned, this can't really be done?

That depends. Your example is not well-suited for that. In other situations, you can get rid of contexts well.

The instance declarations still need the redundant context,

Well, the context is not redundant, that's the crux. You can specify the type `Source v a` even when there is no `Variable v` instance [whether you use DatatypeContexts - which, again, are pretty useless because they don't do what one would expect - or GADTs]. And such a type is inhabited by bottom, you just can't create non-bottom values of such a type. Hence the `Variable v` context gives additional information that is needed for the instance. If you had a `v a` as argument in all methods of `class Variable v`, you could write the instance Variable (Source v) where ... without the `Variable v` context by pattern-matching on `Source` to make the `v` instance available (when using GADTs), then you wouldn't need the `Variable v` context on the `Bindable` instance either (similarly for BindingList). But to have a usable `newVar`, you need the context, and that propagates.

and function definitions need a redundant pattern-matching instead of a redundant context.

The pattern-matching isn't redundant either. But all in all, basically you have the choice between adding a context or pattern-matching for stuff like that.

On Wednesday 24 April 2013, 16:45:35, gs wrote:

Daniel Fischer writes:

...

Well, the context is not redundant, that's the crux.

You can specify the type `Source v a` even when there is no `Variable v` instance [whether you use DatatypeContexts - which, again, are pretty useless because they don't do what one would expect - or GADTs]. And such a type is inhabited by bottom, you just can't create non-bottom values of such a type.

Hence the `Variable v` context gives additional information that is needed

for

...

the instance.

I'm not following - perhaps you could give a practical example? I'm trying to understand the flaw in this:

1) The compiler sees that a Source v a can only be created when v is a variable.

No, that is the catch: undefined :: Source NotAnInstanceOfVariable Int is possible.

2) Whenever Source v a is used, the compiler should understand that v is a variable without me having to remind it.

But when you use the value constructor, foo (Source list var) = ... you know that the `v` parameter of the type must have a Variable instance. When you use a GADT, the compiler knows that too and can use that fact, when you use DatatypeContexts, the compiler can't use that knowledge (even though it has the knowledge). The point is that the type class dictionary is required to use the class methods, and with a GADT, the dictionary is bundled with the constructor, so pattern-matching makes the dictionary available. Not so with DatatypeContexts, hence the dictionary must be explicitly passed with the context on the function. Did I already mention that DatatypeContexts are fairly useless and have therefore been removed from the language?

On Wednesday 24 April 2013, 18:34:07, gs wrote:

Daniel Fischer writes:

...

No, that is the catch:

undefined :: Source NotAnInstanceOfVariable Int

is possible.

OK, I've got that. Now let's say that

data Source v a = Variable v => Source {bindings :: v [Binding a], var :: v a} or data Variable v => Source v a = Source {bindings :: v [Binding a], var :: v a}

instance Variable (Source v) where newVar a = do bindings <- newVar [] v <- newVar a return $ Source bindings v

was allowed - then newVar (undefined :: Source NotAnInstanceOfVariable Int) would then attempt newVar (?? :: NotAnInstanceOfVariable), which doesn't type check, because newVar only works on Variables.

The type annotations here are wrong, since newVar :: a -> IO (v a) But yes, the problem is that the `newVar` implementation for `Source` uses the `newVar` implementation for `v`, hence newVar :: a -> IO (Source NotAnInstance Int) would be a type error. If the type was changed to newVar :: v a -> a -> IO (v a) newVar dummy value = old_implementation_ignoring_dummy you could write an instance Variable (Source v) where newVar (Source _ _) value = do binds <- newVar [] v <- newVar value return (Source binds v) with the GADT, since you get the Variable instance of the `v` parameter by pattern-matching on the dummy argument. For some Source NotAnInstance whatever type (such a type has no non-bottom values), `newVar` would be undefined.

Is this correct? If that's the only problem, it doesn't seem like much of a loss, as even with the type context, undefined :: Source SomeInstanceOfVariable Int isn't going to be of much use either.

The problem is that you can only write a useful instance if you can somehow access a useful Variable instance for the `v` parameter. Without an instance context or pattern-matching, the only possible implementations are variants of undefined.

On Thursday 25 April 2013, 08:03:25, gs wrote:

Daniel Fischer writes:

...

...

You've mentioned GADT a few times, but I can't find a case where it's different to regular datatypes.

data Foo a = Eq a => Foo a

seems to have the same effect as

data Foo a where Foo a :: Eq a => a -> Foo a

Both remember the Eq constraint if I pattern match on the constructor, and both ignore it otherwise.

Oy, sorry, I didn't look properly and moved the constraint before the datatype name (data Eq a => Foo a = Foo a) in my brain, which would be a datatype context. The data Foo a = Eq a => Foo a syntax (requires ExistentialQuantification or GADTs) is indeed equivalent to the GADT syntax or existential quantification. Oh well, at least the part explaining how that requires pattern matching to make the context available remains useful.

On Wednesday 24 April 2013, 18:39:15, gs wrote:

Daniel Fischer writes:

...

The point is that the type class dictionary is required to use the class methods, and with a GADT, the dictionary is bundled with the constructor, so pattern-matching makes the dictionary available.

Not so with DatatypeContexts, hence the dictionary must be explicitly passed with the context on the function.

So is this more of an implementation issue? No "real" ill-typed programs will get through the type checker if the compiler could remember the type dictionary without pattern-matching or explicit context?

It's an implementation issue, yes. But DatatypeContexts were specified so that an implementation wasn't allowed to make the dictionary available without context. I don't remember the details, but there are good reasons why GADTs make the dictionaries only available on pattern-matching, part of it is that with GADTs, you get type refinement, the constructor matched against is used to further refine and restrict or instantiate type variables in the function signature. It could work without pattern-matching for single-constructor GADTs, I think, but that would require a special case for dubious benefit.