CODEWITHSUNDEEP
haskelltypesfunctional-programmingml
henry
henry

Reputation: 185

from types to write a function that satisfies the types

This question is taken from an exam. I don't know how to do that. :-(

Question: Give an example of a haskell or ml function whose type is

( a -> b ) -> ( c -> a ) -> c -> b

How to do that?

Upvotes: 1

Views: 163

Answers (3)

Luis Casillas
Luis Casillas

Reputation: 30227

The other answers so far don't actually show the logical procedure for doing this in general. I won't show it in 100% detail either, but I'll give an example of it.

The "deep" trick to this is that finding a function of a given type is equivalent proving a a logical theorem. Using a form of Lemmon's System L (a friendlier form of natural deduction used in some beginning logic courses), your example would go like this:

Theorem:  ??? :: (a -> b) -> (c -> a) -> c -> b

1.                 f :: a -> b  (aux. assumption)
2.                 g :: c -> a  (aux. assumption)
3.                 x :: c       (aux. assumption)
4.               g x :: a       (2, 3, -> elim; assumes 2, 3)
5.           f (g x) :: b       (1, 4, -> elim; assumes 1, 2, 3)
6.     \x -> f (g x) :: c -> b  (3, 4, -> intro; discharges 3, assumes 1, 2)

7.   \g x -> f (g x) :: (c -> a) -> c -> b
                        (2, 6, -> intro; discharges 2, assumes 1)

8. \f g x -> f (g x) :: (a -> b) -> (c -> a) -> c -> b  
                        (1, 7, -> intro; discharges 1)

The idea here is that there is a tight correspondence between functional programming languages and logic, such that:

  1. Types correspond to logical propositions
  2. Function definitions correspond to logical proofs
  3. Logical proof rules correspond to rules on how to construct programming language expressions.

So the "auxiliary assumption" logical proof rule (steps 1-3) corresponds to introducing a fresh free variable. The implication elimination rule (steps 4-5, a.k.a. "modus ponens") corresponds to function application. The implication introduction rule (steps 6-8, a.k.a. "hypothetical reasoning") corresponds to lambda abstraction. The concept of discharging auxiliary assumptions corresponds to binding free variables. The concept of a proof with no premises corresponds to the concept of an expression with no free variables.

Upvotes: 4

Daniel Fischer
Daniel Fischer

Reputation: 183873

What meaningful function could have the type mystery :: ( a -> b ) -> ( c -> a ) -> c -> b?

Let's see, what could

mystery f g x

be?

It has three things to work with,

  • one value x of type c,
  • one function g of type c -> a and
  • one function f of type a -> b.

It shall produce a value of type b.

The only argument that has anything to do with b is the function f, so the result must be f ???.

What can be the argument of f here? It must have type a, and the only way to produce a value of that type from the given arguments (ignoring bottoms, undefined, error "foo") is applying g to something, so it must be

mystery f g x = f (g ??)

But what could g be applied to? That must be a value of type c. Apart from bottoms, the only value of type c that can be constructed from the arguments is x, so

mystery f g x = f (g x)

must be function composition (or undefined).

Upvotes: 7

Pubby
Pubby

Reputation: 53017

That function is the function composition operator, and by typing the function's type into Hoogle you could find that out: http://www.haskell.org/hoogle/?hoogle=%28+a+-%3E+b+%29+-%3E+%28+c+-%3E+a+%29+-%3E+c+-%3E+b++

You can then click to show the source:

(.)    :: (b -> c) -> (a -> b) -> a -> c
(.) f g = \x -> f (g x)

Upvotes: 2

Related Questions