ambrosebs

6 ms·

1.
by ambrosebs 11y ago
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&
2.
by ambrosebs 11y ago
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 h
3.
by ambrosebs 11y ago
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
4.
by ambrosebs 13y ago
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.
5.
by ambrosebs 13y ago
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.
6.
by ambrosebs 13y ago
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 the
7.
by ambrosebs 13y ago
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.
8.
by ambrosebs 13y ago
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-typ
9.
by ambrosebs 13y ago
No reason.
10.
by ambrosebs 13y ago
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.
11.
by ambrosebs 13y ago
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&q
12.
by ambrosebs 13y ago
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
13.
by ambrosebs 13y ago
Thanks.
14.
by ambrosebs 13y ago
Amusingly, Nicola (Bronsa) let me know CinC already provides the extension points for everything in the blog post.
15.
by ambrosebs 13y ago
(ns my-ns (:require [clojure.core.typed :as t :refer [ann]])) (ann my-keys (All [a] [(t/Map a Any) -> (t/Coll a)])
16.
by ambrosebs 13y ago
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 comple
17.
by ambrosebs 13y ago
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.
18.
by ambrosebs 13y ago
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
19.
by ambrosebs 13y ago
Typed Clojure's type system is too rich to avoid top-level annotations. It's a similar situation to Scala.
20.
by ambrosebs 13y ago
Thanks!
21.
by ambrosebs 13y ago
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 the
22.
by ambrosebs 13y ago
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 lan
23.
by ambrosebs 13y ago
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.
24.
by ambrosebs 13y ago
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://fr
25.
by ambrosebs 13y ago
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.
26.
by ambrosebs 13y ago
I managed to totally miss the claim that Typed Clojure uses ideas from PHP :/ I'm pretty sure there is no relation.
27.
by ambrosebs 13y ago
Oh right, a hash map. That would be very cool, and probably feasible to implement.
28.
by ambrosebs 13y ago
That's insane.
29.
by ambrosebs 13y ago
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.
30.
by ambrosebs 13y ago
What is intellisense on a hash?

More ›