Simply typed Lambda calculas

Question

Recently started a college module on simply typed lambda calculus, for any given example it has just been (t1->t2) or similar, I've never used such a long string of types. The question is to define a term, using as short a definition as you can manage, of type (t1→t3)→(t2→t3→t5)→t2→t1→t7. How do I start this, can I break it up into smaller types or do I have to complete it as a long type.

Answer 1

Start off by taking the type of the function apart. It is a function which takes 4 parameters and returns something of type t7.

• The 1st parameter is a function with 1 parameter of type t1, which returns type t3 => p1
• The 2nd parameter is function with 2 parameters of type t2 and t3 which returns type t5 => p2 etc.

You then need to use these parameters and additional functions (lets say f1...f4) to make the input create something of type t7. When you have something of type t7 you will just have to turn this function into simply typed lambda calculus