
There's a common pattern in Haskell of writing: data E where E :: C a => a -> E also written data E = forall a. C a => E a I recently uploaded a package to Hackage which uses the new ConstraintKinds extension to factor this pattern out into an Exists type parameterized on the constraint, and also for an Existential type class which can encompass these kind of types: http://hackage.haskell.org/package/exists My motivation was mostly to play with my new toys, if it turns out to be useful for anything that's a happy and unexpected bonus. Some interesting things I stumbled upon while writing it: - Did you know you can write useful existentials for Functor, Foldable, and Traversable? I sure didn't beforehand. - You can even write them for various Comonad classes, though in their case I don't think it's good for anything because you have no way to run them. - Surprisingly to me, the only * kinded class in the standardish libraries I found which is useful with existentials is Show, the * -> * kinded ones are more numerous. - I don't know if anyone's ever set out what the precise requirements are for a type class method to be useful with existentials. For example, any method which requires two arguments of the same type (the type in the class head) is clearly useless, because if you have two existentials there's no way to tell whether or not their contents were of the same type. I think this holds any time you have more than one value of the type among the method's parameters in any kind of way (even if it's e.g. a single parameter that's a list). If the type-from-the-class-head (is there a word for this?) is used in the method's parameters in a position where it's not the outermost type constructor of a type (i.e. it's a type argument), that's also no good, because there's no way to extract the type from the existential, you can only extract the value. On the other hand, in the method's return type it's fine if there are multiple values of the type-from-the-class-head (or if it's used as a type argument?), because (as long as the method also has an argument of the type) the type to put into the resulting existentials can be deduced to be the same as the one that was in the argument. But if the type-from-the-class-head is used *only* in the return type, then it's difficult to construct an existential out of the return value because the instance to use will be ambiguous. - There are a lot of ways you can write existentials, and the library only captures a small part of them. Multiparameter constraint? No go. More than one constraint? No go (though you can use Control.Constraint.Combine). More than one type/value stored? No go. Anything which doesn't exactly match the patterns data E where E :: C a => a -> E or data E a where E :: C f => f a -> E a? No go. I don't think there's any way to capture all of the possibilities in a finite amount of code. - ConstraintKinds lets you write class aliases as type synonyms, type Stringy a = (Show a, Eq a). The old way to do this is class (Show a, Eq a) => Stringy a; instance (Show a, Eq a) => Stringy a and requires UndecidableInstances. But if the alias has multiple parameters, the old way is still superior, because it can be partially applied where type synonyms can't. This is analogous to the situation with type synonyms versus newtype/data declarations, but interestingly, unlike data and newtypes, the class+instance method doesn't require you to do any manual wrapping and unwrapping, only the declaration itself is different. - One of the advantages FunctionalDependencies has over TypeFamilies is that type signatures using them tend to be more readable and concise than ones which have to write out explicit equality constraints. For example, foo :: MonadState s m => s -> m () is nicer than foo :: (MonadState m, State m ~ s) => s -> m (). But with equality superclass constraints (as of GHC 7.2), it's possible to translate from TF-form to FD-form (but not the reverse, as far as I know): class (MonadStateTF m, s ~ State m) => MonadStateFDish s m; instance (MonadStateTF m, s ~ State m) => MonadStateFDish s m. - PolyKinds only seems to be useful as long as there's no value-level representation of the polykinded type involved (it's only used as a phantom). As soon as you have to write 'a' for kind * and 'f a' for kind * -> *, you have to do the duplication manually. Is this right? - Writing this library really made me want to have a type-level "Ord instance" for constraints, more precisely a type-level is-implied-by operator. The typechecker clearly knows that Eq is-implied-by Ord, for example, and that Foo is-implied-by (Foo :&: Bar), but I have no way to ask it, I can only use (~). I tried implementing this with OverlappingInstances, but it seems to be fundamentally impossible because you really need a transitive case (instance (c :<=: d, d :<=: e) => c :<=: e) but the transitive case can't work. (My best understanding is that it's because the typechecker doesn't work forward, seeing "ah, c :<=: d and d :<=: e, therefore c :<=: e"; rather it works backwards, and sees that "c might be :<=: e, if there's a suitable d", but then it has no idea what to choose for d and goes into a loop.) Filing a feature request is in the plans. Er... </ul>. Cheers, ~g

That is a great initiative.
I didn't know about those Kind extensions that enable you to pass a
typeclass as a type parameter...
However, have you considered putting the Data.Exists.Default module in a
separate package? That would reduce the dependencies for those who just
need Exists and Existential.
2012/2/5 Gábor Lehel
There's a common pattern in Haskell of writing:
data E where E :: C a => a -> E also written data E = forall a. C a => E a
I recently uploaded a package to Hackage which uses the new ConstraintKinds extension to factor this pattern out into an Exists type parameterized on the constraint, and also for an Existential type class which can encompass these kind of types:
http://hackage.haskell.org/package/exists
My motivation was mostly to play with my new toys, if it turns out to be useful for anything that's a happy and unexpected bonus.
Some interesting things I stumbled upon while writing it:
- Did you know you can write useful existentials for Functor, Foldable, and Traversable? I sure didn't beforehand.
- You can even write them for various Comonad classes, though in their case I don't think it's good for anything because you have no way to run them.
- Surprisingly to me, the only * kinded class in the standardish libraries I found which is useful with existentials is Show, the * -> * kinded ones are more numerous.
- I don't know if anyone's ever set out what the precise requirements are for a type class method to be useful with existentials. For example, any method which requires two arguments of the same type (the type in the class head) is clearly useless, because if you have two existentials there's no way to tell whether or not their contents were of the same type. I think this holds any time you have more than one value of the type among the method's parameters in any kind of way (even if it's e.g. a single parameter that's a list). If the type-from-the-class-head (is there a word for this?) is used in the method's parameters in a position where it's not the outermost type constructor of a type (i.e. it's a type argument), that's also no good, because there's no way to extract the type from the existential, you can only extract the value. On the other hand, in the method's return type it's fine if there are multiple values of the type-from-the-class-head (or if it's used as a type argument?), because (as long as the method also has an argument of the type) the type to put into the resulting existentials can be deduced to be the same as the one that was in the argument. But if the type-from-the-class-head is used *only* in the return type, then it's difficult to construct an existential out of the return value because the instance to use will be ambiguous.
- There are a lot of ways you can write existentials, and the library only captures a small part of them. Multiparameter constraint? No go. More than one constraint? No go (though you can use Control.Constraint.Combine). More than one type/value stored? No go. Anything which doesn't exactly match the patterns data E where E :: C a => a -> E or data E a where E :: C f => f a -> E a? No go. I don't think there's any way to capture all of the possibilities in a finite amount of code.
- ConstraintKinds lets you write class aliases as type synonyms, type Stringy a = (Show a, Eq a). The old way to do this is class (Show a, Eq a) => Stringy a; instance (Show a, Eq a) => Stringy a and requires UndecidableInstances. But if the alias has multiple parameters, the old way is still superior, because it can be partially applied where type synonyms can't. This is analogous to the situation with type synonyms versus newtype/data declarations, but interestingly, unlike data and newtypes, the class+instance method doesn't require you to do any manual wrapping and unwrapping, only the declaration itself is different.
- One of the advantages FunctionalDependencies has over TypeFamilies is that type signatures using them tend to be more readable and concise than ones which have to write out explicit equality constraints. For example, foo :: MonadState s m => s -> m () is nicer than foo :: (MonadState m, State m ~ s) => s -> m (). But with equality superclass constraints (as of GHC 7.2), it's possible to translate from TF-form to FD-form (but not the reverse, as far as I know): class (MonadStateTF m, s ~ State m) => MonadStateFDish s m; instance (MonadStateTF m, s ~ State m) => MonadStateFDish s m.
- PolyKinds only seems to be useful as long as there's no value-level representation of the polykinded type involved (it's only used as a phantom). As soon as you have to write 'a' for kind * and 'f a' for kind * -> *, you have to do the duplication manually. Is this right?
- Writing this library really made me want to have a type-level "Ord instance" for constraints, more precisely a type-level is-implied-by operator. The typechecker clearly knows that Eq is-implied-by Ord, for example, and that Foo is-implied-by (Foo :&: Bar), but I have no way to ask it, I can only use (~). I tried implementing this with OverlappingInstances, but it seems to be fundamentally impossible because you really need a transitive case (instance (c :<=: d, d :<=: e) => c :<=: e) but the transitive case can't work. (My best understanding is that it's because the typechecker doesn't work forward, seeing "ah, c :<=: d and d :<=: e, therefore c :<=: e"; rather it works backwards, and sees that "c might be :<=: e, if there's a suitable d", but then it has no idea what to choose for d and goes into a loop.) Filing a feature request is in the plans.
Er... </ul>.
Cheers, ~g
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

If anyone ever says, "I'd really like to use your package if it
weren't for the dependencies", I'll very gladly remove them. (They're
used for actual instances, by the way, not just the Defaults module.)
2012/2/6 Yves Parès
That is a great initiative. I didn't know about those Kind extensions that enable you to pass a typeclass as a type parameter...
However, have you considered putting the Data.Exists.Default module in a separate package? That would reduce the dependencies for those who just need Exists and Existential.
2012/2/5 Gábor Lehel
There's a common pattern in Haskell of writing:
data E where E :: C a => a -> E also written data E = forall a. C a => E a
I recently uploaded a package to Hackage which uses the new ConstraintKinds extension to factor this pattern out into an Exists type parameterized on the constraint, and also for an Existential type class which can encompass these kind of types:
http://hackage.haskell.org/package/exists
My motivation was mostly to play with my new toys, if it turns out to be useful for anything that's a happy and unexpected bonus.
Some interesting things I stumbled upon while writing it:
- Did you know you can write useful existentials for Functor, Foldable, and Traversable? I sure didn't beforehand.
- You can even write them for various Comonad classes, though in their case I don't think it's good for anything because you have no way to run them.
- Surprisingly to me, the only * kinded class in the standardish libraries I found which is useful with existentials is Show, the * -> * kinded ones are more numerous.
- I don't know if anyone's ever set out what the precise requirements are for a type class method to be useful with existentials. For example, any method which requires two arguments of the same type (the type in the class head) is clearly useless, because if you have two existentials there's no way to tell whether or not their contents were of the same type. I think this holds any time you have more than one value of the type among the method's parameters in any kind of way (even if it's e.g. a single parameter that's a list). If the type-from-the-class-head (is there a word for this?) is used in the method's parameters in a position where it's not the outermost type constructor of a type (i.e. it's a type argument), that's also no good, because there's no way to extract the type from the existential, you can only extract the value. On the other hand, in the method's return type it's fine if there are multiple values of the type-from-the-class-head (or if it's used as a type argument?), because (as long as the method also has an argument of the type) the type to put into the resulting existentials can be deduced to be the same as the one that was in the argument. But if the type-from-the-class-head is used *only* in the return type, then it's difficult to construct an existential out of the return value because the instance to use will be ambiguous.
- There are a lot of ways you can write existentials, and the library only captures a small part of them. Multiparameter constraint? No go. More than one constraint? No go (though you can use Control.Constraint.Combine). More than one type/value stored? No go. Anything which doesn't exactly match the patterns data E where E :: C a => a -> E or data E a where E :: C f => f a -> E a? No go. I don't think there's any way to capture all of the possibilities in a finite amount of code.
- ConstraintKinds lets you write class aliases as type synonyms, type Stringy a = (Show a, Eq a). The old way to do this is class (Show a, Eq a) => Stringy a; instance (Show a, Eq a) => Stringy a and requires UndecidableInstances. But if the alias has multiple parameters, the old way is still superior, because it can be partially applied where type synonyms can't. This is analogous to the situation with type synonyms versus newtype/data declarations, but interestingly, unlike data and newtypes, the class+instance method doesn't require you to do any manual wrapping and unwrapping, only the declaration itself is different.
- One of the advantages FunctionalDependencies has over TypeFamilies is that type signatures using them tend to be more readable and concise than ones which have to write out explicit equality constraints. For example, foo :: MonadState s m => s -> m () is nicer than foo :: (MonadState m, State m ~ s) => s -> m (). But with equality superclass constraints (as of GHC 7.2), it's possible to translate from TF-form to FD-form (but not the reverse, as far as I know): class (MonadStateTF m, s ~ State m) => MonadStateFDish s m; instance (MonadStateTF m, s ~ State m) => MonadStateFDish s m.
- PolyKinds only seems to be useful as long as there's no value-level representation of the polykinded type involved (it's only used as a phantom). As soon as you have to write 'a' for kind * and 'f a' for kind * -> *, you have to do the duplication manually. Is this right?
- Writing this library really made me want to have a type-level "Ord instance" for constraints, more precisely a type-level is-implied-by operator. The typechecker clearly knows that Eq is-implied-by Ord, for example, and that Foo is-implied-by (Foo :&: Bar), but I have no way to ask it, I can only use (~). I tried implementing this with OverlappingInstances, but it seems to be fundamentally impossible because you really need a transitive case (instance (c :<=: d, d :<=: e) => c :<=: e) but the transitive case can't work. (My best understanding is that it's because the typechecker doesn't work forward, seeing "ah, c :<=: d and d :<=: e, therefore c :<=: e"; rather it works backwards, and sees that "c might be :<=: e, if there's a suitable d", but then it has no idea what to choose for d and goes into a loop.) Filing a feature request is in the plans.
Er... </ul>.
Cheers, ~g
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Work is punishment for failing to procrastinate effectively.

Hi, Gábor Lehel wrote:
data E = forall a. C a => E a
I don't know if anyone's ever set out what the precise requirements are for a type class method to be useful with existentials.
More than you seem to think. For example: data Number = forall a . Num a => Number a foo :: Number -> Number foo (Number x) = Number (x * x + 3) So the binary operation (*) can be used. Note that from a type-checking perspective, the pattern match on (Number x) also extracts the type, which is then available when checking the right-hand side. Tillmann

2012/2/6 Tillmann Rendel
Hi,
Gábor Lehel wrote:
data E = forall a. C a => E a
I don't know if anyone's ever set out what the precise requirements are for a type class method to be useful with existentials.
More than you seem to think. For example:
data Number = forall a . Num a => Number a
foo :: Number -> Number foo (Number x) = Number (x * x + 3)
So the binary operation (*) can be used.
Note that from a type-checking perspective, the pattern match on (Number x) also extracts the type, which is then available when checking the right-hand side.
I think what I really meant to say by "useful with exisentials" was "you can write an instance for the existential which forwards to the instance wrapped by the existential and it will be useful", but you're quite right to point out that these are not the same.

On 02/06/2012 03:32 AM, Gábor Lehel wrote:
There's a common pattern in Haskell of writing:
data E where E :: C a => a -> E also written data E = forall a. C a => E a
I recently uploaded a package to Hackage which uses the new ConstraintKinds extension to factor this pattern out into an Exists type parameterized on the constraint, and also for an Existential type class which can encompass these kind of types:
http://hackage.haskell.org/package/exists
My motivation was mostly to play with my new toys, if it turns out to be useful for anything that's a happy and unexpected bonus.
Some interesting things I stumbled upon while writing it:
[snip]
- One of the advantages FunctionalDependencies has over TypeFamilies is that type signatures using them tend to be more readable and concise than ones which have to write out explicit equality constraints. For example, foo :: MonadState s m => s -> m () is nicer than foo :: (MonadState m, State m ~ s) => s -> m (). But with equality superclass constraints (as of GHC 7.2), it's possible to translate from TF-form to FD-form (but not the reverse, as far as I know): class (MonadStateTF m, s ~ State m) => MonadStateFDish s m; instance (MonadStateTF m, s ~ State m) => MonadStateFDish s m. Even better, you can write
type ExistentialWith c e = (Existential e, c ~ ConstraintOf e) instead of class (Existential e, c ~ ConstraintOf e) => ExistentialWith c e instance (Existential e, c ~ ConstraintOf e) => ExistentialWith c e and drop UndecidableInstances.

On Tue, Feb 7, 2012 at 7:23 AM, Mikhail Vorozhtsov
Even better, you can write
type ExistentialWith c e = (Existential e, c ~ ConstraintOf e)
instead of
class (Existential e, c ~ ConstraintOf e) => ExistentialWith c e instance (Existential e, c ~ ConstraintOf e) => ExistentialWith c e
and drop UndecidableInstances.
I actually mentioned this in the preceding point of the [snip]. The problem is that it's not even better because you can't partially apply it.

On 02/07/2012 04:05 PM, Gábor Lehel wrote:
On Tue, Feb 7, 2012 at 7:23 AM, Mikhail Vorozhtsov
wrote: Even better, you can write
type ExistentialWith c e = (Existential e, c ~ ConstraintOf e)
instead of
class (Existential e, c ~ ConstraintOf e) => ExistentialWith c e instance (Existential e, c ~ ConstraintOf e) => ExistentialWith c e
and drop UndecidableInstances.
I actually mentioned this in the preceding point of the [snip]. The problem is that it's not even better because you can't partially apply it. Ah, sorry, I got sloppy. Have you encountered situations where partial application of such "constraint aliases" becomes a problem?

2012/2/7 Mikhail Vorozhtsov
Ah, sorry, I got sloppy. Have you encountered situations where partial application of such "constraint aliases" becomes a problem?
In the particular case of the Existential class I'm not sure (it's hard to imagine a real-world application for it in the first place), but, in general, yes: the (:&:) combinator from Control.Constraint.Combine depends on it, for example. You want to be able to write: type MyExists = Exists1 (MonadState A :&: MonadWriter B :&: MonadReader C) That's a bad example because monads aren't very useful with existentials, but you get the idea. For ExistentialWith it might not particularly matter, but for client code the class+instance way is all advantage and no drawback, so I see no reason not to prefer it.

Are there documentation on constraints being types, how they can be
declared/handled and what are the interests?
2012/2/7 Mikhail Vorozhtsov
On 02/06/2012 03:32 AM, Gábor Lehel wrote:
There's a common pattern in Haskell of writing:
data E where E :: C a => a -> E also written data E = forall a. C a => E a
I recently uploaded a package to Hackage which uses the new ConstraintKinds extension to factor this pattern out into an Exists type parameterized on the constraint, and also for an Existential type class which can encompass these kind of types:
http://hackage.haskell.org/**package/existshttp://hackage.haskell.org/package/exists
My motivation was mostly to play with my new toys, if it turns out to be useful for anything that's a happy and unexpected bonus.
Some interesting things I stumbled upon while writing it:
[snip]
- One of the advantages FunctionalDependencies has over TypeFamilies
is that type signatures using them tend to be more readable and concise than ones which have to write out explicit equality constraints. For example, foo :: MonadState s m => s -> m () is nicer than foo :: (MonadState m, State m ~ s) => s -> m (). But with equality superclass constraints (as of GHC 7.2), it's possible to translate from TF-form to FD-form (but not the reverse, as far as I know): class (MonadStateTF m, s ~ State m) => MonadStateFDish s m; instance (MonadStateTF m, s ~ State m) => MonadStateFDish s m.
Even better, you can write
type ExistentialWith c e = (Existential e, c ~ ConstraintOf e)
instead of
class (Existential e, c ~ ConstraintOf e) => ExistentialWith c e instance (Existential e, c ~ ConstraintOf e) => ExistentialWith c e
and drop UndecidableInstances.
______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe

On 02/07/2012 06:49 PM, Yves Parès wrote:
Are there documentation on constraints being types, how they can be declared/handled and what are the interests? The GHC User's Guide has (somewhat short) section http://www.haskell.org/ghc/docs/latest/html/users_guide/constraint-kind.html
Blog posts: http://blog.omega-prime.co.uk/?p=127 http://comonad.com/reader/2011/what-constraints-entail-part-1/
participants (4)
-
Gábor Lehel
-
Mikhail Vorozhtsov
-
Tillmann Rendel
-
Yves Parès