Bracha v Felleisen “Types for an Untyped World” (2015) [video]
youtube.com
youtube.com
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.
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.
[1] https://sites.google.com/site/stefanhanenberg/
[EDIT] Clarified which effect
Which effect, sorry? I can't identify the referent of "That".
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).
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...
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.
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?
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. 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?
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.
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?
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.
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?
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?
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?
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'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.
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.
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.
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.
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'.
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.
Then why does Haskell exist? And if Haskell nailed it, why does the Backpack module system exist?
Clearly, nobody has "nailed it".
because the JIT will fix it
Exactly. http://blog.metaobject.com/2015/10/jitterdammerung.html
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?
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.
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?
They're especially useful when you are writing libraries for use by somebody else.
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 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.
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.
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.
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?
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
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
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.
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
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.
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.
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.
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).