Viewing profile — 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 clu…

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 functi…

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, `…

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 …

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 idio…

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 comple…

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 mo…

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 nee…

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-c…

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 an…

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'…

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.