Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Can I write a higher order type for a -> b -> *?

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 :-)

like image 314
Tobia Avatar asked May 25 '17 23:05

Tobia


1 Answers

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.

like image 120
Daniel Wagner Avatar answered Nov 07 '22 02:11

Daniel Wagner