Bracha v Felleisen “Types for an Untyped World” (2015) [video](youtube.com)
youtube.com
Bracha v Felleisen “Types for an Untyped World” (2015) [video]
https://www.youtube.com/watch?v=JBmIQIZPaHY
3 comments
They're so right about that.
As a frontend dev, I don't care about that extra 1-2% of bugs that, say, ownership types could catch if it kills my productivity by having to annotate everything.
However, if I can figure out what a method actually returns and click through to it in the IDE, that's the real gain from types for me. Type analysis has to be fast to be able to do that.
My impression of research in academia is that it's disproportionately focused on even stronger types that are even harder to compute. Not everyone builds spaceships.
However, if I can figure out what a method actually returns and click through to it in the IDE, that's the real gain from types for me. Type analysis has to be fast to be able to do that.
My impression of research in academia is that it's disproportionately focused on even stronger types that are even harder to compute. Not everyone builds spaceships.
research in academia is that
it's disproportionately focused
on even stronger types that are
even harder to compute.
Most work on expressive typing systems (e.g. dependent types) has a different aim, namely using types for the verification of arbitrary program properties. This is undecidable, but we want (and need) as much automation as possible to lower the cost of verification, whence a lot of research is about partially automated type inference for very expressive typing systems. For most standard front-end dev, verification is not an issue since
- the field has fairly low correctness requirements that can easily achieved with testing
- typically you don't have strong specifications to verify against. No formal spec, no verification.
[1] L. Damas, R. Milner: Principal type-schemes for functional programs, http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_typ...
Just going to point out here that you are conflating Javascript problems with dynamic language problems. Try Clojure, a well designed dynamic language, and you'll find you are a lot more productive with it than any statically typed language.
Indeed over the weekend I was able to design and build a GUI DSL, layout system, model-view databinding, command event system, and serialisation/deserialisation logic for a side project of mine. This sort of stuff would have taken weeks of effort in a static language.
Indeed over the weekend I was able to design and build a GUI DSL, layout system, model-view databinding, command event system, and serialisation/deserialisation logic for a side project of mine. This sort of stuff would have taken weeks of effort in a static language.
Clojure is a fine language, and I wrote it professionally for a few years.
However, I don't see why this would be true:
> This sort of stuff would have taken weeks of effort in a static language.
I've also written plenty of things in typed languages, and in many ways they can be faster to develop in than dynamic languages. Of course, you do need to change the way you program a bit to really take advantage of types.
I think the main advantage Clojure has over most typed languages is macros, but there is work being done to rectify even that.
However, I don't see why this would be true:
> This sort of stuff would have taken weeks of effort in a static language.
I've also written plenty of things in typed languages, and in many ways they can be faster to develop in than dynamic languages. Of course, you do need to change the way you program a bit to really take advantage of types.
I think the main advantage Clojure has over most typed languages is macros, but there is work being done to rectify even that.
I used to think this, until I used Clojure. I'm surprised you used it professionally and have that mindset, I write far less code in Clojure and get far more done. The productivity gains are amazing, especially when I can just upload new code on the fly as the program is running.
Part of the issue is maintenance. Coming back to code you haven't worked on in a while can require more time to load back into your head than a typed language. And speaking from experience [1], refactoring in a typed language also tends to go more smoothly.
> I'm surprised you used it professionally and have that mindset
I used to have your mindset when I first started working with Clojure :)
Keep in mind that not all typed languages are created equal. Clojure is still much better than Java. But I find I'm quite productive with OCaml, due in large part to the simple but powerful type system, plus the fantastic module system. OCaml does have some drawbacks compared to Clojure, but they're not related to static typing. The main disadvantages are the macro system (even the new extension point stuff is cumbersome compared to a proper macro system) and the smaller library ecosystem.
[1] I've done a lot of refactoring in Clojure, and while it wasn't terrible, types can help a lot.
[Edit] To be clear, I do think Clojure has a lot going for it, but I don't think any of it's advantages are due to being dynamically typed, and there's no reason a statically typed language can't have the same benefits.
> I'm surprised you used it professionally and have that mindset
I used to have your mindset when I first started working with Clojure :)
Keep in mind that not all typed languages are created equal. Clojure is still much better than Java. But I find I'm quite productive with OCaml, due in large part to the simple but powerful type system, plus the fantastic module system. OCaml does have some drawbacks compared to Clojure, but they're not related to static typing. The main disadvantages are the macro system (even the new extension point stuff is cumbersome compared to a proper macro system) and the smaller library ecosystem.
[1] I've done a lot of refactoring in Clojure, and while it wasn't terrible, types can help a lot.
[Edit] To be clear, I do think Clojure has a lot going for it, but I don't think any of it's advantages are due to being dynamically typed, and there's no reason a statically typed language can't have the same benefits.
It's because it's a LISP with good ecosystem. LISP is already strongly, but dynamically, typed from what I'm told. So, you get quite a bit of benefit. You could probably do the same in a statically- or gradually-typed LISP. Main difference is you'll catch a few more interface errors without tests. Also, if using specs or types, one can do automated generation of testing, enabled better static analysis, and/or improve optimization in compilers. Basically, the tools know a bit more about what you're trying to do.
Throwing that back at you: Don't conflate Java problems with static language problems...
Java almost always lost in productivity or correctness studies on programs of significant size unless it was going up against monstrosities like C or C++. So, yeah, it's a holdover from Worse is Better effect and corporate sponsorship rather than illustrative of something great in static 3GL's.
> This sort of stuff would have taken weeks of effort in a static language.
For you, maybe. For someone familiar with that static language? They might have gone faster.
Productivity in a language is highly subjective so it shouldn't come into the equation if you're trying to compare statically and dynamically typed languages.
For you, maybe. For someone familiar with that static language? They might have gone faster.
Productivity in a language is highly subjective so it shouldn't come into the equation if you're trying to compare statically and dynamically typed languages.
For the record, I've been a C# developer for 12 years. A Clojure dev for about ~6 months. Also, productivity is not subjective.
It is unless you're measuring the differences with an apples to apples comparison. Examples of how it was done in case studies or empirical research on software development:
1. Features developed by teams with different languages.
2. Features per day per team.
3. Lines of code that took.
4. Defect rate found after all testing and review.
5. Time taken to modify N lines of existing code.
6. Defects introduced during modifications.
7. Overall productivity rate at end of project for each that factors in initial lines of code minus what was reworked to get real lines of correct code produced averaged across each day usually.
Clojure vs Typed Racket vs commercial Smalltalk vs Ocaml or Haskell w/ meta-programming might tell use something objectively. Right now, you have no measurements on typed alternatives similar to your current tool. Your claim that it's more productive is highly subjective albeit I'll give you that prior measurements with small, sample size confirmed strongly-typed, dynamic languages give major productivity boost over statically-typed 3GL's. LISP and Smalltalk winning in that area over predecessors to C#. Your language vs similar ones remains worth measuring, though.
1. Features developed by teams with different languages.
2. Features per day per team.
3. Lines of code that took.
4. Defect rate found after all testing and review.
5. Time taken to modify N lines of existing code.
6. Defects introduced during modifications.
7. Overall productivity rate at end of project for each that factors in initial lines of code minus what was reworked to get real lines of correct code produced averaged across each day usually.
Clojure vs Typed Racket vs commercial Smalltalk vs Ocaml or Haskell w/ meta-programming might tell use something objectively. Right now, you have no measurements on typed alternatives similar to your current tool. Your claim that it's more productive is highly subjective albeit I'll give you that prior measurements with small, sample size confirmed strongly-typed, dynamic languages give major productivity boost over statically-typed 3GL's. LISP and Smalltalk winning in that area over predecessors to C#. Your language vs similar ones remains worth measuring, though.
To be fair, C# is not the pinnacle of statically typed languages. Go is quite a lot nicer from a productivity perspective, and but there is also Haskell and OCaml if you want a more expressive type system.
Does Clojure support something that JS doesn't, or is it mostly that JS has warts that introduce errors that slow you down? I would think that Clojure is more or less a subset of JS, and if you're disciplined about using that subset, you should be equally productive in either language.
Also, a frequent problem I have in JS and Python is that they don't scale very well; type documentation must be updated manually and inevitably becomes incorrect with time; determining the type of a return is always a matter of extensive grepping, etc. With most statically typed languages, the IDE can tell you this right away, but in the worst case you just look at the function signature; does Clojure have a solution for this problem?
Also, a frequent problem I have in JS and Python is that they don't scale very well; type documentation must be updated manually and inevitably becomes incorrect with time; determining the type of a return is always a matter of extensive grepping, etc. With most statically typed languages, the IDE can tell you this right away, but in the worst case you just look at the function signature; does Clojure have a solution for this problem?
Thinking of Clojure as a subset of JS is a new one. It's more accurate to say JS is a badly implemented Lisp! These are the main reasons Clojure works so well:
1. It is a Lisp: The only type is the 'list', and in Clojure you also have 'maps' too (basically a dictionary in JS). That's it. Any object in JS is a map in Clojure, which keeps everything nice and simple. The main power of this is you only ever need to support lists or maps in your functions, and then your functions work for every data structure you ever create! For example clojure.core ships with 'get-in' 'assoc-in', 'diff' etc, all functions that work on your structures no matter how complex.
2. It is a functional language: JS is imperative, meaning you have to fit your ideas to the language, breaking everything down into for loops and if statements. With Clojure you fit the language to the idea, and think in data transformations instead. Then you create a set of functions that deal with that problem specifically, all wrapped up in single namespace. For example a 'tilemap' ns that contains a set of functions for converting to/from screen and grid coordinates. Or getting the neighbours of a specified tile from the 2d array. The end result is a custom DSL that reads almost like English.
3. It is 'immutable by default': All data structures are persistent. The problems you have with scaling in JS and Python is all because of mutable local and global state, as it becomes very difficult to know what is changing what. Clojure doesn't have this problem, as values can't be edited, only new ones returned. There is still mutability of course, but it is restricted to maybe 10 locations in your codebase. The mental burden this lifts from your shoulders cannot be understated.
4. It has a REPL: Let me ask how much effort you think building a HTML editor is? Or the UI designer in Visual Studio? With Clojure, I can just make edits to the GUI code on the fly and press F10 and voila the changes appear in-app. Instant editor, for free. This is what i was doing the other day; editing my GUI code (re-arranging controls, changing positions and sizes) and then immediately inspecting the result in the running program. The productivity gains are huge when you remove the laborious 'write code, wait for build, navigate to place in the app, finally test your changes, find error, end program, change code, repeat' cycle from your workflow.
5. Macros: Lisp macros are just Lisp code again. Literally the whole language available to you at compile time. The clojure.async library for example uses this to provide Go style channels for async programming. It means you can write code that looks great, and still compiles down to something performant at the end.
1. It is a Lisp: The only type is the 'list', and in Clojure you also have 'maps' too (basically a dictionary in JS). That's it. Any object in JS is a map in Clojure, which keeps everything nice and simple. The main power of this is you only ever need to support lists or maps in your functions, and then your functions work for every data structure you ever create! For example clojure.core ships with 'get-in' 'assoc-in', 'diff' etc, all functions that work on your structures no matter how complex.
2. It is a functional language: JS is imperative, meaning you have to fit your ideas to the language, breaking everything down into for loops and if statements. With Clojure you fit the language to the idea, and think in data transformations instead. Then you create a set of functions that deal with that problem specifically, all wrapped up in single namespace. For example a 'tilemap' ns that contains a set of functions for converting to/from screen and grid coordinates. Or getting the neighbours of a specified tile from the 2d array. The end result is a custom DSL that reads almost like English.
3. It is 'immutable by default': All data structures are persistent. The problems you have with scaling in JS and Python is all because of mutable local and global state, as it becomes very difficult to know what is changing what. Clojure doesn't have this problem, as values can't be edited, only new ones returned. There is still mutability of course, but it is restricted to maybe 10 locations in your codebase. The mental burden this lifts from your shoulders cannot be understated.
4. It has a REPL: Let me ask how much effort you think building a HTML editor is? Or the UI designer in Visual Studio? With Clojure, I can just make edits to the GUI code on the fly and press F10 and voila the changes appear in-app. Instant editor, for free. This is what i was doing the other day; editing my GUI code (re-arranging controls, changing positions and sizes) and then immediately inspecting the result in the running program. The productivity gains are huge when you remove the laborious 'write code, wait for build, navigate to place in the app, finally test your changes, find error, end program, change code, repeat' cycle from your workflow.
5. Macros: Lisp macros are just Lisp code again. Literally the whole language available to you at compile time. The clojure.async library for example uses this to provide Go style channels for async programming. It means you can write code that looks great, and still compiles down to something performant at the end.
Thanks for the response! +1! Let me take a stab at these points, bearing in mind that I'm not a JS fan or a Clojure opponent; just playing devil's advocate for my own learning purposes:
1. I accept that there are only lists and maps and primitives in Clojure, but I think the same is true of JS. The problem is that functions depend on these map/list structures having a particular schema, so in essence you can't just pass any old list or map to a function and have it do the right thing. I guess I don't see how Clojure and JS differ here.
2. What's stopping you from programming JS in a functional style? It's very possible to avoid `for` in JS (not sure what Clojure uses instead of `if` though). The JS standard library offers many functional features, and there are libraries dedicated to exactly this. I don't see how JS differs from Clojure here, except that it also supports an imperative style and "less is more".
3. If you're disciplined, you can do the same in JS or Python, but I accept that having rails in a language is better than resorting to discipline. The problems I mentioned with scaling JS and Python were related to typing (see point 1), not mutating state. I'm not sure what you mean by mutability introducing scaling problems, but Go is a mutable-by-default language which scales very nicely, both in terms of project size and parallelism (while I accept that immutability makes for easier parallelism, JS and Python's lack of parallelism have nothing to do with mutability except in the runtime). Clojure supports parallelism, which JS does not, so +1 for Clojure here.
4. I hear this a lot from Clojure proponents. The only REPL I've used is Python's, and I'm not a fan, but I understand that the Clojure REPL is a different beast entirely. I'll have to take you at your word here. Clojure beats JS here.
5. JS doesn't actually compile, so you can do all the metaprogramming you like. I also understand that JS has generators and coroutines, which should make async JS suck less; however, I haven't used them yet.
It seems like the biggest advantages Clojure has over JS are:
A) REPL B) Parallelism C) Rails + conventions > discipline
Thoughts?
1. I accept that there are only lists and maps and primitives in Clojure, but I think the same is true of JS. The problem is that functions depend on these map/list structures having a particular schema, so in essence you can't just pass any old list or map to a function and have it do the right thing. I guess I don't see how Clojure and JS differ here.
2. What's stopping you from programming JS in a functional style? It's very possible to avoid `for` in JS (not sure what Clojure uses instead of `if` though). The JS standard library offers many functional features, and there are libraries dedicated to exactly this. I don't see how JS differs from Clojure here, except that it also supports an imperative style and "less is more".
3. If you're disciplined, you can do the same in JS or Python, but I accept that having rails in a language is better than resorting to discipline. The problems I mentioned with scaling JS and Python were related to typing (see point 1), not mutating state. I'm not sure what you mean by mutability introducing scaling problems, but Go is a mutable-by-default language which scales very nicely, both in terms of project size and parallelism (while I accept that immutability makes for easier parallelism, JS and Python's lack of parallelism have nothing to do with mutability except in the runtime). Clojure supports parallelism, which JS does not, so +1 for Clojure here.
4. I hear this a lot from Clojure proponents. The only REPL I've used is Python's, and I'm not a fan, but I understand that the Clojure REPL is a different beast entirely. I'll have to take you at your word here. Clojure beats JS here.
5. JS doesn't actually compile, so you can do all the metaprogramming you like. I also understand that JS has generators and coroutines, which should make async JS suck less; however, I haven't used them yet.
It seems like the biggest advantages Clojure has over JS are:
A) REPL B) Parallelism C) Rails + conventions > discipline
Thoughts?
True Javascript has maps, and you could use immutable.js for your structures. It also has functional capabilities too thesedays. But the difficult part of language design is actually making all these pieces work together fluidly. This is what Clojure achieves.
Immutable.js is great until I need to use a 3rd party lib that doesn't support the structures, so there is a copy involved and performance is lost and the code gets ugly. Functional constructs were botched into JS, so most code out there is a litter of imperative and functional, as well as containing lots of mutable global state. It's object orientated, losing much of the benefits that come from being functional first.
> I'm not sure what you mean by mutability introducing scaling problems
Side-effect free programming makes reasoning about your code easier. More here: https://stackoverflow.com/questions/214714/mutable-vs-immuta...
> The only REPL I've used is Python's
I've not used it, but the point is you can change code and upload it as the programs runs. Great for tweaking stuff. And because there's no global mutable state, you don't have to restart the REPL very often as everything just works.
> JS doesn't actually compile
Actually it is compiled on page load. Also JS has no macros, but it does have some metaprogramming capabilities at runtime (reflection mainly). Again though, having a feature doesn't make it any good. Clojure's consistent and easy API blows JS out of the water.
Immutable.js is great until I need to use a 3rd party lib that doesn't support the structures, so there is a copy involved and performance is lost and the code gets ugly. Functional constructs were botched into JS, so most code out there is a litter of imperative and functional, as well as containing lots of mutable global state. It's object orientated, losing much of the benefits that come from being functional first.
> I'm not sure what you mean by mutability introducing scaling problems
Side-effect free programming makes reasoning about your code easier. More here: https://stackoverflow.com/questions/214714/mutable-vs-immuta...
> The only REPL I've used is Python's
I've not used it, but the point is you can change code and upload it as the programs runs. Great for tweaking stuff. And because there's no global mutable state, you don't have to restart the REPL very often as everything just works.
> JS doesn't actually compile
Actually it is compiled on page load. Also JS has no macros, but it does have some metaprogramming capabilities at runtime (reflection mainly). Again though, having a feature doesn't make it any good. Clojure's consistent and easy API blows JS out of the water.
> Immutable.js is great until I need to use a 3rd party lib that doesn't support the structures, so there is a copy involved and performance is lost and the code gets ugly.
Don't use a library for immutability, just don't mutate. Easy-peasy.
> Functional constructs were botched into JS, so most code out there is a litter of imperative and functional, as well as containing lots of mutable global state. It's object orientated, losing much of the benefits that come from being functional first.
Yeah, multi-paradigm code is a pain.
> Actually it is compiled on page load. Also JS has no macros
If we're being pedantic, it compiles continually during interpretation as most popular implementations use JIT compilation. But my point is that macros wouldn't benefit such a language because there is no discrete compile phase.
> it does have some metaprogramming capabilities at runtime (reflection mainly)
I guess I'm not very familiar with metaprogramming. Most anything I can do with macros in a compiled language I could do at runtime in a dynamic language without special standard library or language support. I'll take you on your word that metaprogramming is useful and that Clojure does it better.
Anyway, I don't think you answered one of my questions--how is Clojure's IDE support? Can it do gotodef or tell you about the types of parameters, etc?
Don't use a library for immutability, just don't mutate. Easy-peasy.
> Functional constructs were botched into JS, so most code out there is a litter of imperative and functional, as well as containing lots of mutable global state. It's object orientated, losing much of the benefits that come from being functional first.
Yeah, multi-paradigm code is a pain.
> Actually it is compiled on page load. Also JS has no macros
If we're being pedantic, it compiles continually during interpretation as most popular implementations use JIT compilation. But my point is that macros wouldn't benefit such a language because there is no discrete compile phase.
> it does have some metaprogramming capabilities at runtime (reflection mainly)
I guess I'm not very familiar with metaprogramming. Most anything I can do with macros in a compiled language I could do at runtime in a dynamic language without special standard library or language support. I'll take you on your word that metaprogramming is useful and that Clojure does it better.
Anyway, I don't think you answered one of my questions--how is Clojure's IDE support? Can it do gotodef or tell you about the types of parameters, etc?
The problem is JS is built from the ground up to be mutable. For example one big difference in Clojure is that all mutation is done through the Atom, which is transactional, making it threadsafe.
I wasn't being pedantic saying JS is compiled, because it really is. Sure it's compiled to an IR though, which is then JIT compiled as needed.
Nice thing about macros is they are zero cost abstractions, so there is no overhead added by using them. For example in C# using Linq creates garbage, so you can't use it in a game engine else you get freezes every couple of seconds as the GC does a collection. With macros you can have the convenience while still compiling to something that is memory efficient.
As for an IDE, look at the Cursive plugin for IntelliJ. It's free for personal use and gives you a debugger, autocomplete, errors, goto definition, find usages etc.
I wasn't being pedantic saying JS is compiled, because it really is. Sure it's compiled to an IR though, which is then JIT compiled as needed.
Nice thing about macros is they are zero cost abstractions, so there is no overhead added by using them. For example in C# using Linq creates garbage, so you can't use it in a game engine else you get freezes every couple of seconds as the GC does a collection. With macros you can have the convenience while still compiling to something that is memory efficient.
As for an IDE, look at the Cursive plugin for IntelliJ. It's free for personal use and gives you a debugger, autocomplete, errors, goto definition, find usages etc.
The following responses are terse because I'm posting from my phone. Apologies in advance!
JS is not parallelized, so whether or not it's thread safe is a moot point.
Python is also compiled to a bytecode before interpretation; were still don't call it a compiled language.
In a JIT language, macros aren't significantly faster than runtime abstractions. In the latter case, you can always precompile your abstraction on program load at the expense of slower start times (think regex engines or precompile linq queries). The cost is negligible.
I can't seem to find anything on type documentation for Cursive. How can I ask it what type a function returns or what types it's arguments should take?
JS is not parallelized, so whether or not it's thread safe is a moot point.
Python is also compiled to a bytecode before interpretation; were still don't call it a compiled language.
In a JIT language, macros aren't significantly faster than runtime abstractions. In the latter case, you can always precompile your abstraction on program load at the expense of slower start times (think regex engines or precompile linq queries). The cost is negligible.
I can't seem to find anything on type documentation for Cursive. How can I ask it what type a function returns or what types it's arguments should take?
> JS is not parallelized
https://johnresig.com/blog/web-workers/
https://ponyfoo.com/articles/understanding-javascript-async-...
> Python is also compiled to a bytecode before interpretation; were still don't call it a compiled language.
https://softwareengineering.stackexchange.com/questions/2455...
> macros aren't significantly faster
> you can always precompile your abstraction on program load at the expense of slower start times
http://www.ilikebigbits.com/blog/2015/12/6/the-fastest-code-...
> How can I ask it what type a function returns or what types it's arguments should take?
http://www.braveclojure.com/core-functions-in-depth/
https://johnresig.com/blog/web-workers/
https://ponyfoo.com/articles/understanding-javascript-async-...
> Python is also compiled to a bytecode before interpretation; were still don't call it a compiled language.
https://softwareengineering.stackexchange.com/questions/2455...
> macros aren't significantly faster
> you can always precompile your abstraction on program load at the expense of slower start times
http://www.ilikebigbits.com/blog/2015/12/6/the-fastest-code-...
> How can I ask it what type a function returns or what types it's arguments should take?
http://www.braveclojure.com/core-functions-in-depth/
> https://johnresig.com/blog/web-workers/
Sorry, I should have said "JS doesn't support shared memory parallelism for all intents and purposes, so memory sharing concerns are a moot point".
> https://softwareengineering.stackexchange.com/questions/2455....
This supports my point; not sure why you're posting this...
> http://www.ilikebigbits.com/blog/2015/12/6/the-fastest-code-....
This is also congruent with my points; if this is meant to be contradiction, you'll have to clarify.
> http://www.ilikebigbits.com/blog/2015/12/6/the-fastest-code-....
I'm not spending any more of my time skimming these mysterious links; this is a very straightforward question and you've evaded it several times and then referred me to an 8 kiloword document. What gives?
Sorry, I should have said "JS doesn't support shared memory parallelism for all intents and purposes, so memory sharing concerns are a moot point".
> https://softwareengineering.stackexchange.com/questions/2455....
This supports my point; not sure why you're posting this...
> http://www.ilikebigbits.com/blog/2015/12/6/the-fastest-code-....
This is also congruent with my points; if this is meant to be contradiction, you'll have to clarify.
> http://www.ilikebigbits.com/blog/2015/12/6/the-fastest-code-....
I'm not spending any more of my time skimming these mysterious links; this is a very straightforward question and you've evaded it several times and then referred me to an 8 kiloword document. What gives?
The "documentation for humans" effect is also the only effect that has had at least some empirical validation[1]. Interestingly, it is not necessary to have the type names/annotations actually statically checked.
[1] https://sites.google.com/site/stefanhanenberg/
[EDIT] Clarified which effect
[1] https://sites.google.com/site/stefanhanenberg/
[EDIT] Clarified which effect
> That's also the only effect that has had at least some validation scientifically
Which effect, sorry? I can't identify the referent of "That".
Which effect, sorry? I can't identify the referent of "That".
Sorry, fixed. They also studied "time to completion" and "correctness" for a new task, and for those the dynamic languages did better.
Thanks. After commenting I read the first paper in the page you linked. The one about trying to give an advantage to dynamic languages (Groovy vs Java), and measuring time-to-completion, for 4 tasks.
Turns out a static language has a time advantage when using an API, but a dynamic one has an advantage when writing code (that nobody will reuse).
Turns out a static language has a time advantage when using an API, but a dynamic one has an advantage when writing code (that nobody will reuse).
> This was experience from the Strongtalk project, which implemented a fast, typed Smalltalk.
That sounds like the global optimum of what I want in a language.
> They actually expected the correctness factor to be much higher, but in practice the static type system only helped to find one or two minor bugs in largely unused code-paths in the libraries.
Maybe these were already mature, well tested libraries?
That sounds like the global optimum of what I want in a language.
> They actually expected the correctness factor to be much higher, but in practice the static type system only helped to find one or two minor bugs in largely unused code-paths in the libraries.
Maybe these were already mature, well tested libraries?
"That sounds like the global optimum of what I want in a language."
I'd love to see them pitted against each other on many types of programming problems with same tooling and similarly-skilled developers. I want to know what differences there would be on large programs in terms of productivity, defect introduction, defect removal, and maintenance-level changes.
I'd love to see them pitted against each other on many types of programming problems with same tooling and similarly-skilled developers. I want to know what differences there would be on large programs in terms of productivity, defect introduction, defect removal, and maintenance-level changes.
because the JIT will fix it
> This has not been borne out in practise.
Exactly. http://blog.metaobject.com/2015/10/jitterdammerung.html
Exactly. http://blog.metaobject.com/2015/10/jitterdammerung.html
To make things faster, the memory layout matters these days.
The type system is a convenient way to express memory layout. Java is a bad example, because it intentionally hides the memory layout. You could use other means than the type system, but I don't know any examples off the top of my head. Maybe some Python meta class magic?
The type system is a convenient way to express memory layout. Java is a bad example, because it intentionally hides the memory layout. You could use other means than the type system, but I don't know any examples off the top of my head. Maybe some Python meta class magic?
> Research on Types and Soundness smothers research on programming languages
Perhaps, but you could turn it around, too.
Statically typed languages had time to catch up because innovation into "more powerful/better language mechanisms" has stalled, for some other reasons.
Perhaps, but you could turn it around, too.
Statically typed languages had time to catch up because innovation into "more powerful/better language mechanisms" has stalled, for some other reasons.
innovation into "more powerful/better
language mechanisms" has stalled, for
some other reasons.
- verification
- concurrency/parallelism
because both are beset with deep unsolved problems: for verification the problem is how to do it efficiently (we know we can do it in principle), and for concurrency/parallelism we have not yet discovered core abstractions including the right types that can express simple properties of concurrency/parallelism (at least that is my working hypothesis). This is intimately related to our current inability to auto-parallelise.
> For sequential languages there is probably not much to improve -- except at the edges. ML nailed it.
And that's the problem right there. There is sooo much that is out of whack with programming, even sequential.
For starters look up 'architectural mismatch'.
And that's the problem right there. There is sooo much that is out of whack with programming, even sequential.
For starters look up 'architectural mismatch'.
That was solved with formal specifications in languages such as Z, CSP, ASM's, B, and recently TLA+. Even if you don't do proof, high-assurance projects would specify context of sequential components in such languages to find mismatches at interfaces, protocol errors, and so on. It got pretty easy to do, too. The tooling is really good for that now esp on TLA+ end.
So, there's not so much a problem in programming languages with architecture so much as programmers ignoring proven ways of catching such problems. Usually what I just mentioned plus review and testing. People like hwayne are laying groundwork for reductions in this problem by making accessible tutorials showing practical value of such techniques.
https://learntla.com/introduction/
So, there's not so much a problem in programming languages with architecture so much as programmers ignoring proven ways of catching such problems. Usually what I just mentioned plus review and testing. People like hwayne are laying groundwork for reductions in this problem by making accessible tutorials showing practical value of such techniques.
https://learntla.com/introduction/
>ML nailed it.
Then why does Haskell exist? And if Haskell nailed it, why does the Backpack module system exist?
Clearly, nobody has "nailed it".
Then why does Haskell exist? And if Haskell nailed it, why does the Backpack module system exist?
Clearly, nobody has "nailed it".
Haskell is an ML variant, that basically extends ML with higher-kinded types, which are used -- among other things -- to constrain effects monadically.
One under-appreciated aspect of static types is that they make certain classes of stupidity a little more difficult, for example, overloading the permissible types on an object's member variable such that every bit of code that uses it needs to do an `isinstance()` check to see if it has the type that particular bit of code wants. Doing this would be tedious in a statically typed language where the sane solution is often the easier solution. This doesn't mean it's hard to write bad code in a static language, just that it's harder to do by accident.
Although it'll always be tempting to provide isinstance() type checks in your dynamic language, there's no reason you have to have them!
Over the last few years I've started using them a lot simply because it means you get simpler, clearer and more actionable errors more quickly.
They're especially useful when you are writing libraries for use by somebody else.
They're especially useful when you are writing libraries for use by somebody else.
Yeah -- a dynamic language could provide an assertinstance() operation, which throws an error if the types don't match, without going all the way to a boolean isinstance() check.
This is basically the "correctness" argument for static typing. That you do this in a dynamic language is a liability.
Placing a small number of sanity (hint: it's not always type that needs checking) checks on border code is not any kind of argument for static typing.
I'd do the same thing in most languages - in fact, I'd end up doing way way way more of it in C because it's very weakly typed.
I'd do the same thing in most languages - in fact, I'd end up doing way way way more of it in C because it's very weakly typed.
> it's not always type that needs checking
I think type theorists would disagree.
> Placing a small number of sanity checks on border code is not any kind of argument for static typing.
Yes it is if any of those checks are for types.
> I'd do the same thing in most languages - in fact, I'd end up doing way way way more of it in C because it's very weakly typed.
C doesn't have type checks, unless you're using some runtime type system (like GObject) on top of it. At any rate, C may not be completely type safe, but it's better than dynamic languages which are completely type unsafe; even if you could do type assertions, you would do them far less frequently in C than, say, Python. Further, C is not the canonical statically typed language, and you would be laughed out your workplace if you proposed adding a runtime type check on your function parameters.
Even if you're using Python (assuming you have the good fortune to use a modern version), you can just use type annotations and the static type checker rather than littering the code and slowing your program. Albeit your point stands about writing library code for another's consumption.
I think type theorists would disagree.
> Placing a small number of sanity checks on border code is not any kind of argument for static typing.
Yes it is if any of those checks are for types.
> I'd do the same thing in most languages - in fact, I'd end up doing way way way more of it in C because it's very weakly typed.
C doesn't have type checks, unless you're using some runtime type system (like GObject) on top of it. At any rate, C may not be completely type safe, but it's better than dynamic languages which are completely type unsafe; even if you could do type assertions, you would do them far less frequently in C than, say, Python. Further, C is not the canonical statically typed language, and you would be laughed out your workplace if you proposed adding a runtime type check on your function parameters.
Even if you're using Python (assuming you have the good fortune to use a modern version), you can just use type annotations and the static type checker rather than littering the code and slowing your program. Albeit your point stands about writing library code for another's consumption.
>C doesn't have type checks, unless you're using some runtime type system (like GObject) on top of it. At any rate, C may not be completely type safe, but it's better than dynamic languages which are completely type unsafe
And worse than dynamic languages which have greater type-safety. Point being that it's type safety, not static typing that helps cut down on the need for sanity checking.
>you can just use type annotations
Type annotations are both unchecked and render any code that you write unusable in python 2.
>rather than littering the code
Type annotations DO litter the code.
And worse than dynamic languages which have greater type-safety. Point being that it's type safety, not static typing that helps cut down on the need for sanity checking.
>you can just use type annotations
Type annotations are both unchecked and render any code that you write unusable in python 2.
>rather than littering the code
Type annotations DO litter the code.
> And worse than dynamic languages which have greater type-safety
I think you're confusing strong typing with type safety. Strong typing doesn't preclude errors; you just don't see the error until you hit the code, which might be all the time for a happy path, or almost never for an error path. Static typing, on the other hand, completely eliminates the need for sanity type checks (and depending on your language's notion of 'type' this can include virtually all forms of sanity checks).
> Type annotations are both unchecked and render any code that you write unusable in python 2
Static type checking is supported for both Python 2 and 3. If you need to write Python 2/3, you could probably just use the Python 2 annotations.
> Type annotations DO litter the code.
They don't. They're a small annotation that tells you what the variable actually is/does. Much neater than Sphinx docs, etc. And you do need to know the type, whether you like it or not.
I think you're confusing strong typing with type safety. Strong typing doesn't preclude errors; you just don't see the error until you hit the code, which might be all the time for a happy path, or almost never for an error path. Static typing, on the other hand, completely eliminates the need for sanity type checks (and depending on your language's notion of 'type' this can include virtually all forms of sanity checks).
> Type annotations are both unchecked and render any code that you write unusable in python 2
Static type checking is supported for both Python 2 and 3. If you need to write Python 2/3, you could probably just use the Python 2 annotations.
> Type annotations DO litter the code.
They don't. They're a small annotation that tells you what the variable actually is/does. Much neater than Sphinx docs, etc. And you do need to know the type, whether you like it or not.
>I think you're confusing strong typing with type safety.
Check the wikipedia page for strong typing. Type safety is one of the ~11 or so different definitions. It's one reason I try to avoid using the term - because it's more emotional than meaningful.
>Static typing, on the other hand, completely eliminates the need for sanity type checks
You've not programmed in C have you?
Check the wikipedia page for strong typing. Type safety is one of the ~11 or so different definitions. It's one reason I try to avoid using the term - because it's more emotional than meaningful.
>Static typing, on the other hand, completely eliminates the need for sanity type checks
You've not programmed in C have you?
[deleted]
I agree; but there's nothing enforcing it either, and I always prefer rails for enforcing best practices rather than code review (where egos tend to be bruised, feedback takes longer, etc etc).
Depressing that correctness comes in last, especially since it includes so many valuable sub properties, among which
1. Correctness of the code
2. Correctness of automatic refactorings, which dynamically typed languages can never achieve, which is why refactoring a dynamically typed language always requires the supervision of a human
1. Correctness of the code
2. Correctness of automatic refactorings, which dynamically typed languages can never achieve, which is why refactoring a dynamically typed language always requires the supervision of a human
I think it's tragic how easily dismissed ML/Miranda-evolved languages are considered a priori bad.
What is more interesting about a sound type system is what category theory enables. Proven composition, sound abstractions, etc. I'm not a huge fan of category theory but it undeniably useful. In practice this means we get very rich, provable composition.
It's quite liberating how far good, reasonable constraints can take you.
What is more interesting about a sound type system is what category theory enables. Proven composition, sound abstractions, etc. I'm not a huge fan of category theory but it undeniably useful. In practice this means we get very rich, provable composition.
It's quite liberating how far good, reasonable constraints can take you.
it's tragic
Dart could have been such a great language if it was statically typed but Bracha's obsession with dynamic types ruined that effort.
They pivoted a lot in that direction. Dart's strong mode is statically typed and sound and all that, except that you can say "dynamic" if you really need to.
Yes, so they realized that statically typed languages are superior years after creating the language, which is something we've learned and known for more than ten years.
Retrofitting a type system into a dynamically typed language has never been done successfully and it's unlikely Dart will invalidate that claim.
It's really a pity, Dart could have been a game changer.
Retrofitting a type system into a dynamically typed language has never been done successfully and it's unlikely Dart will invalidate that claim.
It's really a pity, Dart could have been a game changer.
I don't think they had any such "realization" about a superiority of static typing, especially as research indicates that there are tradeoffs between dynamic and static typing, not that there is superiority of one or the other model. Both Bracha and Felleisen tend to fall in the soft [1] or gradual [2] typing camp, after all. See, for example, Bracha's paper on pluggable type systems [3].
As for retrofitting a type system into a dynamically typed language, Dart had gradual typing from the beginning (with types being checked at runtime), so it's an entirely different beast from (say) Ruby or Python.
[1] http://wiki.c2.com/?SoftTyping
[2] https://en.wikipedia.org/wiki/Gradual_typing
[3] http://bracha.org/pluggableTypesPosition.pdf
As for retrofitting a type system into a dynamically typed language, Dart had gradual typing from the beginning (with types being checked at runtime), so it's an entirely different beast from (say) Ruby or Python.
[1] http://wiki.c2.com/?SoftTyping
[2] https://en.wikipedia.org/wiki/Gradual_typing
[3] http://bracha.org/pluggableTypesPosition.pdf
> especially as research indicates that there are tradeoffs between dynamic and static typing
Not really.
How come there are plenty of dynamically typed languages that are migrating toward optionally static typing but never the other way around?
Even Bracha himself, a very strong advocate of dynamically typed languages, has felt the need to work on Strongtalk and then later, to have Dart support optional static types.
Today, we have very good type inference engines and there is really no reason to ever want to use a dynamically typed language. This is the trend, this is the present and the future.
Javascript is going to be around for a while for legacy reasons but in a few years, we'll look back at dynamically typed languages with a fond "Yeah, it was a good idea at the time but we know better now" look.
Not really.
How come there are plenty of dynamically typed languages that are migrating toward optionally static typing but never the other way around?
Even Bracha himself, a very strong advocate of dynamically typed languages, has felt the need to work on Strongtalk and then later, to have Dart support optional static types.
Today, we have very good type inference engines and there is really no reason to ever want to use a dynamically typed language. This is the trend, this is the present and the future.
Javascript is going to be around for a while for legacy reasons but in a few years, we'll look back at dynamically typed languages with a fond "Yeah, it was a good idea at the time but we know better now" look.
> Not really.
Can you provide support for this claim? Existing research [1] seems to indicate that it isn't clear-cut at all.
> Today, we have very good type inference engines and there is really no reason to ever want to use a dynamically typed language.
Type inference has its shares of issues once you're dealing with non-local type inference, subtype polymorphism or parametric polymorphism.
[1] https://danluu.com/empirical-pl/
Can you provide support for this claim? Existing research [1] seems to indicate that it isn't clear-cut at all.
> Today, we have very good type inference engines and there is really no reason to ever want to use a dynamically typed language.
Type inference has its shares of issues once you're dealing with non-local type inference, subtype polymorphism or parametric polymorphism.
[1] https://danluu.com/empirical-pl/
> Type inference has its shares of issues once you're dealing with non-local type inference, subtype polymorphism or parametric polymorphism.
Just wanted to point out that actually, type inference works quite well with parametric polymorphism, like in ML. Even non-local type inference can work fine given other constraints, also like in ML.
Just wanted to point out that actually, type inference works quite well with parametric polymorphism, like in ML. Even non-local type inference can work fine given other constraints, also like in ML.
1. Only for unconstrained parametric polymorphism. For constrained parametric polymorphism, ML requires functors (don't get me wrong, I think ML functors are brilliant, but they do require you to be rather explicit about your typing).
2. I wouldn't say that it's without problems even for unconstrained parametric polymorphism. Consider the value restriction [1] and the fact that if you add subtyping to the mix (as in OCaml), you're getting some really non-trivial issues (as Scala found out the hard way).
[1] http://mlton.org/ValueRestriction
2. I wouldn't say that it's without problems even for unconstrained parametric polymorphism. Consider the value restriction [1] and the fact that if you add subtyping to the mix (as in OCaml), you're getting some really non-trivial issues (as Scala found out the hard way).
[1] http://mlton.org/ValueRestriction
Yes, subtyping makes everything more complicated. I think there was a paper about type inference for subtyping posted on HN a while back, but I don't remember much about it.
Citation needed. Oh, and: wrong. And you obviously didn't listen to the talk...
Q: "Do you hate static types" GB: "No" MF: "No"
GB: "Types are useful for: 1. Doc for human 2. Doc for machine 3. Making things faster … 4. Correctness"
This was experience from the Strongtalk project, which implemented a fast, typed Smalltalk. Strongtalk was purchased by Sun and the tech. was the basis for Java's Hotspot. They actually expected the correctness factor to be much higher, but in practice the static type system only helped to find one or two minor bugs in largely unused code-paths in the libraries. I also find it interesting that "making things faster" is on the list, because the mantra from that part of the discipline has always been that static types do not help for performance, because the JIT will fix it all.
MF: “Research on Types and Soundness smothers research on programming languages”
Clarifying, says something along the lines that you have to figure out more powerful/better language mechanisms first, then later start thinking about how to type them properly.