How to define a function based on its type?-CodePudding

I'm trying to define a simple Haskell function with the type (m -> n -> l) -> (m -> n) -> m -> l. I thought that it needs be to defined as f g h x = f g (h x), but apparently that's not true. How could I correct this function?

CodePudding user response：

Based on the signature, the only sensical implementation is:

f :: (m -> n -> l) -> (m -> n) -> m -> l
f g h x = g x (h x)

This makes sense since we are given two functions g :: m -> n -> l and h :: m -> n, and a value x :: m. We should construct a value with type l. The only way to do this is to make use of the function g. For the parameter with type m we can work with x, for the second parameter we need a value of type n, we do not have such value, but we can construct one by applying h on x. Since h x has type h x :: n, we thus can use this as second parameter for g.

This function is already defined: it is a special case of (<*>) :: Applicative f => f (n -> l) -> f n -> f l with f ~ (->) m.

Djinn is a tool that reasons about types and thus is generating function definitions based on its signature. If one queries with f :: (m -> n -> l) -> (m -> n) -> m -> l, we get:

f :: (m -> n -> l) -> (m -> n) -> m -> l
f a b c = a c (b c)

which is the same function (except that it uses other variable names).

CodePudding user response：

f :: (m -> n -> l) -> (m -> n) -> m -> l
f    g                h           x  = _

Now you need to use the arguments in some way.

   g (_ :: m) (_ :: n) :: l
   h (_ :: m) :: n
   x :: m

Both g and h need a value of type m as their first argument. Well, luckily we have exactly one such value, so it's easy to see what to do.

   g x (_ :: n) :: l
   h x :: n
   x :: m

So now g still needs a value of type n. Again we're lucky, because applying h to x has produced such a value.

   g x (h x) :: l
   h x :: n
   x :: m

Ok, and there we now have something of type l, which is what we needed!

f g h x = g x (h x)

CodePudding user response：

f :: (m -> n -> l) -> (m -> n) -> m -> l
f    g                h           x  = l
  where
  l =

what can produce an l for us? only g:

which takes two parameters, an m and an n,

m n

but where can we get those? Well, m we've already got,

  m = x

and n we can get from h,

  n = h

which needs an m

and where do we get an m? We've already got an m!