3

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.)

migrated from stackoverflow.com May 29 '14 at 20:17

This question came from our site for professional and enthusiast programmers.

  • 1
    You've heard of Typed Racket, yes? The prima facie answer to your prima facie question is "Scheme has lists and numbers, because they're part of the language standard." – Robert Harvey May 29 '14 at 20:14
  • Sure, but do you understand the question? I am asking what is the underlying type system used on Racket - and, if it actually has types, why it is called untyped. – MaiaVictor May 29 '14 at 20:16
  • Scheme is an extension of untyped lambda calculus. While Untyped Lambda Calculus doesn't have any concept of types, it doesn't mean that a language built on top of it has to be untyped. – Robert Harvey May 29 '14 at 20:25
  • You might find this SO question about a section in SICP on implementing cons, car, and cdr with closures interesting: stackoverflow.com/questions/21769348/… You are essentially assuming that lists are a fundamental type when that's not necessarily true. All you really need are atoms (to contain a singular "thing") and closures. – Evicatos May 29 '14 at 23:20
  • Yes, but from a type theorist perspective, you could just say nil : List and cons : a -> List and it is now perfectly statically typed. That is what I don't get: it seems like you could infer the type of any term like that, so why not just say Scheme is statically typed? – MaiaVictor May 29 '14 at 23:30
7

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).

  • Eh, you almost have me. Your answer dances around what I think you're really trying to say. – Robert Harvey May 29 '14 at 20:50
  • @RobertHarvey What do you think that might be? – user7043 May 29 '14 at 20:59
  • ULC is untyped because it doesn't concern itself with types. Scheme is typed, even if it is loosely-typed or dynamically-typed, because in the real world we have to store and manipulate real data, rather than mathematical symbols. That Scheme is based on ULC just means that it likes some of its features. – Robert Harvey May 29 '14 at 21:01
  • 1
    @RobertHarvey That is not what I'm trying to say. My point is that "type" can mean one of two very different things. – user7043 May 29 '14 at 21:02
  • Oh. Well, there is that. – Robert Harvey May 29 '14 at 21:03
6

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

3

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.

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.