I wish the project success- there’s a lot of innovation still to happen in programming languages and I’m always glad to see new ones getting built.
That said, I’m a little skeptical of the recent trends in optional typing. I don’t dismiss the idea that we might be able to make it work, but my experience so far has been that optional typing ends up being a worst-of-both-worlds scenario. You don’t really get the benefits of a strong static type system, since you have to deal with potentially untyped values, but you still spend some amount of time appeasing the type checker for the code that you did end up trying to make well typed. In the best case scenario you end up with an un-typed language, but more often than not they turn out to have all of the safety and reliability of untyped languages with the quick development time and short iteration cycles of a typed language.
Agreed! The following struck me as a pretty typical “pitch” for optional / gradual typing, but it doesn’t make sense (to me):
When prototyping, don’t specify any types, and Stanza will behave like a dynamically-typed scripting language. But when confident in your design, gradually add in types to make your code bulletproof.
I tend to think about programs as transformations applied to data, so the literal first thing I think about is the types (the data). I don’t write the transformations until I’ve got the types mostly worked out anyway, so there’s no point at which I want to omit the types.
I agree. I see optional typing as a way of adding some benefits of static typing to dynamic languages when you can’t start over from scratch. I don’t see the point of starting a language from scratch with optional typing, unless there is some high-value externality that induces it (Typescript wanting compatibility with Javascript, for instance).
my experience so far has been that optional typing ends up being a worst-of-both-worlds scenario. You don’t really get the benefits of a strong static type system, since you have to deal with potentially untyped values, but you still spend some amount of time appeasing the type checker for the code that you did end up trying to make well typed
As far as I can tell, every optionally typed language is simply going about it wrong: The default is that the programmer has to prove something to the type system, otherwise you get a static type error. A better default would be type annotations that cooperate with a runtime contract system for which only guaranteed runtime failures are converted to static errors. For cases where you do in fact want to force static checking, you could signal some assertion as static.
Another way to think about it is that type systems produce three-valued logics: proven, unproven, and disproven.
What happens when something is unproven is the key design point: Most type systems error. Unsound type systems “assume” the unproven thing is true. A contract system “checks” the unproven things at runtime. We should flip the default form “assume” to “check”, which requires runtime support. Explicit assume, runtime-check, and static-assert syntaxes could provide escape hatches for unsafe eliding of runtime checking, pushing out the boundaries of statically verified code, and requiring static proof respectively.
we even quote and link to stanza in our typing faq :) never actually used stanza beyond a few toy programs, but i’m a big fan of the design and ideas behind it.
A better default would be type annotations that cooperate with a runtime contract system for which only guaranteed runtime failures are converted to static errors.
This is how SBCL handles Common Lisp’s optional type annotations by default, “Declarations as Assertions”: “all type declarations that have not been proven to always hold are asserted at runtime.”
Sadly, as far as I can tell from the CL implementations I’ve seen, they only support the declaration of primitive types and arrays thereof. Things get really interesting once you get to user-defined type constructors, higher-kinded types, first-class functions, mutable objects, etc. Especially true if you want to preserve non-functional properties, such as constant space usage or predictable runtime. For example, there are trivial cases where contracts can cause behavior to become accidentally quadratic with naive implementations.
It doesn’t include your entire wishlist, but CL’s type system does support user-defined type constructors, arbitrary unions and intersections of types, etc., which is enough to do algebraic data types and some mildly fancy types like “nonempty list” or “integer outside the range [-500,500]”. There’s an overview here: https://alhassy.github.io/TypedLisp
I think most people who reach for optional typing, based on the pitch they use, really want whole program type inference. Haskell and a few others have this. Most languages with “inference” just have local inference and so you still have to “think about type annotations” but there is no reason to require that.
Speaking as someone who prefers dynamic typing (for live coding, creative coding, generative design, and hobby projects), the benefits I see in using type annotations in a dynamic language are: speeding up performance sensitive code, and getting high quality error messages when I misuse a library function. For the latter, I want error messages to tell me which argument was bad in a call to a library function – I don’t want a stack trace from the interior of a library function that requires me to understand the code.
Neither of these benefits requires that all type errors should be reported at compile time. If a statically typed library function runs fast and gives good error messages at runtime, then it meets the requirements.
The only time I expect to “fight the type checker” is when I have descended into the language’s statically typed low-level subset to write some high performance code.
I think that type annotations and compile time type errors are both excellent additions to a dynamically typed language. By the latter, I mean the compiler is able to deduce and report some run-time errors at compile time. This doesn’t lead to “fighting the type checker” if the static checker doesn’t report false positives (which static type systems will invariably do).
My reading of the Stanza docs is that Stanza is not a pure dynamic language. It switches to static type checking rules (inaccurately reporting false-positive type errors on good code) if all of your variables have type annotations. It’s a compromise that attempts to appeal to both static- and dynamic-typing users, but I suspect doesn’t give either side all that they want. So if, by “optional typing”, you mean this kind of compromise, then I may agree.
Typescript’s an interesting one, in that the strictness is adjustable and can be ramped up as you migrate your JS code over. For new projects you just start with super-strict settings.
That’s just not possible if there’s any IO. Well… maybe it’s not technically not possible but it’s culturally not possible. Maybe if every library in the world used strict TypeScript and didn’t do casts then there wouldn’t need to be runtime checks.
That is the theoretical aim, but in practice it winds up just being a half-typed codebase IME. Kind of a shame tbh. But, it’s turned me off of believing this language direction is trustworthy, as opposed to better linter.
I’ve been using stanza daily for a little over two years now - some other awesome features :
A statically typed/live reloading REPL
Mixed compiled and interpreted code
Dynamic multiple dispatch (as opposed to single dispatch)
Union and intersection types with subtyping
A second, “LoStanza” that allows you to write lowlevel systems code underneath “HiStanza” (which means you can implement all sorts of low level data structures, work over FFI, etc)
It’s an extremely productive and forgiving language, you tend to statically type most things but don’t feel like you’re fighting the type system. With subtyping and multimethods you don’t feel the need for advanced parametric polymorphism (although there is support for type parameters in types and functions)
In terms of personal projects, I wrote a little semver parsing library, originally intended to be used for a package manager (although I just converted it to a newer packaged format for a different PM tool), about a year ago I put together a proof-of-concept for async/await based on stanza’s nested coroutines that required optional typing, and I also prototyped an audio graph compilation algorithm in Stanza before rewriting in Rust.
The big project we’re building with stanza is JITX (disclaimer: I work there, but my thoughts are my own). We use it extensively for the implementation of the compiler and libraries, you can see some of the open source JITX code (as a DSL embedded into stanza) over here.
I think it was somewhat of a perfect storm for our founders when they began the project, and Stanza was the tool for the job. Our about page has a little more info about the people behind it.
Opening Brackets:
Syntactically, an identifier followed immediately by a opening bracket character is treated differently than if the two were separated by spaces. For example f(x) is syntactically different than f (x)
For example, this is why it was stressed to you to remember the space after main in defn main () :
I get why in an expression f (x) and f(x) need to be distinguished. However, why force that in the function definition? It looks awkward. Are you doing something interesting there? For example, can I do the following?
I haven’t tried to read it, but I just I stumbled into the underlying dissertation while looking for any discussion of Stanza alongside Racket. In case it’s of interest to anyone:
The documentation seems really well structured and written, and there seems to be a focus on software architecture at the language design level, which I think is worth noting. Now what I want to know is how well it performs compared to say, Python and Go.
I wish the project success- there’s a lot of innovation still to happen in programming languages and I’m always glad to see new ones getting built.
That said, I’m a little skeptical of the recent trends in optional typing. I don’t dismiss the idea that we might be able to make it work, but my experience so far has been that optional typing ends up being a worst-of-both-worlds scenario. You don’t really get the benefits of a strong static type system, since you have to deal with potentially untyped values, but you still spend some amount of time appeasing the type checker for the code that you did end up trying to make well typed. In the best case scenario you end up with an un-typed language, but more often than not they turn out to have all of the safety and reliability of untyped languages with the quick development time and short iteration cycles of a typed language.
Agreed! The following struck me as a pretty typical “pitch” for optional / gradual typing, but it doesn’t make sense (to me):
I tend to think about programs as transformations applied to data, so the literal first thing I think about is the types (the data). I don’t write the transformations until I’ve got the types mostly worked out anyway, so there’s no point at which I want to omit the types.
I agree. I see optional typing as a way of adding some benefits of static typing to dynamic languages when you can’t start over from scratch. I don’t see the point of starting a language from scratch with optional typing, unless there is some high-value externality that induces it (Typescript wanting compatibility with Javascript, for instance).
As far as I can tell, every optionally typed language is simply going about it wrong: The default is that the programmer has to prove something to the type system, otherwise you get a static type error. A better default would be type annotations that cooperate with a runtime contract system for which only guaranteed runtime failures are converted to static errors. For cases where you do in fact want to force static checking, you could signal some assertion as static.
Another way to think about it is that type systems produce three-valued logics: proven, unproven, and disproven.
What happens when something is unproven is the key design point: Most type systems error. Unsound type systems “assume” the unproven thing is true. A contract system “checks” the unproven things at runtime. We should flip the default form “assume” to “check”, which requires runtime support. Explicit assume, runtime-check, and static-assert syntaxes could provide escape hatches for unsafe eliding of runtime checking, pushing out the boundaries of statically verified code, and requiring static proof respectively.
You’ll like Pytype, which only errors on disproven code: https://github.com/google/pytype#how-is-pytype-different-from-other-type-checkers
Neat!
The other big one I’ve heard of (but have not tried) is Erlang’s “Dialyzer” based on “success types”: https://easychair.org/publications/paper/FzsM
Unfortunately, I don’t think either of these perform have a runtime checking/contract system.
we even quote and link to stanza in our typing faq :) never actually used stanza beyond a few toy programs, but i’m a big fan of the design and ideas behind it.
This is how SBCL handles Common Lisp’s optional type annotations by default, “Declarations as Assertions”: “all type declarations that have not been proven to always hold are asserted at runtime.”
Sadly, as far as I can tell from the CL implementations I’ve seen, they only support the declaration of primitive types and arrays thereof. Things get really interesting once you get to user-defined type constructors, higher-kinded types, first-class functions, mutable objects, etc. Especially true if you want to preserve non-functional properties, such as constant space usage or predictable runtime. For example, there are trivial cases where contracts can cause behavior to become accidentally quadratic with naive implementations.
It doesn’t include your entire wishlist, but CL’s type system does support user-defined type constructors, arbitrary unions and intersections of types, etc., which is enough to do algebraic data types and some mildly fancy types like “nonempty list” or “integer outside the range [-500,500]”. There’s an overview here: https://alhassy.github.io/TypedLisp
I think most people who reach for optional typing, based on the pitch they use, really want whole program type inference. Haskell and a few others have this. Most languages with “inference” just have local inference and so you still have to “think about type annotations” but there is no reason to require that.
Speaking as someone who prefers dynamic typing (for live coding, creative coding, generative design, and hobby projects), the benefits I see in using type annotations in a dynamic language are: speeding up performance sensitive code, and getting high quality error messages when I misuse a library function. For the latter, I want error messages to tell me which argument was bad in a call to a library function – I don’t want a stack trace from the interior of a library function that requires me to understand the code.
Neither of these benefits requires that all type errors should be reported at compile time. If a statically typed library function runs fast and gives good error messages at runtime, then it meets the requirements.
The only time I expect to “fight the type checker” is when I have descended into the language’s statically typed low-level subset to write some high performance code.
I think that type annotations and compile time type errors are both excellent additions to a dynamically typed language. By the latter, I mean the compiler is able to deduce and report some run-time errors at compile time. This doesn’t lead to “fighting the type checker” if the static checker doesn’t report false positives (which static type systems will invariably do).
My reading of the Stanza docs is that Stanza is not a pure dynamic language. It switches to static type checking rules (inaccurately reporting false-positive type errors on good code) if all of your variables have type annotations. It’s a compromise that attempts to appeal to both static- and dynamic-typing users, but I suspect doesn’t give either side all that they want. So if, by “optional typing”, you mean this kind of compromise, then I may agree.
that’s been my experience with Typescript, for sure.
Typescript’s an interesting one, in that the strictness is adjustable and can be ramped up as you migrate your JS code over. For new projects you just start with super-strict settings.
And yet it’s only so strict. No runtime checks and no runtime references to types.
The whole point is to get rid of the need for runtime checks :)
That’s just not possible if there’s any IO. Well… maybe it’s not technically not possible but it’s culturally not possible. Maybe if every library in the world used strict TypeScript and didn’t do casts then there wouldn’t need to be runtime checks.
Which is why a single
anyrapidly spreads out like cancer and turns your typedefs into lies.It doesn’t have to be
anyit can beastoo. For example:await fetch().json() as MyAPIResponseThat is the theoretical aim, but in practice it winds up just being a half-typed codebase IME. Kind of a shame tbh. But, it’s turned me off of believing this language direction is trustworthy, as opposed to better linter.
I’ve been using stanza daily for a little over two years now - some other awesome features :
It’s an extremely productive and forgiving language, you tend to statically type most things but don’t feel like you’re fighting the type system. With subtyping and multimethods you don’t feel the need for advanced parametric polymorphism (although there is support for type parameters in types and functions)
What sort of things are you building with stanza?
In terms of personal projects, I wrote a little semver parsing library, originally intended to be used for a package manager (although I just converted it to a newer packaged format for a different PM tool), about a year ago I put together a proof-of-concept for async/await based on stanza’s nested coroutines that required optional typing, and I also prototyped an audio graph compilation algorithm in Stanza before rewriting in Rust.
The big project we’re building with stanza is JITX (disclaimer: I work there, but my thoughts are my own). We use it extensively for the implementation of the compiler and libraries, you can see some of the open source JITX code (as a DSL embedded into stanza) over here.
that’s pretty awesome. what made jitx decide on using stanza?
I think it was somewhat of a perfect storm for our founders when they began the project, and Stanza was the tool for the job. Our about page has a little more info about the people behind it.
oh hah, patrick li is a cofounder :) definitely makes sense that he would use stanza, then, and that’s an awesome proof of the language’s worth.
It’s a bit rich to dunk on LISP parens and then make your language whitespace soup…
From Chapter 2
I get why in an expression
f (x)andf(x)need to be distinguished. However, why force that in the function definition? It looks awkward. Are you doing something interesting there? For example, can I do the following?I haven’t tried to read it, but I just I stumbled into the underlying dissertation while looking for any discussion of Stanza alongside Racket. In case it’s of interest to anyone:
https://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-215.pdf
The documentation seems really well structured and written, and there seems to be a focus on software architecture at the language design level, which I think is worth noting. Now what I want to know is how well it performs compared to say, Python and Go.
It’s not obvious to me what the benefit of this is over Python. Better performance when compiled than compiled Python?