> Unlike current languages, Stanza is neither dynamically- nor statically-typed, and has instead what we call an optional type system.
Why "optional typing"? It sounds like you are describing "gradual typing". [0] Using the more common term would make it easier for fans of Stanza to discover the slew of other languages that are pursuing similar type systems.
Optional typing is the general term for such type systems. "Gradual typing" was coined originally in a paper by Jeremy Siek and refers to a specific set of axioms that must be satisfied.
Thank you for the link though. I will see how the term is used colloquially nowadays.
The PL academic community here in New England seems to use the word in fairly broad sense. (Admittedly, type theory isn't my area, and they very well may use a different term when they actually write papers.)
There seems to be a lot of variance in what people mean by gradual/optional typing.
For example, Pyret (a language I work on) has both typed and untyped semantics. In both semantics, bindings can be optionally annotated with a type, and any Pyret program can be executed with dynamic type checking, or can be first statically type checked before executing (but doing so does not remove the dynamic checks). What should this be called? The practical effect is much the same: users can gradually add type annotations.
On the other hand, it's a far simpler approach than typed racket or reticulated python. We made the conscious decision only to include language features for which we had a static type-checking story for, wrote the compiler as if there was no static type checking, and then wrote a type inferencer/checker for the language which can be optionally enabled.
Ah I have skimmed through the webpage for Pyret before. It's nice to meet you. I have some questions for you about that that I'll ask you later.
What you're describing is, I believe, one particular strategy among many with the goal of allowing users to gradually add type annotations. The goal itself is not new, and is often called optional-typing. The two words "gradual typing" specifically is also one particular strategy for optional typing but is under the ownership of Jeremy since he coined it. Informally, people do seem to use the term in a looser way.
> Our optional type system was designed from the perspective that a single language can consistently contain the semantics of both a dynamically-typed and a statically-typed language.
The obvious meaning of the word "consistently" here would preclude Turing-complete languages from this (recognition of the same language + undecidability), unless you adopt a fairly idiosyncratic definition of "type safe". I haven't read the whole thing, but it seems like there's a lot of dancing around this without actually coming out and saying it. For me, at least, headlining what you're not claiming would make this substantially more readable.
Edit: Okay, read some more and the "Parametric Types and Stanza's Captured Type System" and "Implications for Safety" sections "dance closer", but it feels like the implications need to be pulled out and moved way up. The covariance assumption in particular...let's just say that I was expecting something substantially different by the time I got to that point.
Finally, if you want some nit-picky editing advice: The terms "Thus" and (to a lesser extent) "Hence" are used...frequently. Possibly just me, but I found it fairly jarring.
> preclude Turing-complete languages from this (recognition of the same language + undecidability)
Can you explain what you mean here? What is the undecidability result you are referring to?
I kind of have the feeling you are trying to make a point about formal languages being "the same", whereas the article uses "the same language" to mean "a single programming language" that allows, but does not require, type declarations.
That such a language can exist should not be a point of contention. You yourself pointed to the PEP that defines such a language.
> What is the undecidability result you are referring to?
Just the correspondence between static type safety and the halting problem.
> I kind of have the feeling you are trying to make a point about formal languages being "the same", whereas the article uses "the same language" to mean "a single programming language" that allows, but does not require, type declarations.
Yes this. To me, it felt like the article was making the "stronger" claim, at least until the end when it starts talking about co/contra-variance.
> Just the correspondence between static type safety and the halting problem.
I'm not sure if you are saying that there cannot be programming languages with decidable static type systems. Because there are programming languages with decidable static type systems. Typically you cannot encode Turing machines in the type system, so you don't get the kind of problem you seem to be talking about. (But you haven't really explained what you are talking about.)
// ... Well typed things ...
if (arbitrary_well_typed_function()) {
v = 0xF00 + "bar"
}
// ... Well typed things ...
Let's say this program is well typed iff `arbitrary_well_typed_function()` is falsy. If a static type checker can not compute `arbitrary_well_typed_function`, it needs to make a trade-off which a dynamic type checker need not.
type card_value = [`Jack | `Queen | `King | `Ace | `Num of int]
(* not really necessary, but nice to have *)
type royal_card = [`Jack | `Queen | `King]
let royal_value (card: royal_card): int =
match card with `Jack | `Queen | `King -> 1
When trying to abuse this, you get a static type error at compile time:
royal_value `Ace;;
Error: This expression has type [> `Ace ]
but an expression was expected of type royal_card
The second variant type does not allow tag(s) `Ace
Hmm...no mention of Objective-C? Optionally typing things since the early 90ies. The "?" type sound a lot like "id" in Objective-C. And the "feel" is very much what you describe. Quick prototyping, incremental hardening.
> Doesn't whether a language is compiled or interpreted have an effect on the type system?
The question is not well-posed. Would you call Haskell or OCaml "compiled" languages? They certainly can be compiled to machine code, and often are, but both also have interpreted versions. Would you call Python an "interpreted" language? There are compilers from Python to machine code, which are more or less successful at optimizing away type checks. Being compiled or interpreted (or one of the many intermediate things) is not so much a language property as a property of the implementation.
That said, there are of course some correlations. Python code can heavily inspect and modify itself and its execution context. This kind of thing is easier to do in an interpreter, and it's much easier to do with a dynamic type system. Dynamically typed languages also tend to be interpreted because the dynamic typing incurs runtime costs anyway, so often you would not win a lot of performance by simple ahead-of-time compilation.
(Of course, if your goal is to have a compiled implementation without dynamic type checks, you will design a static type system.)
Why "optional typing"? It sounds like you are describing "gradual typing". [0] Using the more common term would make it easier for fans of Stanza to discover the slew of other languages that are pursuing similar type systems.
[0] https://en.wikipedia.org/wiki/Gradual_typing