Future directions for core.typed

[Ambrose Bonnaire-Sergeant]

Hi all,

Time for an update on the direction I hope to steer core.typed in the next year.

# Gradual typing.

We've already seen some prototyping of the core.typed REPL. This will

evolve into basically Typed Racket for Clojure, with automatic contract

enforcement for "gradually typed" namespaces.

One question is: will the core.typed that exists today be subsumed by gradual typing?

That is, will we still be able to use check-ns and completely optional type checking,

instead of being integrated into the REPL (a requirement of gradual typing).

I think the "optional" type system core.typed currently provides is very useful, and

probably a tool that should stick around.

I can see core.typed being used in several ways:

1. Annotating untyped namespaces without checking (purely documentation)

2. Optional type checking (can ship without core.typed)

3. Gradual type checking (need to AOT or ship with core.typed)

What happens if (3) interacts with (2)? Does (3) need to be protected from (2)

as if it was untyped like (1)?

Typed Clojure probably needs more knobs than Typed Racket here, while striving

for the safest defaults.

Immediate steps are:

- improving contracts support (adding higher-order casts)

- safely import untyped code and export gradually typed code via rewriting

- fix the quirks around REPL evaluation

  - eg. vim-fireplace likes to evaluate its internal completion code, which doesn't type check

# Propositions and Objects

There are some things I want to do with propositions.

1. Remove negative propositions

Negative type propositions can be replaced by the Not type (which I plan to add

better support for).

(! t 0) ==> (is (Not t) 0)

2. Better syntax for propositions

The current syntax is not good, especially with larger objects.

Even `identity` can be improved.

clojure.core/identity 

(All [x] [x -> x

          :filters {:then (! (U nil false) 0)

                    :else (is (U nil false) 0)}

          :object {:id 0}])

My first idea is to make :filters optional if you know the :object --- they can be trivially

inferred anyway. We can drop the :id.

clojure.core/identity 

(All [x] [x -> x :object 0])

It would be even nicer if we supported named parameters instead of just De Bruijn indices.

clojure.core/identity 

(All [x] [a :- x -> x :return-val a])

I also want to move away from using propositions and use

type environments at the syntax level. eg.

clojure.core/identity 

(All [x] [a :- x -> x

          :then [a :- (Difference x (U nil false))]

          :else [a :- (U nil false)]

          :object a])

That is, if `identity` returns true then `a` (ie. the argument) is of type

(Difference x (U nil false)) with some chosen `x`. This seems more readable.

I had an idea that every FilterSet can also carry a cached type environment with respect to the type environment it was created in, which

might make `filter` easier to type check with something like

clojure.core/filter

(All [x y]

  [[a :- x -> Any :then [a :- y]] 

   (Option (Seqable x)) 

   -> (ASeq y)])

In theory, looking up `y` is just a pattern match to the :then type environment

in eg. the annotation for identity.

# Refinement types

I want to type check code like this:

(fn [x :- (U Sym nil)]

  (let [[sym?] (if (symbol? x) [true] [false])

    (when sym?

      (name x))))

There are various ways to do this (one is to store the current environment

in each element of a HVec) but they all seem to generalise to refinement

types.

Another is to make the TCResult triple type/propositions/object be a real type,

which ends up being a kind of refinement type. One advantage to this approach

is that we only need to change a few places for all expressions to return refinement

types.

The type of `true` --- and thus sym? --- above would be

(Refine true

        :then [x :- Sym]

        :else [x :- Nothing])

so we can infer [x :- Sym] in the `name` call.

# Transducers

Supporting transducers requires more than just annotating them. The local

type inference implementation needs restructuring to improve constraint

resolution.

Even (map identity coll) cannot be currently checked, let alone inferring

an appropriate polymorphic type for the transducer (map identity).

Luckily, that is exactly what this paper tackles (see the example on the first page!).

We're pretty sure it can also check (map #(inc %) coll) for us. ie. elide annotations

for local functions.

It's unclear how far this inference goes --- I have a hunch it can help infer the

type for entire top-level functions if it knows the type of all the vars used inside of it.

I plan on chipping away at this over the next year.

# Type check more core functions

I've revisited some old favourites. Here's some notes I've compiled.

clojure.core/some-fn

; - Unions need to support dots for this to work:

; - ...+ is a non-empty ...

; - (or [y :- t] ... b) is a disjunction of propositions

;   expanded by dots (no idea how to implement this) like

;   (or [y :- t] [y0 :- t0] [y1 :- t1])

; - [y ... b :- e ... b] is a conjunction of propositions like

;   [y :- e, y1 :- e1, y2 :- e2]

;

; (All [i t e r b ...]

;   [[x :- i -> r :then [x :- t], :else [x :- e]] ...+ b

;    -> [y :- i ... b -> (U r ... b)

;        :then (or [y :- t] ... b)

;        :else [y ... b :- e ... b]]])

clojure.core/get-in

; - I have no idea how to assign a type to `m`, even with

;   refinement types.

; (All [m k ...]

;   [m '(k ... k) -> (GetIn m '(k ... k)) :object {:id 0 :path [(GetIn k ... k)]}])

clojure.core/assoc-in

; (All [[m :< (Associative Any Any)] v k ...]

;   [m '(k ... k) v -> (AssocIn m '(k ... k) v)])

clojure.core/split-with

 (All [x y z] 

   [[x -> Any 

     :then [0 :- y], 

     :else [0 :- z]] 

    (Option (Seqable x)) -> '[(ASeq y) (ASeq z)]]

Anyway, happy hacking!

Thanks,

Ambrose

[Johan Gall]

This looks really great!

However a few points concern me.

It would be nice though to have a JIRA triage pass:
- clean up the old entries which are not valid anymore (there are only 62 major entries).
- fix the most egregious bugs (there are only 62 major entries total).

I unfortunately had to drop the use of core.typed in my project at work because of regressions. I hope I can get to try again in a 1-2 months (unchecked typed annotations rot fast...).

I wanted to complain about CHANGELOG.md being stuck at 0.3.0 but you just updated it which is pretty nice!

Anyway, sorry for the grievance, great job!

[Elliot Block]

Thank you for the update!  Very exciting.

If you have time to entertain a higher-level question, I am curious if it
might ever be attractive to have a clearer separation between typed and
untyped parts of a codebase.  In the gradual typing case, there will be many
boundaries between typed and untyped code, both in terms of 1. where a
compiler would need to insert runtime contract checks, 2. where a human will
need to remember to switch code styles from untyped to typed, and vice versa.

I'm curious if it would ever make sense to, instead of having many fine-
grained boundaries between worlds, have a smaller number of coarse boundaries,
e.g. everything in `src-cljt` was strictly typed from the ground up.  Like
with CLJS, CLJT could be a specific dialect with types baked in from the
ground up.  Then, rather than pervasive interaction between typed and untyped
worlds, there would be a smaller number of interactions between one world that
was completely statically typed and the other world that was untyped or
gradually type--although both world would nicely share the same Clojurey
goodness and underpinning (as opposed to for example, shelling out from Clojure
to Scala/ML/Haskell to get these sorts of interactions).

Would a two-worlds constraint such as above possibly make your job easier of
integrating type support, or is it just as hard/easy to implement full gradual
typing?

Thanks for your thoughts / all your hard work.

- Elliot

[Ambrose Bonnaire-Sergeant]

On Fri, Jul 17, 2015 at 1:52 AM, Johan Gall <johan...@gmail.com> wrote:

This looks really great!

However a few points concern me.

It would be nice though to have a JIRA triage pass:
- clean up the old entries which are not valid anymore (there are only 62 major entries).
- fix the most egregious bugs (there are only 62 major entries total).

Yes I will give an hour to this today and see where we're at.

 

I unfortunately had to drop the use of core.typed in my project at work because of regressions. I hope I can get to try again in a 1-2 months (unchecked typed annotations rot fast...).

Which regressions?

[Ambrose Bonnaire-Sergeant]

On Fri, Jul 17, 2015 at 2:27 AM, Elliot Block <elli...@gmail.com> wrote:

Thank you for the update!  Very exciting.

If you have time to entertain a higher-level question, I am curious if it
might ever be attractive to have a clearer separation between typed and
untyped parts of a codebase.

My hunch says no, because it probably means less flexibility in partial porting

of code, and it's unclear what it would buy in return.

 

In the gradual typing case, there will be many
boundaries between typed and untyped code, both in terms of

 

1. where a
compiler would need to insert runtime contract checks,

I believe there would be just as many boundaries. The interesting cases are higher

order, where the boundaries "live on" as --- for example --- higher-order untyped 

functions get passed around in an untyped setting. Also every untyped

interaction is a boundary crossing, reshuffling them into another namespace

will yield the same results.

 

 

2. where a human will
need to remember to switch code styles from untyped to typed, and vice versa.

The proposed system will work like so:

- if your namespace looks like this: (ns my-foo {:core.typed true})

  then it is gradually typed, unless you opt-out with tc-ignore/no-check

- otherwise you are untyped/optionally typed

I'm curious if it would ever make sense to, instead of having many fine-
grained boundaries between worlds, have a smaller number of coarse boundaries,
e.g. everything in `src-cljt` was strictly typed from the ground up.  Like
with CLJS, CLJT could be a specific dialect with types baked in from the
ground up. 

This would have far reaching implications with tooling for little payback. The

fact that core.typed works with .clj and .cljc is one of its selling points.

 

Then, rather than pervasive interaction between typed and untyped
worlds, there would be a smaller number of interactions between one world that
was completely statically typed and the other world that was untyped or
gradually type--although both world would nicely share the same Clojurey
goodness and underpinning (as opposed to for example, shelling out from Clojure
to Scala/ML/Haskell to get these sorts of interactions).

Would a two-worlds constraint such as above possibly make your job easier of
integrating type support, or is it just as hard/easy to implement full gradual
typing?

It would be just as hard, even, as far as I can tell, equivalent.

 

Thanks for your thoughts / all your hard work.

Thanks,

Ambrose 

[Johan Gall]

It was CTYP-197.

Our data access layer uses protocols with multiple arity. It just put a stop right there to our core.typed effort.