9 ms·

This is the first I've heard of Shen, so I can't say. However the Racket engineers, particularly Matthias Felleisen, are doing cutting-edge research into types

This is the first I've heard of Shen, so I can't say. However the Racket engineers, particularly Matthias Felleisen, are doing cutting-edge research into types. Typing is not a solved problem, because if it was, there wouldn't be a static vs dynamic type debate that lingers ad nauseum. Racket is in an interesting sweet spot for typing research because it is a traditional lisp with dynamic types, to which gradual typing that works both in typed and untyped land has been introduced and continues to undergo extensive attention.

effie 10y ago
"Typing is not a solved problem, because if it was, there wouldn't be a static vs dynamic type debate that lingers ad nauseum." Could you clarify? Surely even if typing was completely solved, we would still have debates of that kind, because there are benefits to both approaches and there will always be people preferring one or another.
- hellofunk 10y ago
  > because there are benefits to both approaches and there will always be people preferring one or another And that is exactly my point: people prefer one or the other because it is not a solved problem, there is no universally accepted way.
- groovy2shoes 10y ago
  The reason typing is not a solved problem is this: there are valid programs which can be expressed in an untyped language that cannot be (directly) expressed in a typed one at the moment. For example: (define (foo p?) (if p? 42 "forty-two")) What is the type of `foo`? It could be `bool -> int` or `bool -> string`, depending on the result of `p?`! In an untyped language, this is a perfectly valid program. In a typed language, this presents a type error, even if `p?` happens to always result in `true` or always result in `false`. The programmer reading the program knows that if `p?` is always `true`, then the type of `foo` is `bool -> int`, and that if `p?` is always `false`, the type is `bool -> string`. However, this program, as-is, is will be rejected as ill-typed. In a language providing sum types, we can work around this by using a type like `(int * string) either`: (define (foo p?) (if p? (left 42) (right "forty-two"))) Where `left` and `right` are type constructors for values of type `('a * 'b) either`. Now, the type of `foo` is `bool -> (int * string) either`. This workaround effectively adds a run-time tag to the `either` values to distinguish the `left` case from the `right` case, which is essentially the way dynamically checked languages operate for values of all types but in a more restricted, specific, and arguably meaningful form. In many (most?) languages with sum types, the language will ensure that the programmer always checks the tag of the `either` values before accessing the underlying "actual" value -- this is the only way to guarantee type safety while ensuring that the program does not barf due to a "type" error at run-time. Now, it could be argued that the typing problem presented above is basically solved by sum types. But it could also be argued that this doesn't really solve the problem, because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?`, which could maybe be written as `p:=bool -> (p ? int : string)`, for example. Perhaps dependent typing could help us come to a true solution for this case, but there are other cases where other solutions will be needed. According to Benjamin C. Pierce in Types and Programming Languages: "Being static, type systems are necessarily also conservative : they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence, and hence they must also sometimes reject programs that actually behave well at run time. ... The tension between conservativity and expressiveness is a fundamental fact of life in the design of type systems. The desire to allow more programs to be typed -- by assigning more accurate types to their parts -- is the main force driving research in the field.[0] In essence, while there is already a vast array of programs we already know how to type, and while it's possible to work around cases that resist typing, type theory is still an active field of research with plenty of open questions yet to be answered. The corollary to this is that there are still valid reasons to prefer untyped languages to typed ones, as my sibling commentor pointed out. The day when typing is solved is the day people can no longer not look like an bozos for preferring untyped languages, but until that day comes, untyped languages remain fundamentally more expressive than typed ones (in the sense that they're fundamentally capable of expressing more programs[1]). --- [0]: Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002. §1.1, pp. 2,3. [1]: There's also a sense in which typed languages are more expressive than untyped ones, and that's the sense that they are capable of expressing more properties of the program as part of the program itself.
  - hellofunk 10y ago
    This is quite a nice write-up, thank you. Regarding this point: >because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?` Is this situation not resolved by allowing p? to not be a bool necessarily but also a sum type that informs foo which case of a different sum type to return? Anyway, I like your footnote [1] which, for me, is what allows a typed program to actually be more expressive, in the sense that you can literally express the types in your head as you code, which is difficult or simply not provided in a dynamic language, despite that most developers will be "thinking in types" regardless of typing of the language. Now, "expressive" also often means "elegant" because you can express an idea easily with less verbosity in a dynamic language. A language with type inference is an interesting medium that sort of removes the expressivity of explicit type annotations while gaining the expressivity of a dynamic language in some respects.
    - groovy2shoes 10y ago
      > Is this situation not resolved by allowing p? to not be a bool necessarily but also a sum type that informs foo which case of a different sum type to return? In the example I provided, the `bool -> (int * string) either` function is essentially a map from a `bool` to an `(int * string) either`. From a type-theoretic perspective, bool (which has two nullary type constructors, `true` and `false`) can be expressed as the sum of two units: `1 + 1` (or equivalently, `() + ()` or `unit + unit`) = `2`. If I understand your question correctly, then you're asking if we could just use some other sum type to express the branch to take, like: `type if-branch = consequent | alternative;`, and the answer is that such a type is precisely isomorphic to a Boolean -- because it consists of two nullary constructors, it can also be expressed as the sum of two units, `1 + 1` = `2`. To answer your question more directly, `p?` already is a sum type that informs `foo` which case to return: `type bool = true | false;`. > Anyway, I like your footnote [1] which, for me, is what allows a typed program to actually be more expressive, in the sense that you can literally express the types in your head as you code, which is difficult or simply not provided in a dynamic language, despite that most developers will be "thinking in types" regardless of typing of the language. "Expressive" can mean any of quite a few different things, so I wanted to be specific which I meant. In this case, I mean that untyped languages are more expressive because they're capable of expressing a greater number of programs than their typed counterparts. The ultimate goal of type theory is to eliminate that gap, but short of some miracle revelation, we've resigned to gradually filling it in. Note that this isn't the same as saying you can express it more elegantly or less verbosely in an untyped language -- there are some programs that are strictly not expressible with current type systems. That's on purpose! The point of the type system is to reject programs which have bugs caused by type errors, so we make those programs inexpressible on purpose, so it's usually a good thing to be less expressive in that way. The problem is that our type systems sometimes reject bug-free programs that actually would run totally fine simply because it wasn't able to prove that such was the case. Again, type theorists are working to improve the situation. What it comes down to is a question of what is being expressed. Taking programs as descriptions of processes, at the lowest level a language allows us to express a run-time process. Going up one level to the level of types, we can express information about the program itself. Thus, in a sense, by using a typed language we trade in the expressiveness of some processes for the expressiveness of some metaprocesses.

effie 10y ago

"Typing is not a solved problem, because if it was, there wouldn't be a static vs dynamic type debate that lingers ad nauseum." Could you clarify? Surely even if typing was completely solved, we would still have debates of that kind, because there are benefits to both approaches and there will always be people preferring one or another.

hellofunk 10y ago
> because there are benefits to both approaches and there will always be people preferring one or another And that is exactly my point: people prefer one or the other because it is not a solved problem, there is no universally accepted way.
groovy2shoes 10y ago
The reason typing is not a solved problem is this: there are valid programs which can be expressed in an untyped language that cannot be (directly) expressed in a typed one at the moment. For example: (define (foo p?) (if p? 42 "forty-two")) What is the type of `foo`? It could be `bool -> int` or `bool -> string`, depending on the result of `p?`! In an untyped language, this is a perfectly valid program. In a typed language, this presents a type error, even if `p?` happens to always result in `true` or always result in `false`. The programmer reading the program knows that if `p?` is always `true`, then the type of `foo` is `bool -> int`, and that if `p?` is always `false`, the type is `bool -> string`. However, this program, as-is, is will be rejected as ill-typed. In a language providing sum types, we can work around this by using a type like `(int * string) either`: (define (foo p?) (if p? (left 42) (right "forty-two"))) Where `left` and `right` are type constructors for values of type `('a * 'b) either`. Now, the type of `foo` is `bool -> (int * string) either`. This workaround effectively adds a run-time tag to the `either` values to distinguish the `left` case from the `right` case, which is essentially the way dynamically checked languages operate for values of all types but in a more restricted, specific, and arguably meaningful form. In many (most?) languages with sum types, the language will ensure that the programmer always checks the tag of the `either` values before accessing the underlying "actual" value -- this is the only way to guarantee type safety while ensuring that the program does not barf due to a "type" error at run-time. Now, it could be argued that the typing problem presented above is basically solved by sum types. But it could also be argued that this doesn't really solve the problem, because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?`, which could maybe be written as `p:=bool -> (p ? int : string)`, for example. Perhaps dependent typing could help us come to a true solution for this case, but there are other cases where other solutions will be needed. According to Benjamin C. Pierce in Types and Programming Languages: "Being static, type systems are necessarily also conservative : they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence, and hence they must also sometimes reject programs that actually behave well at run time. ... The tension between conservativity and expressiveness is a fundamental fact of life in the design of type systems. The desire to allow more programs to be typed -- by assigning more accurate types to their parts -- is the main force driving research in the field.[0] In essence, while there is already a vast array of programs we already know how to type, and while it's possible to work around cases that resist typing, type theory is still an active field of research with plenty of open questions yet to be answered. The corollary to this is that there are still valid reasons to prefer untyped languages to typed ones, as my sibling commentor pointed out. The day when typing is solved is the day people can no longer not look like an bozos for preferring untyped languages, but until that day comes, untyped languages remain fundamentally more expressive than typed ones (in the sense that they're fundamentally capable of expressing more programs[1]). --- [0]: Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002. §1.1, pp. 2,3. [1]: There's also a sense in which typed languages are more expressive than untyped ones, and that's the sense that they are capable of expressing more properties of the program as part of the program itself.
- hellofunk 10y ago
  This is quite a nice write-up, thank you. Regarding this point: >because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?` Is this situation not resolved by allowing p? to not be a bool necessarily but also a sum type that informs foo which case of a different sum type to return? Anyway, I like your footnote [1] which, for me, is what allows a typed program to actually be more expressive, in the sense that you can literally express the types in your head as you code, which is difficult or simply not provided in a dynamic language, despite that most developers will be "thinking in types" regardless of typing of the language. Now, "expressive" also often means "elegant" because you can express an idea easily with less verbosity in a dynamic language. A language with type inference is an interesting medium that sort of removes the expressivity of explicit type annotations while gaining the expressivity of a dynamic language in some respects.
  - groovy2shoes 10y ago
    > Is this situation not resolved by allowing p? to not be a bool necessarily but also a sum type that informs foo which case of a different sum type to return? In the example I provided, the `bool -> (int * string) either` function is essentially a map from a `bool` to an `(int * string) either`. From a type-theoretic perspective, bool (which has two nullary type constructors, `true` and `false`) can be expressed as the sum of two units: `1 + 1` (or equivalently, `() + ()` or `unit + unit`) = `2`. If I understand your question correctly, then you're asking if we could just use some other sum type to express the branch to take, like: `type if-branch = consequent | alternative;`, and the answer is that such a type is precisely isomorphic to a Boolean -- because it consists of two nullary constructors, it can also be expressed as the sum of two units, `1 + 1` = `2`. To answer your question more directly, `p?` already is a sum type that informs `foo` which case to return: `type bool = true | false;`. > Anyway, I like your footnote [1] which, for me, is what allows a typed program to actually be more expressive, in the sense that you can literally express the types in your head as you code, which is difficult or simply not provided in a dynamic language, despite that most developers will be "thinking in types" regardless of typing of the language. "Expressive" can mean any of quite a few different things, so I wanted to be specific which I meant. In this case, I mean that untyped languages are more expressive because they're capable of expressing a greater number of programs than their typed counterparts. The ultimate goal of type theory is to eliminate that gap, but short of some miracle revelation, we've resigned to gradually filling it in. Note that this isn't the same as saying you can express it more elegantly or less verbosely in an untyped language -- there are some programs that are strictly not expressible with current type systems. That's on purpose! The point of the type system is to reject programs which have bugs caused by type errors, so we make those programs inexpressible on purpose, so it's usually a good thing to be less expressive in that way. The problem is that our type systems sometimes reject bug-free programs that actually would run totally fine simply because it wasn't able to prove that such was the case. Again, type theorists are working to improve the situation. What it comes down to is a question of what is being expressed. Taking programs as descriptions of processes, at the lowest level a language allows us to express a run-time process. Going up one level to the level of types, we can express information about the program itself. Thus, in a sense, by using a typed language we trade in the expressiveness of some processes for the expressiveness of some metaprocesses.