0
$\begingroup$

I'm looking at some lambda calculus at the moment and came across this question:

0:R

1:R

plus: R->R->R

(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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
0
$\begingroup$

While your way of calculating the types isn't quite how it works, it gives the right answer here. As you say, you end up with f 0 having type R and g 0 having type R. Since we apply f 0 to g 0, R must be of the form R -> X for some X. In other words, you have the equi-recursive type R = R -> X. Such types are almost always disallowed. Thus, this would be a type error. If R is a fixed primitive type, e.g. a type of primitive natural numbers, then it is simply not the case that R = R -> X and so you would also get a type error.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks, this is what I was thinking of when I said contradicting with the lack of recursion. So, for example $\lambda_{:T} v . v v$ is always invalid in simply typed lambda calculus, ie. we cannot find an appropriate type for T? $\endgroup$
    – Rob M
    Commented Jan 9, 2018 at 18:48
  • $\begingroup$ There's a difference between having value-level recursion, e.g. a fixed point primitive, which is quite common in simply typed lambda calculi meant for programming, and having type-level equi-recursion, which is very uncommon. Iso-recursive types, where you have to explicitly "wrap" and "unwrap" between a type and its expansion is fairly common. Equi-recursive and iso-recursive types don't require value-level recursion, though they often provide an indirect way of creating it. For the simply typed lambda calculus without equi-recursive types, $\lambda v\!:\!T.vv$ is always a type error. $\endgroup$
    – Derek Elkins left SE
    Commented Jan 9, 2018 at 18:57
  • $\begingroup$ There are other type systems that can give a type to $\lambda v\!:\!T.vv$. Intersection type systems can give it a type like $(T \& (T \to X)) \to X$. In polymorphic type systems with higher-rank types, you can set $T=\forall a.a \to a$, but the type $\forall a.a\to a$ is very strict, e.g. in many systems there is only one value for that type, the identity function. $\endgroup$
    – Derek Elkins left SE
    Commented Jan 9, 2018 at 19:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.