frenchy64

;https://github.com/JoeOsborn/gamalyzer/blob/3dbbb927308004ca056980fe4e743b59e7221870/metric/src/gamalyzer/data/range.clj#L5
(ann ^:no-check multiset.core/multiset (All [a] [a -> (clojure.lang.IPersistentSet a)]))

;https://github.com/simon-nicholls/pizzure/blob/a6fda5cbe533c231230af2853721af265cee9f4c/src/pizzure/types.clj#L33-L35
(ann ^:no-check korma.core/exec (All [[a :< EntityValue]] [Query -> (Seq a)]))
(ann ^:no-check korma.core/transform
     (All [[a :< EntityValue]] [Entity [a -> a] -> Entity]))

frenchy64

(ns typed
  {:core.typed true
   :import-untyped
    {u/a String}}
  (:require [clojure.core.typed :as t]
            [untyped :as u]))

(ann f [-> String])
(defn f []
  (.toUpperCase u/a))

frenchy64

(ns untyped)

(def id identity)

(ns typed
  {:core.typed
    {:untyped-imports
      {u/id (All* [a] [a -> a])}}}
  (:require [untyped :as u]
            [clojure.core.typed :as t]))

frenchy64

Polymorphic contracts

(ns utyped1)

(defn id identity)

frenchy64

Contracts in Clojure

Developing a gradual typing system for Clojure requires a rich contracts library. Some libraries already exist like Schema and core.contracts. These do not provide more advanced contracts like polymorphic function contracts or dependent contracts. This article explores the possibilities in implementing polymorphic function contracts in Clojure.

Racket's contract library has the concept of Opaque values which can be effectively locked with a key. This is a problem when directing control flow, because the only difference we want from adding contracts is more errors and there is potential to change return values. For example

(defn minc [n]
  (if (number? n)
 (inc n)

frenchy64

Practical Considerations of Intercepting Clojure evaluation

One important extension that Gradually Typed Clojure will require is hooking into the standard Clojure evaluation process. There are at least two motivations for this:

1. As discussed in previous articles, it is often necessary to insert extra checks in code depending on how it is used.
2. Typed Clojure can uncover type-based optimisations, such as identifying a missing type hint, and we want to automatically apply this.

The existing prototype has been a useful experiment which has revealed some of the subtleties of Clojure evaluation.

The basic approach is to use nREPL middleware to type check REPL interactions.

frenchy64

Towards Gradual typing for Clojure

Abstract

Typed Clojure is an optional type system for Clojure, implemented as an external compiler pass manually triggered by the programmer. This way, Typed Clojure is rather limited, being unable to interact with the normal compilation process despite being able to infer program optimisations. The goal of "gradual typing" also address the issue of interlanguage communication. Currently, any code that is not checked by the type checker is assigned a trusted type by the programmer. This effectively means whenever a Typed Clojure program calls normal Clojure or vice-versa, there is an opportunity to break static invariants assumed by the type checker.

There are several challenges to address to design a satisfying gradual type system for Clojure. Datatypes in Clojure are implemented as public, final and effectively immutable Java classes. The classic approach of proxying is not as useful fields are immutable, so contracts can be implemented as either flat checks or clo

frenchy64

Defining and using Vars in Typed and Untyped Lands with Gradual Typing

One of the key aspects of gradual typing is that the same code can execute in two different contexts with different kinds of contracts. For example take the following code:

(ns my-typed
  {:lang :core.typed})

(ann my-plus [Num Num -> Num])
(defn my-plus [a b] (+ a b))

frenchy64

Unbound Vars and Gradual Typing

Vars are one of the most beloved features of Clojure, whether users know it or not. Vars are global top-level variables in Clojure, implemented as unmanaged references (with respect to Clojure's STM implementation).

(def a 1)

The previous expression defines a new var a and assigns 1 as its root binding. To access the current value inside a var, you need just to name the var.

frenchy64

Ill-typed Typed Clojure code should be evaluated and enforced at Runtime

A longstanding issue with Typed Clojure has been its lack of integration with the rest of Clojure's compilation process. This means type-based optimisations simply get left on the floor because there is no way to integrate them.

Actually addressing this raises an interesting question: should type-checking evaluate a form once it is determined to be ill-typed? Intuitively the answer is no: we throw away any static guarantees we were trying to enforce in the first place. But gradual typing is more flexible in when static guarantees are enforced, and introduces some flexibility.

For example, typed code can be verified to satisfy static invariants so no runtime properties are inserted to preserve them. However, if some code cannot be statically checked to adhere to a type, gradual typing says we can enforce this type at runtime via contracts. This is common in cross-language interaction; if typed code calls untyped code, the untyped