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.
Start off by taking the type of the function apart. It is a function which takes 4 parameters and returns something of type t7.
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