plans summary

gistfile1.txt

Types in Clojure
================

What is Typed Clojure?
- optional type system Clojure
  - based on Typed Racket "Gradual typing"
    - dynamic checking
    - static checking  <--- 

Why is it built that way?
- Racket vs Clojure
- Local Type Inference
  (ann f [Int -> Int])
  (defn f [n] (inc n))
+ Good error messages (localised, specific)
- annotation burden

Does it work in practice?

Problems
- annotation burden
- namespace often too large, programmers

New vision:
- Typed Clojure from the inception of a Clojure program

design mode
- completely unchecked, just for top-level documentation
- hooks into documentation tools
- generative testings
- does everything that Schema can do

runtime check mode
- use top-level annotations as runtime checks
- insert better runtime checking for core functions with
  known types.
- best effort runtime checking.

success typing mode
- only throw an error if 100% sure something is wrong
- eg. calling a function with wrong arity
- passing a core function obviously the wrong type

runtime inference mode
- instrument code to remember the types
  flowing through them at runtime
- use generative/unit testing to feed example input
- core.typed outputs annotations

compile-time inference mode
- import untyped code to "temporary" dynamic
  type that can travel anywhere
- record all the places the variable goes
  eg. (inc (:a m)), m must be at least '{:a Num}
- also might infer fn parameters
- core.typed outputs annotations

optional type checker mode
- like core.typed today

gradual type checker mode
- imports protected by runtime contracts

dependent typing?

proof?



Typed Clojure is a gradual type system for Clojure that supports common Clojure idioms and offers compile-time and runtime verification to Clojure programmers.

A practical installation of Typed Clojure code was trialled at CircleCI for two years, however the overall experience with the language was negative. They present a post-mortem here.

In this talk, we first present what we learnt as the designers and implementors of Typed Clojure based on practical experiences.

On the positive side, the fundamental theory underlying Typed Clojure has proved successful:

- User reports of Typed Clojure allowing ill-typed code or allowing a type-based runtime error to occur were rare.
- Typed Clojure also supports a majority of the common Clojure idioms, like heterogeneous maps and control flow typing.
- Types in Typed Clojure are expressive and often useful for many documentation tasks.

However, the rest of the experience with Typed Clojure suffers from major problems:

- To maintain static soundness, Typed Clojure requires programmers to annotate libraries they refer to, a costly activity especially as annotations are rarely available. 
- The implementation has crippling performance problems, implicitly reloading transitive dependencies to ensure code-reloading could not break the type system.
- Porting namespaces from Clojure to Typed Clojure is extremely labour intensive, requiring programmers to manually reverse engineer untyped code to assign an appropriate type signature. Even then ..
- Cryptic error messages fail to indicate whether a shortcoming of the type system or the user program is to blame, leaving many users in the dark.
- Typed Clojure cannot integrate into the Clojure compiler, unlike other verification systems like Schema, leading to frustrating annotation redundancies.
- Documentation for core type system features is non-existent.

The narrow goals of Typed Clojure from its inception (“static soundness at all costs”) has proved user-hostile in practice. We discuss new directions of Typed Clojure’s design and implementation that address its shortcomings, working towards a language that provides the agility and, most importantly, fun that you might expect from a Clojure-variant.