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.)
8
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).
8
Untyped Lambda Calculus is untyped, because it doesn’t concern itself with types. Untyped Lambda Calculus is not a practical programming language, but merely a foundation for a practical programming language.
Scheme is typed, because in the real world we have to store and manipulate real data, rather than mathematical symbols. That Scheme is based on the Untyped Lambda Calculus just means that it likes some of its features.
If you want to find out more about Scheme’s dynamic type system, you can read http://www.r6rs.org/final/html/r6rs/r6rs-Z-H-2.html#node_toc_node_sec_1.1
0
The simple answer is that Scheme is not untyped: as you noticed, Scheme programs can use values of several useful types. Still, people do mean something when they say Scheme is untyped, they mean something that is better expressed by saying that Scheme has a dynamic type system. Let me (eventually) explain.
When people say “the untyped lambda calculus”, they call it untyped because all the values it deals with are of the same type: combinators (you may have heard them called “functions”, too). Programming in such a language feels dangerous because you have to keep straight in your head what kind of thing you wanted to represent with each value. The system has no built in help to catch your errors.
Languages people actually program in tend[^1] to have more help telling different sort of values apart, this extra help is in the form of (1) a richer collection of types for the values the language lets you talk about and (2) error messages you get when you attempt to apply an operation to a value of a type for which the operation is not defined.
In some language implementations, programs can be compiled or preprocessed in some way prior to being run. If you get error messages about using values of the wrong type during this compilation phase, before running your program, the implementation is said to use static typing.
If either (1) there is no compilation or preprocessing phase or (2) there is but you still only get error messages about using values of the wrong type during the running of your program, then the implementation is said to use dynamic typing.
Most (all?) Scheme implementations use a dynamic typing system. There are languages fairly similar to Scheme which have an implementation using static typing, such as Typed Racket.
[^1]: There are languages that people have actually used to make software where all values are essentially of the same type, such as most computer’s native machine languages, assembly languages and BCPL.