I was continuing the exploration of lambda world this summer. When I take a look at the simply typed lambda calculus, it looks like there is no use for usual chuch numerals and boolean forms anymore. If types are declared in the environment, how would you actually implement it without referring to the internal types of the implementing language?

Other way of asking it is that if the application ((L x:int x) 1) is replaced with a chuch numeral instead of 1, how would it be possible to determine, if the chuch number is int indeed?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.