Some Typed Clojure types

types.clj

;; Some potential type annotations

; some of this is wishful thinking. Most of it inspired by Typed Racket and Scala

;; Introducing some type constructors

;(U t1 t2 ..) is a union of types

;(Inst Seqable a)  is a type where:
;    (seq this) :- (U nil a)

;(Inst IPersistentCollection o co e f r n)
;   is a type where:
;      (conj this o) :- co
;      (empty this) :- e
;      (first this) :- (U nil f)
;      (rest this) :- r
;      (next this) :- (U nil n)

;(Inst Associative k v r)
; is a type where:
;    (assoc this k v) :- r

;(Inst IPersistentMap k v o do)
; is a type where:
;    (assoc this k v) :- (Inst IPersistentMap k v o do)
;    (dissoc this o) :- do

;; The type annotations

;reference:
; (+T v t) annotates var v with type t
; (Fn ...) is an ordered intersection of arity types (See PADL 2012, Sam TH)
; (Inst c ...) instantiates a polymorphic constructor c with type arguments
; (All [[a :variance v] ...] t)  defines a scope for type variable a, with variance v and optional upper bound with :<

(+T clojure.core/seq
    (All [[a :variance :contravariant]
          [x :variance :invariant]]
      (Fn [(Inst Seqable x) -> (U x Nil)]
          [CharSequence -> (U StringSeq Nil)]
          ;array -> (U ArraySeq Nil)
          [Nil -> Nil]
          [(U Map Iterable) -> (U IteratorSeq Nil)])))

(+T clojure.core/conj
    (All [[x :variance :invariant]   ;object to cons
          [c :variance :invariant]]  ;cons result
      (Fn [(Inst IPersistentCollection x c _ _ _) x & x * -> c]
          [Nil & x * -> (Inst PersistentList x)])))

(+T clojure.core/first
    (All [[f :variance :invariant]]
      (Fn [(Inst IPersistentCollection _ _ _ f _ _) -> (U f Nil)]
          [(Inst Seqable (Inst IPersistentCollection _ _ _ f _ _)) -> (U f Nil)]
          [CharSequence -> (U StringSeq Nil)]
          ;array -> (U Any Nil)
          [Iterable -> (U IteratorSeq Nil)]
          [Nil -> Nil])))

(+T clojure.core/rest
    (All [[r :variance :invariant]]  ;rest
      (Fn [(Inst IPersistentCollection _ _ _ _ r _) -> r]
          [(Inst Seqable (Inst IPersistentCollection _ _ _ _ r _)) -> r]
          [CharSequence -> (U StringSeq PersistentList$EmptyList)]
          [Nil -> PersistentList$EmptyList]
          ;array -> (U ArraySeq PersistentList$EmptyList)
          [(U Map Iterable) -> (U IteratorSeq PersistentList$EmptyList)])))

(+T clojure.core/next
    (All [[n :variance :invariant]]  ;next
      (Fn [(Inst IPersistentCollection _ _ _ _ _ n) -> (U Nil n)]
          [(Inst Seqable (Inst IPersistentCollection _ _ _ _ _ n)) -> (U Nil n)]
          [CharSequence -> (U StringSeq Nil)]
          [Nil -> Nil]
          ;array -> (U ArraySeq Nil)
          [(U Map Iterable) -> (U IteratorSeq Nil)])))

(+T clojure.core/assoc
    (All [[a :variance :invariant] ;key
          [b :variance :invariant] ;value
          [c :variance :invariant]];result
         (Fn [(Inst Associative a b) a b & [a b] * -> c] ;TODO "keyword" rest args
             [Nil a b & [a b] * -> (U (Inst PersistentArrayMap a b)
                                      (Inst PersistentHashMap a b))] ;sufficient return type? seems hacky - Ambrose
             )))

(+T clojure.core/dissoc
    (All [[a :variance :invariant]
          [b :variance :invariant]]
         (Fn [(Inst IPersistentMap _ _ a b) & a -> b]
             [Nil & Any -> Nil])))