Dispatch a type-function on the existence (or not) of instances?

Dear all, I have been curious about the ability to detect the presence of a certain instance (ClassFoo TypeBar) in the type system. Specifically, is it possible to "dispatch" a type on the existence (or not) of such an instance. For example given two functions: withInstance :: (ClassFoo TypeBar) => TypeIfInstanceExists withoutInstance :: TypeIfInstanceDoesNotExists I would be able to consolidate them into something like this: withOrWithoutInstance :: (r ~ InstanceExists ClassFoo TypeBar, a ~ If r TypeIfInstanceExists TypeIfInstanceDoesNotExists) => a I guess what I need is: 1) A type-level "if". 2) The possibility of "converting" a constraint into a type-level bool. I am sure (1) is possible but have no idea about (2). Anyone? Best regards, Hans

I am sure that "2) The possibility of "converting" a constraint into a type-level bool." is *not* possible. And, it really shouldn't be possible. The problem has to do with modules. Suppose we have:
module A where data Foo type Magic -- invented syntax: | Show Foo = Int | otherwise = Bool
module B where import A instance Show Foo bar :: Magic bar = 3
module C where import A quux :: Magic -- no (Show Foo) here! quux = False
module D where import B import C hasSameType :: a -> a -> () hasSameType _ _ = () unit :: () unit = hasSameType bar quux
Does that last line of D type-check? `bar` and `quux` are both declared to have the same type. But, of course, they don't have the same type! Yuck. Thus, `Magic` cannot exist.
In my own work, I've often wanted something like Magic, but I've learned that whenever I start wanting Magic, what I really want is a very different design.
If you really, really want Magic and just can't live without it though, you might consider using Template Haskell. TH code can query the database of available instances and branch on the existence of an instance. See `reifyInstances`. TH can't cause the problem I described above, because the equivalent using TH would give `bar` and `quux` different types at compile time, because the TH code is fully evaluated, unlike something like `Magic` which might not be.
I hope this helps!
Richard
On Jan 31, 2014, at 12:56 PM, Hans Höglund
Dear all,
I have been curious about the ability to detect the presence of a certain instance (ClassFoo TypeBar) in the type system. Specifically, is it possible to "dispatch" a type on the existence (or not) of such an instance. For example given two functions:
withInstance :: (ClassFoo TypeBar) => TypeIfInstanceExists withoutInstance :: TypeIfInstanceDoesNotExists
I would be able to consolidate them into something like this:
withOrWithoutInstance :: (r ~ InstanceExists ClassFoo TypeBar, a ~ If r TypeIfInstanceExists TypeIfInstanceDoesNotExists) => a
I guess what I need is:
1) A type-level "if". 2) The possibility of "converting" a constraint into a type-level bool.
I am sure (1) is possible but have no idea about (2). Anyone?
Best regards, Hans _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

This makes sense, thank you for clearing it up. My problem arises from the following situation, where I want to overload t depending whether a getter is available or not. class HasTGetter a class HasTSetter a t :: HasTSetter a -> Setter a T t :: (HasTGetter a, HasTSetter a) -> Lens a T I could probably resolve the ambiguity by using a separate type function. instance HasTSetter Foo type instance LensType Foo T = Setter Foo T instance HasTGetter Bar instance HasTSetter Bar type instance LensType Bar T = Lens Bar T t :: (HasGetter a, HasSetter a) -> LensType a T Regards, Hans On 1 feb 2014, at 19:21, Richard Eisenberg wrote:
I am sure that "2) The possibility of "converting" a constraint into a type-level bool." is *not* possible. And, it really shouldn't be possible.
The problem has to do with modules. Suppose we have:
module A where data Foo type Magic -- invented syntax: | Show Foo = Int | otherwise = Bool
module B where import A instance Show Foo bar :: Magic bar = 3
module C where import A quux :: Magic -- no (Show Foo) here! quux = False
module D where import B import C hasSameType :: a -> a -> () hasSameType _ _ = () unit :: () unit = hasSameType bar quux
Does that last line of D type-check? `bar` and `quux` are both declared to have the same type. But, of course, they don't have the same type! Yuck. Thus, `Magic` cannot exist.
In my own work, I've often wanted something like Magic, but I've learned that whenever I start wanting Magic, what I really want is a very different design.
If you really, really want Magic and just can't live without it though, you might consider using Template Haskell. TH code can query the database of available instances and branch on the existence of an instance. See `reifyInstances`. TH can't cause the problem I described above, because the equivalent using TH would give `bar` and `quux` different types at compile time, because the TH code is fully evaluated, unlike something like `Magic` which might not be.
I hope this helps! Richard
On Jan 31, 2014, at 12:56 PM, Hans Höglund
wrote: Dear all,
I have been curious about the ability to detect the presence of a certain instance (ClassFoo TypeBar) in the type system. Specifically, is it possible to "dispatch" a type on the existence (or not) of such an instance. For example given two functions:
withInstance :: (ClassFoo TypeBar) => TypeIfInstanceExists withoutInstance :: TypeIfInstanceDoesNotExists
I would be able to consolidate them into something like this:
withOrWithoutInstance :: (r ~ InstanceExists ClassFoo TypeBar, a ~ If r TypeIfInstanceExists TypeIfInstanceDoesNotExists) => a
I guess what I need is:
1) A type-level "if". 2) The possibility of "converting" a constraint into a type-level bool.
I am sure (1) is possible but have no idea about (2). Anyone?
Best regards, Hans _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
Hans Höglund
-
Richard Eisenberg