ambrosebs

I went back to Siek & Taha's original formulation and they have a nice examples section in 5.3 of some interesting higher-order cases with Dyn, that better demonstrates than my clumsy attempt.

http://www.cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_grad...

Right, I think when you have a Dyn, you import all untyped code as type Dyn or containing Dyn. Then the idea is, when you unwrap a Dyn function at runtime, to distribute the function checks to the domain and range of the function.

Say you had some untyped function `f` that is Dyn -> Dyn.

(defn f [a :- Dyn] :- Dyn a)

Running

(inc (f 1))

would wrap 1 in Dyn, then a Dyn exits as a return value, so no further wrapping is needed. Now it's `inc`'s responsibility to ensure it's really being passed a number, so it unwraps the Dyn and finds an int inside.

So you're right - it only works with first-order values without this kind of machinery, which end up looking pretty much like what I talk about in the article.

Great point.

`Any` is also often called `Dyn` or `Dynamic` in normal typed languages, which is slightly different to `Any` here (core.typed's `Any` is the supertype to all types, `Dyn` is usually both the super and subtype to all types).

It shouldn't be too surprising given the similarities between Clojure and Racket.

Typed Clojure and Typed Racket are very closely related in theory and implementation.

Typed Clojure is currently static analysis only and offers no automatic speed improvements. It has the nice property that code will compile and run no matter what the type checker thinks.

To type check Clojure idioms we use techniques that resemble light-weight dependent types. No particular attempt is made to go beyond the minimum required for checking certain idioms.

We can express lengths of sequences for example, but they only support explicit lengths: you can't put a type variable in the length position.

Clojure's map takes at least 2 arguments, so that's why we have an extra "a".

I also commented on the blog post explaining the terms I used.

The dotted type-variable on the right hand side of ... is what ensures both sets of dots get instantiated with the same sequence of types.

Both sides of b ... b are actually completely different. The left is a type (called a "pre-type") and the right is a dotted type variable currently in scope.

The trick is that the dotted type-variable is also scoped as a normal free variable in the pre-type.

It might help thinking of "b ... b" as expanding to "b1 b2 b3 b4 b5", where each is a fresh type variable.

Then, consider "(NonEmptySeqable b) ... b" as expanding to "(NonEmptySeqable b1) (NonEmptySeqable b2) (NonEmptySeqable b3) (NonEmptySeqable b4) (NonEmptySeqable b5)".

The b's "match up" pairwise, but they're quite different than what you might expect.

No reason.

Rich hasn't been directly involved, aside from providing encouragement.

Almost all the design/implementation work was done via Typed Racket anyway. I stole a lot of it and spent most of the time on Clojure-specific problems.

The information on what needs annotating isn't quite complete: loops and some other macros need annotations.

I'm probably responsible for the thinking that annotations are only needed for "top levels and function parameters". I usually forget about the other ones, but I think those two are the most significant.

So I tried out my ideas for type checking core.match with CinC, and it worked out wonderfully.

http://www.youtube.com/watch?v=g2zts1hW19k

Thanks.

Amusingly, Nicola (Bronsa) let me know CinC already provides the extension points for everything in the blog post.

(ns my-ns (:require [clojure.core.typed :as t :refer [ann]]))

(ann my-keys (All [a] [(t/Map a Any) -> (t/Coll a)])

There would be annotations in the same places as Typed Clojure, except :no-check would be replaced by type soundness-preserving runtime assertions. There would be no need for :no-check anyway; Typed Racket's base annotations are complete AFAIK.

I will tiptoe carefully around the issue you're bringing up and point out that the styles of type checking provided by Dialyzer and Typed Clojure are pretty different.

nil is explicit in Typed Clojure, and it's a goal to statically avoid misuses of nil.

This rough screencast describes on aspect to the approach http://vimeo.com/55280915

Typed Clojure's type system is too rich to avoid top-level annotations. It's a similar situation to Scala.

Thanks!

Yep that's correct. I want a tool that infers a rough approximation of top-levels to accelerate the process of porting untyped code to be typed. The programmer would inspect the annotations manually and fix any inaccurate ones, and then run the type checker.

AFAIK Typescript is level 1 gradual typing. Typed Clojure is also level 1, but I'm aiming for level 3.

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.

Also I'm not aware of a tool to "guess" top level annotations for Typed Racket. This is an area I want to explore further, soon.

Speaking speculatively, improving type inference is a great place for collaboration.

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.

FWIW I've been pushing Typed Clojure in interesting directions that can be directly applied back to Typed Racket. The implementations are so similar that there is good potential for cross pollination.

I managed to totally miss the claim that Typed Clojure uses ideas from PHP :/ I'm pretty sure there is no relation.

Oh right, a hash map. That would be very cool, and probably feasible to implement.

That's insane.

You're correct. Sam Tobin-Hochstadt is the star of the show, and is given a mention in the article, along with his fantastic Typed Racket.

What is intellisense on a hash?