Composing type constructors like functions

Question

I recently came across a situation where I wanted to be able to compose type constructors in an instance declaration. I would have liked to do this:

instance (SomeClass t, SomeClass t') => SomeClass (t . t') where

with (t . t') defined such that (t . t') a = t (t' a) (so t and t' have kind * -> *. We can partially apply type constructors, like functions, so what is the reason we cannot compose them? Also, is there perhaps a workaround for what I was trying to achieve? Perhaps with equality constraints?

(I do know that Control.Compose exists, but it simply creates a newtype wrapper - I would like a type synonym).

Answer 1

(I do know that Control.Compose exists, but it simply creates a newtype wrapper - I would like a type synonym).

This is not allowed in Haskell. A type synonym must be fully applied: you can't write Compose t t', only Compose t t' a.

Allowing partially applied type synonyms would lead to type-level lambdas, which makes type inference undecidable, hence the lack of support for it in Haskell.

---

For instance, (enabling all the relevant GHC extensions)

type Compose t t' a = t (t' a)
data Proxy (k :: * -> *) = Proxy

pr :: Proxy (Compose [] [])
pr = Proxy

results in:

 Type synonym ‘Compose’ should have 3 arguments, but has been given 2
    In the type signature for ‘pr’: pr :: Proxy (Compose [] [])

Similarly,

class C k where f :: k Int -> Int
instance C (Compose [] []) where f _ = 6

yields:

Type synonym ‘Compose’ should have 3 arguments, but has been given 2
    In the instance declaration for ‘C (Compose [] [])’

Here's an example where type synonym partial application is allowed, instead (enabling LiberalTypeSynonyms):

type T k = k Int
type S = T (Compose [] [])

bar :: S -> S
bar = map (map succ)

Note however that this works only because after synonym expansion we get a fully applied type [] ([] Int) (i.e., [[Int]]). Roughly, this feature does not allow to do anything which one could have done without it, manually expanding the synonyms.