Derive Haskell Type and Implementation (<*>) (<*>)

Question

I'm a newbie just starting to learn Haskell, so please bear with me if I ask stupid questions.

I recently came across questions in SO, demonstrating how to infer the type and implementation of functions and expressions (questions such as

How can I understand "(.). (.)"?

&

Composition of the Haskell function, type (.) (.) And how it is presented )

I find the answers very inspiring

Then I will try to come up with some exercises for myself to make sure that I know how to apply these methods.

Then I myself came up with this expression: (<*>)(<*>) , which I do not know how to solve.

In GHCi, it gives a type signature like:

 (<*>)(<*>) :: Applicative f => (f (a -> b) -> fa) -> f (a -> b) -> fb 

but my problem is how could I start with

 (<*>) :: Applicative f => f (a -> b) -> fa -> fb 

and get the type signature given by GHCi?

In addition, based on the type signature, how will the implementation be implemented (<*>)(<*>) = ?? ?

I am stuck and cannot resolve this with methods such as reinstalling terms, etc. I don’t even know where to start.

Did anyone help me?

Thank you so much

note **: the expression (<*>)(<*>) really has no special meanings, it's just an exercise that I come up with for myself by chance

Answer 1

First of all, write a type (<*>) with two disjoint sets of type variables:

 (<*>) :: (Applicative f) => f (a -> b) -> fa -> fb (<*>) :: (Applicative g) => g (c -> d) -> gc -> gd 

If we want to use the second with the first as an argument, we need

 g (c -> d) ~ f (a -> b) -> fa -> fb 

getting

 g ~ (f (a -> b) ->) or, ((->) (f (a -> b)) ) c ~ fa d ~ fb 

and note that the choice of g indeed an applicative functor: this is the non-novelty of the applicative Reader (f (a -> b)) .

And so the application is of type

 gc -> gd 

which we now know how

 (f (a -> b) -> fa) -> (f (a -> b) -> fb) 

qed

Answer 2

So we have a function

 (<*>) :: Applicative f => f (a -> b) -> fa -> fb 

and apply <*> :: Applicative g => g (c -> d) -> gc -> gd (I replaced the type variables because they have different meanings in the internal and external <*> of (<*>)(<*>) . If we applied the second <*> to the first <*> , then the second <*> must be of type f (a -> b) . Thus, we have the following equation for types:

 g (c -> d) -> gc -> gd = f (a -> b) 

But g (c -> d) -> gc -> gd is the syntactic sugar for (->) (g (c -> d)) (gc -> gd) . So:

 (->) (g (c -> d)) (gc -> gd) = f (a -> b) 

Constructors of both types and parameter types of both sides must be equal, therefore:

 (->) (g (c -> d)) = f 

and

 (gc -> gd) = (a -> b) 

which means that a = gc and b = gd .

Now we see that the return value of the first (<*>) is equal to

 fa -> fb = ((->) (g (c -> d)) (gc)) -> ((->) (g (c -> d)) (gd)) = (g (c -> d) -> gc) -> (g (c -> d) -> gd) 

which coincides with (f (a -> b) -> fa) -> f (a -> b) -> fb modulo renaming variables.

The tricky part in this example is that (->) (g (c -> d)) is applicative (just like any other (->) e ).

Answer 3

Also, based on the type signature, how is the implementation (<*>)(<*>) = ?? will be?

It is easier to reverse the order (first find the implementation, and then enter its type).

Applicative instance for functions

 instance Applicative ((->) a) where pure = const (<*>) fgx = fx (gx) 

So, simply replacing <*> with f in the above definition, (<*>) (<*>) - \gx -> x <*> gx . Or after the alpha transform \gh -> h <*> gh .

Since the first argument (<*>) is h , it must be of type h :: f (a -> b) for some a and b , where f is in Applicative .

Since g takes h as an argument, it must be of type g :: f (a -> b) -> c for some c .

Since the first argument (<*>) , h is of type f (a -> b) , and the second argument (<*>) is gh , its type must be gh :: fa , because

 (<*>) :: f (a -> b) -> fa -> fb 

Since g :: f (a -> b) -> c and gh :: fa ,

 h :: f (a -> b) g :: f (a -> b) -> c gh :: fa , c ~ fa (!) 

Since h is of type f (a -> b) , h <*> (whatever :: fa) is of type fb .

And generally speaking:

 h :: f (a -> b) g :: f (a -> b) -> fa h <*> gh :: fb 

So we have

 \gh -> h <*> gh :: (f (a -> b) -> fa) -> f (a -> b) -> fb 

Answer 4

As an exercise, narrowing it down to functions, where <*> is just an S- combinator,

 Prelude> let sfgx = fx (gx) Prelude> :tss ss :: ((t -> t1 -> t2) -> t -> t1) -> (t -> t1 -> t2) -> t -> t2 -- g2 g4 g2 g1 -- g3 g3 -- g5 -- g6 

It is important to know that arrows in types are associated on the right, therefore ((t -> t1 -> t2) -> t -> t1) in fact ((t -> t1 -> t2) -> (t -> t1)) , and (t -> t1 -> t2) - (t -> (t1 -> t2)) .

Implementation:

 g6 g5 g3 t :: t2 g3 t t1 :: t2 -- need t1 g5 g3 t :: t1 g3 t (g5 g3 t) :: t2 -- so, hfgx = gx (fgx) 

So, when we have a type, it's just a matter of connecting wires, so to speak, or combining Lego bricks. We are trying to see which combinations of these entities (arguments) are of what type, and use them in the following combinations if they are useful for obtaining the desired type of output ( t2 , above).

Similarly

 Prelude Control.Applicative> :t (<*>) (<*>) (<*>) (<*>) :: (Applicative f) => (f (a -> b) -> fa) -> f (a -> b) -> fb -- f fg Prelude Control.Applicative> :t let axa f fg = fg <*> f fg in axa let axa f fg = fg <*> (f fg) in axa :: (Applicative f) => (f (a -> b) -> fa) -> f (a -> b) -> fb