If Scheme is untyped, how can it have numbers and lists

lambdalambda-calculusracketschemetype-systems

Scheme is said to be just an extension of the Untyped Lambda Calculus (correct me if I am wrong). If that is the case, how can it have Lists and Numbers? Those, to me, look like 2 base types. So I'd say Racket is actually an extension of the Simply Typed Lambda Calculus. No?

Question:

  • Is Scheme's type system actually based or more similar to Simply Typed or Untyped Lambda Calculus?

  • In what ways does it differ from Untyped and or Simply Typed Lambda Calculus?

(The same question is valid for "untyped" languages such as Python and JavaScript – all of which look like they have base types to me.)

Best Answer

When type theorists say "typed", they mean a what most programmers call statically typed. This is due to a fundamental divide: Type theorists care about proofs and related beasts, and hence care about statements that apply to all possible executions of a program. The mere notion of a "runtime type tag" doesn't make sense to them. If a type theorist says "this has type int" they mean "I can formally proof that this only ever takes on int values".

In contrast, an untyped language is one where you can't create such a proof, because the language doesn't give you enough guarantees/information. This is the original meaning of "untyped" and it's actively used by (a minority of) people talking about type systems online. An alternative term is "unityped", because if you have to assign a type, you only have the trivial type "any value whatsoever" available.

The simply typed lambda calculus is typed in this sense, it has a static type system as you'd say. In the same sense, both Scheme and the untyped lambda calculus are untyped.

Programmers, on the other hand, primarily want to know what kind of value is in some memory location; whether this knowledge is innate in the source code for a compiler to explore and make use of, or whether it is determined at run time, is a separate decision.

In accordance with their understanding of "type", programmers have a different definition of "untyped": A system that has neither static information nor runtime tags, because there is effectively only "one type" to choose from (e.g. in Tcl, everything is a string). In this sense, the untyped lambda calculus is still untyped (everything is a function), but Scheme is, as you note, typed (though dynamically).

Related Topic