3
$\begingroup$

I'm going to take the few pieces of knowledge I have about lambda calculi and ask a pair of very uninformed questions :-)

Is it possible to "embed" the corners of the lambda cube within the untyped lambda calculus?

It would seem that this might lead to a language where the programmer implements the type system in the language, rather than having it already implemented in the compiler. Also, maybe the concept of type system could be generalized to "any arbitrary compile-time or run-time constraint checking". Does such a language already exist?

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ The question is a bit unclear. You can take typed $\lambda$-calculus of any kind and just delete the types. That "embeds" it into the untyped $\lambda$-calculus. But you must be talking about something else. What exactly? $\endgroup$
    – Andrej Bauer
    Jan 16 '14 at 23:03
  • 1
    $\begingroup$ I may be totally wrong but doesn't typed lambda calculus implement the type system in the language of untyped lambda calculus, and it is the use of syntactic sugar which makes typed language calculus look like a new language. My understanding is that typed lambda calculus can be implemented from just untyped lambda calculus. $\endgroup$
    – Guy Coder
    Jan 17 '14 at 14:03
  • $\begingroup$ @AndrejBauer Hmm, perhaps I am confusing the type system in a lambda with a particular implementation of it (within a programming language) that performs type checking. I mean to express the constraints that a type system implies using the untyped lambda calculus. From Guy Coder's comment, maybe this is already the case and I just didn't realize it. $\endgroup$
    – Aaron
    Jan 17 '14 at 15:21
  • $\begingroup$ @GuyCoder Interesting, you may very well be right- I don't understand enough to say either way. Do you mean that type information is encoded in untyped lambda terms in a similar way to Church numerals, etc? (That would relate it to something I understand.) $\endgroup$
    – Aaron
    Jan 17 '14 at 15:23
  • $\begingroup$ I was hoping that @AndrejBauer would comment on my comment otherwise I will have to make is a new separate question. With regards to your statement, I believe so. Take a look at "An Introduction To Functional Programming Through Lambda Calculus by Greg Michaelson" which I added as link to the Lambda Calculus tag. It will take you some reading to understand, but it should have enough detail to answer your question. $\endgroup$
    – Guy Coder
    Jan 17 '14 at 15:34
4
$\begingroup$

As mentioned in the comments, it is possible to reduce simply typed lambda calculus to untyped lambda calculus. This is the approach associated with Alonzo Church, called "Church Types" or "intrinsic types". Here, types are embedded in the language, and are intrinsic to the language. Still, the language can be stripped of it's types.

However, it is also possible to construct simply typed lambda calculus from untyped lambda calculus. This approach is associated with Haskell Curry, called "Curry Types" or "extrinsic types". Here, types can be derived from the AST of the language.

The latter type is what you are looking for. A thorough overview of the subject is here

Improve this answer
$\endgroup$

Your Answer

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

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