I understand that (->) a
is a higher order type of kind * -> *
, that when applied to a type argument b
gives the type a -> b
Can I write a type of kind * -> *
that when applied to c
would give a -> b -> c
?
If not, why not? Maybe using some language extensions and forall
?
This would let me write instances of Functor and Applicative (and other classes) where the functorial structure is "a -> b ->
" as in:
(<*>) :: Applicative t => t (c -> d) -> t c -> t d
(<*>) :: (a -> b -> c -> d) -> (a -> b -> c) -> a -> b -> d
This would be useful as a combinator for binary (curried) functions.
NB. Maybe this is related Functors and Applicatives for types of kind (* -> *) -> * but I'm not sure, because it went over my head :-)
No, you can't. You could imagine many language features to support this; e.g. type-level lambdas would be a natural one:
instance Functor (\c. a -> b -> c) where ...
Unfortunately, type-level lambdas would mean we have to move from first-order unification to higher-order unification during type inference, which is notably difficult. (I want to say undecidable off the top of my head, but I'm not certain of this.)
You can get halfway there if you insert an explicit type-checking hint by way of a newtype
wrapper. The standard one is Compose
:
a -> b -> c ~= Compose (a ->) (b ->) c
\c. a -> b -> c ~= Compose (a ->) (b ->)
And, indeed, the Functor
and Applicative
instances for Compose (a ->) (b ->)
are exactly the ones you would expect for \c. a -> b -> c
, at the cost of a bit of syntactic noise when creating and consuming values of this type.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With