Hi,
In Haskell, instances of a type class can only be well-formed type
constructors, which in turn is defined by:
TC ::= T -- a type constant
| a -- a variable
| TC TC -- a type constructor application
Note there is no type constructor abstraction.
In practice, I found this rule too restrictive. For example, given:
> data T a b = ...
T, T a and T a b are all valid candidates for instance declaration, but
T _ b is not (where _ is a hole waiting for a type parameter)!
Here is an example where I need an instance declaration for T _ b:
> data T a b = T (a -> b)
>
> class Functor f where
> fmap :: (x -> y) -> f x -> f y
>
> class CoFunctor cf where
> comap :: (x -> y) -> cf y -> cf x
>
> instance Functor (T a) where
> fmap f (T g) = T (f.g)
Now I want:
> instance CoFunctor (T _ b) where
> comap f (T g) = T (g.f)
but this is invalid Haskell.
First I was attempted to write:
> type T' b a = T a b
>
> instance CoFunctor (T' b) where ...
However, this is invalid too since a type synonym must be always fully
applied in Haskell. (I guess this restriction is to ensure that a type
synonym always expands to a well-formed type constructor.)
Of course we can write:
> newtype T' b a = T' (T a b)
>
> instance CoFunctor (T' b)
but this is not quite what I want: I am still unable to use T in the
context where class CoFunctor is required.
In retrospect, I realized even the _ notation I used is not expressive
enough: when there are more than one holes, we'd like to be able to
change their order.
How about extending TC with a branch for abstraction:
TC ::= ...
| /\a. TC -- abstraction
This is too powerful and will get out of control -- we surely don't want
to give TC the full power of lambda-calculus. So let's impose a
restriction: in /\a.TC, a must occur free in TC *exactly once*. This
way, abstraction can only be used to specify with respect to which
argument a partial application is. (or I think so -- I haven't tried to
prove it.)
With the extension, we can have:
> instance CoFunctor (/\a. T a b) where ...
Why not extending Haskell to allow this? Is it just that too few people
have asked for it? Or is there any fundamental difficulty? Or is the
problem not well studied yet?
-- Zhanyong Wan
Yale University
