I'm looking at some lambda calculus at the moment and came across this question:
(lambda f:T . lambda g:U . (f 0) (g 0)) (plus 1) (plus (plus 1 1))
Is it well typed given appropriate types for T and U?
I'm new to lambda calc but I gather that we substitute (plus 1) for f and (plus (plus 1 1)) for g.
This will reduce to
(plus 1 0) (plus (plus 1 1) 0) The right hand side (plus 1 1) will reduce to an R and then we will have (plus R 0) which will reduce to an R. The left side will reduce to an R so the whole expression reduces to the form R R.
Is this correct? Then f and g are of type R -> R (from currying) to make it valid. Is it an issue that the final expression will be of the form R R. Does this mean R gets applied to R then, so R would have to be an 'automorphic' function (mapping from a type to the same type)... is this something related to not having recursion in simply typed lambda calc?