5 ms·

And of course, it is not "untyped". It is dynamically typed.

by _ph_ 10y ago

rayiner 10y ago
PL theorists generally talk about whether or not syntactic terms (as opposed to runtime values) have types. Scheme is untyped by that definition.
- klibertp 10y ago
  PL theorists - from what I saw, not being one - prefer the term "unityped". It's not true that there are no (static!) types - there is a single, unnamed type which contains all possible values.
  - kazinator 10y ago
    PL theorists who know what they are talking about know that this is false, because the actual diverse types of those values can be reasoned about at compile time. Such a "unityped" program is made up of syntax. We can reason about an expression more deeply than just "it returns a value" and we can do so statically. For instance in Lisp we know more about an expression like (cons 1 2) than that it returns a value. We know statically that it returns a cons. From that we can infer that (+ (cons 1 2) 3) is not well-typed. Type isn't just an implementation system; it's how we can reason about the program, as a mathematical object. The reasoning which informs us that (+ (cons 1 2) 3) is not well-formed without evaluating it, has to do with type. How we implement values (using a generic "cell" that is type-tagged) is just a convenience. We can get things working without being concerned for up-front type checking. It also represents the philosophy that type is innate to objects (not just a syntactic property of programs). A piece of compiled code can have a type passed into it which didn't exist when that code was compiled, and sensible things can happen anyway.
    - tel 10y ago
      It's not false, it's just unspecified. If you hand me scheme I can provide it a unitype system without conflict. If you hand me Haskell I cannot because the language has explicitly said that uncheckable statements are invalid. You can of course go further with your static analysis—a language may support many type systems in principle regardless of what the compiler accepts.
  - szemet 10y ago
    It depends on the context. I guess rayiner has referred to "untyped lambda calculus". Thats not a bad name as it is self consistent - there are no type expressions in that language. If you say that it is actally "unityped" it is (just) your (semantical) categorization looking at it from a higher level perspective. Of course on the other side whole numbers were just "number"-s, before fractionals came, so in the end it may be ok to introduce higher level perspective in naming just to diferrentiate better. :)
  - deleted 10y ago
    [deleted]
- kazinator 10y ago
  PL theorists don't get own the definition of what "type" means. Type pervades computing. A directory is a different type from a file or character device. A JPEG is a different file type from a PNG. You have MIME types in your e-mail. An ICMP packet is a different type from a TCP datagram. Machine language instruction sets have types: pointers, signed and unsigned words of various sizes, floating-point values. "Type" is a very broadly encompassing word. What all notions of type have in common is that it refers to some representation by whose rules some digital bits are interpreted to have a meaning (in some context which somehow establishes which rules apply).
  - rayiner 10y ago
    > PL theorists don't get own the definition of what "type" means. Every field has its terms of art. "Type" is a term of art in PL theory; PL theorists are entitled to define it how they want. Of course you can use the word however you want, but you can't complain if that non-standard usage results in miscommunication with others. Besides that, it's very useful to able to talk about the "types" of syntactic terms as distinct from the "types" of runtime values. You can easily reason about syntactic types. You can, for example, use syntactic types to resolve syntax ambiguities (as in C++) or prove program properties. Runtime "types" are much less useful to PL theorists because it's hard to reason about them.
  - noblethrasher 10y ago
    A PL theorist would note that most of the time when people talk about ‘types’, that they really mean ‘classes’, and that all of those things your mentioned would be considered to be the latter. Types are rather the elements of your program that correspond directly to logical propositions (which your program proves to be true).
    - kazinator 10y ago
      In software engineering, programs are usually not constructed to prove anything; this claim is just the consequence of an equivalence between logic and static typing (Curry-Howard). Programming languages do not make very good logic systems in spite of the isomorphism. They are not designed to be expressive that way. The logic system exhibited by the type system is geared toward proving trivialities about the program: mainly that its run-time translation won't misuse data. Plus it supports certain devices like polymporphism and pattern matching and whatnot. Now instead of writing a useful program, we can exploit the type system for doing logic in a separate domain, detached from the program. The proof occurs as a byproduct when we compile the program. Somehow we encode, for instance, the "all men are mortal; Socrates is a man; therefore Socrates is mortal" argument into types and write the corresponding code. Then when the code compiles, it verifies: yes, the argument is valid. At that point, we throw the program away. What (if anything) that program does is irrelevant; its types have proven the modus ponens as it passed through the compiler, thus quod erat demonstrandum. That is supposedly what type is all about in a very narrow, myopic branch of computer science.

And of course, it is not "untyped". It is dynamically typed.

by _ph_ 10y ago

And of course, it is not "untyped". It is dynamically typed.

PL theorists generally talk about whether or not syntactic terms (as opposed to runtime values) have types. Scheme is untyped by that definition.

klibertp 10y ago
PL theorists - from what I saw, not being one - prefer the term "unityped". It's not true that there are no (static!) types - there is a single, unnamed type which contains all possible values.
- kazinator 10y ago
  PL theorists who know what they are talking about know that this is false, because the actual diverse types of those values can be reasoned about at compile time. Such a "unityped" program is made up of syntax. We can reason about an expression more deeply than just "it returns a value" and we can do so statically. For instance in Lisp we know more about an expression like (cons 1 2) than that it returns a value. We know statically that it returns a cons. From that we can infer that (+ (cons 1 2) 3) is not well-typed. Type isn't just an implementation system; it's how we can reason about the program, as a mathematical object. The reasoning which informs us that (+ (cons 1 2) 3) is not well-formed without evaluating it, has to do with type. How we implement values (using a generic "cell" that is type-tagged) is just a convenience. We can get things working without being concerned for up-front type checking. It also represents the philosophy that type is innate to objects (not just a syntactic property of programs). A piece of compiled code can have a type passed into it which didn't exist when that code was compiled, and sensible things can happen anyway.
  - tel 10y ago
    It's not false, it's just unspecified. If you hand me scheme I can provide it a unitype system without conflict. If you hand me Haskell I cannot because the language has explicitly said that uncheckable statements are invalid. You can of course go further with your static analysis—a language may support many type systems in principle regardless of what the compiler accepts.
- szemet 10y ago
  It depends on the context. I guess rayiner has referred to "untyped lambda calculus". Thats not a bad name as it is self consistent - there are no type expressions in that language. If you say that it is actally "unityped" it is (just) your (semantical) categorization looking at it from a higher level perspective. Of course on the other side whole numbers were just "number"-s, before fractionals came, so in the end it may be ok to introduce higher level perspective in naming just to diferrentiate better. :)
- deleted 10y ago
  [deleted]
kazinator 10y ago
PL theorists don't get own the definition of what "type" means. Type pervades computing. A directory is a different type from a file or character device. A JPEG is a different file type from a PNG. You have MIME types in your e-mail. An ICMP packet is a different type from a TCP datagram. Machine language instruction sets have types: pointers, signed and unsigned words of various sizes, floating-point values. "Type" is a very broadly encompassing word. What all notions of type have in common is that it refers to some representation by whose rules some digital bits are interpreted to have a meaning (in some context which somehow establishes which rules apply).
- rayiner 10y ago
  > PL theorists don't get own the definition of what "type" means. Every field has its terms of art. "Type" is a term of art in PL theory; PL theorists are entitled to define it how they want. Of course you can use the word however you want, but you can't complain if that non-standard usage results in miscommunication with others. Besides that, it's very useful to able to talk about the "types" of syntactic terms as distinct from the "types" of runtime values. You can easily reason about syntactic types. You can, for example, use syntactic types to resolve syntax ambiguities (as in C++) or prove program properties. Runtime "types" are much less useful to PL theorists because it's hard to reason about them.
- noblethrasher 10y ago
  A PL theorist would note that most of the time when people talk about ‘types’, that they really mean ‘classes’, and that all of those things your mentioned would be considered to be the latter. Types are rather the elements of your program that correspond directly to logical propositions (which your program proves to be true).
  - kazinator 10y ago
    In software engineering, programs are usually not constructed to prove anything; this claim is just the consequence of an equivalence between logic and static typing (Curry-Howard). Programming languages do not make very good logic systems in spite of the isomorphism. They are not designed to be expressive that way. The logic system exhibited by the type system is geared toward proving trivialities about the program: mainly that its run-time translation won't misuse data. Plus it supports certain devices like polymporphism and pattern matching and whatnot. Now instead of writing a useful program, we can exploit the type system for doing logic in a separate domain, detached from the program. The proof occurs as a byproduct when we compile the program. Somehow we encode, for instance, the "all men are mortal; Socrates is a man; therefore Socrates is mortal" argument into types and write the corresponding code. Then when the code compiles, it verifies: yes, the argument is valid. At that point, we throw the program away. What (if anything) that program does is irrelevant; its types have proven the modus ponens as it passed through the compiler, thus quod erat demonstrandum. That is supposedly what type is all about in a very narrow, myopic branch of computer science.