Constructing concrete types for typeclasses with GADTs

Question

The inspiration for this is creating a list of values that are instances of Show. I found the following snippet that uses GADTs to create a concrete Showable type.

data Showable where Showable :: Show a => a -> Showable

instance Show Showable where
    show (Showable x) = show x

list :: [Showable]
list = [Showable 4, Showable "hello", Showable 'a']

Then, I tried to make Showable more general by creating a type that could make any typeclass concrete.

data Concrete a where Concrete :: a b => b -> Concrete a

instance Show (Concrete Show) where
    show (Concrete x) = show x

list :: [Concrete Show]
list = [Concrete 4, Concrete "hello", Concrete 'a']

This works with the ConstraintKinds and FlexibleInstances language extensions, but in order to use Concrete to make concrete types for other typeclasses, each one would require a new instance.

Is there a way to create something similar to Concrete such that, for example, Concrete Show is automatically an instance of Show?

Since Concrete is a type constructor and Show is a type class, the expression Concrete Show isn't even legal, much less an instance of anything. I might be wrong, but I'm going to suggest you won't ever get this to work. — MathematicalOrchid
@MathematicalOrchid It already did work, with ConstraintKinds and FlexibleInstances. I added this to the question. — afuous
@MathematicalOrchid Now you can, since the kinding system allows Show :: * -> Constraint, and you can parametrize a type with such kind, as done above. — chi
Interesting. I had no idea such craziness is possible. Next they'll be adding language extensions that make the type system Turing-complete... oh, wait. — MathematicalOrchid
I don't think this is doable. It would require something like instance c (Concrete c). Also, don't forget that [Showable] is a known antipattern since it is an overcomplication of [String]. — chi

chi chi · Accepted Answer · 2016-06-29T08:31:12

It is not possible. Consider this:

instance Monoid (Concrete Monoid) where
   mappend (Concrete x) (Concrete y) = Concrete (mappend x y) -- type error!

This is a type error since x and y come from two different existential quantifications. There is no guarantee that x and y can be added together.

In other words, [Concrete [1,2], Concrete ["hello"]] has type [Concrete Monoid] but can not be summed (mconcat).

This is precisely the same problem for which, in OOP, the following base class/interface does not work:

interface Vector {
   Vector scale(double x);
   Vector add(Vector v);
}
class Vec2D implements Vector { ... }
class Vec3D implements Vector { ... }

The interface implies that a 2D vector is addable to any other vector, including a 3D one, which makes no sense. For an OOP solution, see F-bounded quantification and its related popularization callled curiously recurring template pattern.

In Haskell, we often do not need such techniques since there is no subtyping, hence two types in, say, a Vector type class are already not mixable.

class Vector a where
   scale :: Double -> a -> a
   add :: a -> a -> a
instance Vector (Vec2D) where ...
instance Vector (Vec3D) where ...

Constructing concrete types for typeclasses with GADTs

1 Answers