Why we're supporting Typed Clojure
blog.circleci.com
blog.circleci.com
http://www.eecs.northwestern.edu/~robby/pubs/papers/oopsla20...
[1] http://docs.racket-lang.org/
[2] The Type Racket Guide: http://docs.racket-lang.org/ts-guide/
[3] The Type Racket Reference: http://docs.racket-lang.org/ts-reference/
In other words, Racket is now being driven by research into computation and the earlier generation's area of emphasis - the pedagogy of computation - is being treated as a largely solved problem. This is not to say that PLT is no longer pursuing pedagogical projects or that in the past there wasn't significant discovery and invention within computation, only that the How to Design Programs project offers a mature and battle tested framework for teaching introductory programming and there is not a lot of reason to revisit it.
One of the things that attracts me to Racket - beyond the fact that it is a Lisp - is that the documentation is full stack. I was aware of the paper because there is a link within the Racket documentation of the contract system. The payoff from reading a paper that is specifically organized around the language at hand is intellectual continuity and when the language is a Lisp that continuity extends all the way from implementation to the lambda calculus.
Program verification is cool, but enabling "intellisense" on a hash is even cooler.
If the parser error recovery is decent (and there is some effort put into this in most substantial front ends, since it's key to good error messages in large projects with long compile times, where recompile on every error fix isn't a great experience), the code doesn't need to be in a good state.
I've found that most IDEs support two kinds of compilers: the compiler used to generate code and find type errors, and a "presentation" compiler to provide interactive feedback that is error tolerant and can run in incomplete contexts. Java works this way, Scala worked this way (at least when I was working on the plugin), C# has a lot of infrastructure separate from the compiler to support its use in Visual Studio. A lot of work goes into this infrastructure beyond "writing a decent compiler," and emacs very simple language-aware interface didn't seem to support it very well (when I looked ~8 years ago).
It is how the Delphi compiler works in the IDE. I used to work for Borland, then Embarcadero, on the compiler front end.
When the compiler is running for code completion (kibitz mode, it calls it), it does a lot less work. No codegen, no type analysis of function bodies (begin / end blocks are entirely skipped), unless the cursor location is discovered to be inside a function body, whereupon the it rewinds and does more complete analysis. Normally takes no more than a few milliseconds to finish.
It's basically the same UX as you're used to in Java, except the info comes from asking the running process, rather than parsing statically.
Happily, by the time I got around to working at a company like that, somebody had written Merlin which does not need anything like that. It even worked with js_of_ocaml, which was very impressive. I thought it was a very good tool.
[2]: http://kiwi.iuwt.fr/~asmanur/blog/merlin/
Emacs also has good support for a few other languages. Haskell has ghc-mod[3] and scion[4], for example.
[3]: http://www.mew.org/~kazu/proj/ghc-mod/en/
[4]: https://github.com/nominolo/scion
Similarly, there is ENSIME[5] for Scala.
[5]: https://github.com/aemoncannon/ensime
You can also use eclim[6] with Emacs, which integrates with Eclipse to offer rich functionality for Java.
[6]: https://github.com/senny/emacs-eclim
Of course, Emacs has language-aware editing for Emacs Lisp by default :). You can get similar support for most other popular dynamically typed languages as well.
So yes, Emacs does support plenty of languages like that, although almost always through a plugin. Happily, with the new package manager, installing and managing plugins is now trivial.
The word "hash" a shorthand for the noun-phrase "hash code" (aka "digest") and a verb for the process of creating hash codes.
Concretely, I've extended several minor ideas.
Typed Clojure uses occurrence typing in sequential forms, as well as conditionals: http://frenchy64.github.io/2013/09/08/simple-reasoning-asser...
We can type check (filter identity coll) a little more accurately (which is actually quite hard to do): https://github.com/clojure/core.typed/blob/master/src/main/c...
The type system's interaction with Java's type system is interesting, which is something I've fleshed out.
I have heterogeneous maps as well as heterogeneous vectors, and support complex operations like merge. Unsure if relevant to Racket.
There are lots of other ideas which I need to implement to type check Clojure, but aren't necessarily crucial to type checking Racket, but would be nice to have.
Clojure's type system sounds more powerful than Typescript's though.
I guess Typed Clojure is more powerful than Typescript in a few ways, but it's more about how well the type system fits the language. I've never used Typescript, but it seems to fit nicely, with interesting tradeoffs.
Based on my experience, dynamic languages without optional typing make large scale enterprise development unbearable.
Sure, one should be writing unit tests, but in the enterprise context those tests rarely do exist, or if they do, either don't test what they should or are so complex that invalidate any re-factoring taking place.
I'm curious how many runtime errors persist due to the optionality of the type system. Perhaps code standards requiring all "library" code to be typed would be a good balance.
Most enterprise customers I have worked with, favour dynamic languages just for scripting tasks, while using static typed ones for the large scale projects.
By large scale, I mean, projects with at least three development sites, at least 30 developers, all the different set of skills. With lots of attrition.
The only time I saw it working, was in a project done with TCL, which lacks optional types, but everyone on team was a top developer, the team was small, and located on the same open space. So startup world, not enterprise.
Sample:
@typ((int,float), ret=(int,float))
def square(x):
return x*x
It doesn't currently let you compose types, but that wouldn't be too difficult to add, e.g. {str:int} could mean a dictionary whose keys are strings and values are integers.
@typ[A implements *](A, ret=A)
def square(x):
return x * x
BTW, your printargs looks pretty cool! I might just makes something like that for JS...
I don't think that's possible in Python.
> Also, what you'd really want is something that implements type variables
That is possible, you could check what the type of the incoming parameter is and then check that the return value is the same type. I'm not sure that there's an obvious syntax for saying this, but one could always send a string to @typ and have it parse some made-up syntax.
I suspect this would be a lot of effort and it would probably make sens to use a typed language, instead of trying to shoehorn it into Python. I invented @typ so I could quickly document the types in my functions, & with the added advantage that it catches some errors.
> your printargs looks pretty cool! I might just makes something like that for JS...
I look forward to seeing it.
It's a nice feature, but calling it "one of the biggest advancements to dynamic programming languages in the last few decades" is ignorant.
Pre- and post-checks are of course possible, but I've rarely seen them used in practice. More importantly, they can't be used to provide any sort of correctness guarantee, which static typing can.
I'm not sure what you mean by tagged values and pattern matching - I know what those concepts are, but I think you're saying they're widely used by good developers? I have not seen evidence for this.
The reason I call it one of the biggest advancements is that it is actually being used in production, has low overhead (both in cognitive load and performance-wise), and actually handles the complexities of duck-typing. It shows that it is practical. (By contrast, Erlang is sufficiently different to most other dynamic languages, both in use case and semantics, that it is difficult to generalize from Erlang to say Python).
I agree, I wish more people (especially Javascript developers) saw the value of pre (and post!) checking.
>The reason I call it one of the biggest advancements is that it is actually being used in production, has low overhead (both in cognitive load and performance-wise), and actually handles the complexities of duck-typing. It shows that it is practical. (By contrast, Erlang is sufficiently different to most other dynamic languages, both in use case and semantics, that it is difficult to generalize from Erlang to say Python).
This is fair, I just meant to point out that conceptually this isn't new, it's just a new implementation. Can you expand a bit on what you said about duck-typing?
So the type of an object in a duck-typed language is based on the functions and fields it has _now_, not its instance type. Since there is no name for that type, you cannot do "nominal" typing. Instead, you must use "structural" typing, which checks its structure. This is exactly what Typed Clojure does.
An example of how that works in practice, is you say that the 2nd parameter must be a map with one of the following configurations: a key named :foo and a key named :bar, both mapping to strings, or a key named :error, mapping to a string.
NB. And I believe Perl6 in certain cases will/can raise compile-time type errors.
nil isn’t allowed
If this really is what I think it is (a certain reference to a class can never be nil) then I am really excited. It never made sense to me that someone was able to call a function I wrote that really needed instances with nils instead, so I was forced to check and throw in case they did. It's just not clear and it leads to a lot of unnecessary checking or nil pointer exceptions.
This rough screencast describes on aspect to the approach http://vimeo.com/55280915
Great language too if you're down with .NET.
I'm sure there have been great advances. But you are showcasing this as if it was a completely new idea, even though PHP has been using it for a long time. Correct me if I'm wrong.
$f = function helloAction(Http\Request $request) {
$response = new Http\Response("Hello " . $request->query->get('name'), 200);
$response->setMa // at this point the IDE will show a list of methods like 'setMaxAge($time)', because it knows its type
};
$someObject->someMethod($f);
protected method someMethod($f) {} // no checks!
protected method someMethod(\Closure $f) {} // only an argument of type Closure will be accepted.
Response $r = new Response(...);
Of course, in this example, it's silly and type inference would be used to ensure that you don't need to write the left side.
The advantage is that before running your code you can suss out much greater degrees of what your code "could possibly mean". The \Closure bit is a start, but it needs to fail prior to running to be statically typed. It also could potentially include much more information like (\Closure[Http\Request -> Http\Response]) and reject even more bad arguments.
http://research.microsoft.com/apps/pubs/default.aspx?id=1961...
I think we can go much farther in this area than we have with Hindley Milner. Of course, this is still research, but as long as you are claiming "biggest advance in the last few decades" I might as well just throw this out there.
Unit testing is great for verifying that a piece of code works conforms to specification, but typing verifies that you're using a piece of code as expected. Two different things.
100% enumeration of runtime behaviors is another property, far stronger than any non-dependent static types today, but also exponentially more difficult than 100% test coverage.
Good static types are a cheap way to get probably halfway between those two on a log scale.