we could use `:repeat` key and `<*` syntax in Typed Clojure to do useful annotation

mileston.clj

; It's been a long time that Typed Clojure couldn't annotate `hash-map` using
; first class type. Because these functions require even number of arguments,
; and also have some special type constrain on its arguments.
; So we used to check these functions using special handler in checker.
; One of my GSOC goal is to make it possible to type check these kind of
; function without special handler.
; And now I made it. Thanks Sam Tobin-Hochstadt and Asumu Takikawa who inspired
; us.
; You can try it at my fork of Typed Clojure
; https://github.com/xudifsd/core.typed/tree/repeat-support

; I'll introduce some of my contribution here.
; If you're new to Typed Clojure, please read user guide first
; https://github.com/clojure/core.typed/wiki/User-Guide

user=> (require '[clojure.core.typed :as t])

; we already have HeterogeneousVector, HeterogeneousSeq and HSequential in
; Typed Clojure
user=> (t/cf '[1 "a" \c] (HVec [(Value 1) (Value "a") (Value \c)]))
[(HVec [(Value 1) (Value "a") (Value \c)]) {:then tt, :else ff}]

user=> (t/cf '(1 "a" \c) (HSeq [(Value 1) (Value "a") (Value \c)]))
[(List* (Value 1) (Value "a") (Value \c)) {:then tt, :else ff}]

; but vector is not HeterogeneousSeq, and list is not vector,
; so following code will get type error
; user=> (t/cf '[1 "a" \c] (HSeq [(Value 1) (Value "a") (Value \c)]))
; user=> (t/cf '(1 "a" \c) (HVec [(Value 1) (Value "a") (Value \c)]))

; HSequential represent Heterogeneous Sequential, so it can accept both list and
; vector
user=> (t/cf '[1 "a" \c] (HSequential [(Value 1) (Value "a") (Value \c)]))
[(HVec [(Value 1) (Value "a") (Value \c)]) {:then tt, :else ff}]
user=> (t/cf '(1 "a" \c) (HSequential [(Value 1) (Value "a") (Value \c)]))
[(List* (Value 1) (Value "a") (Value \c)) {:then tt, :else ff}]

; My contribution begins
; we can't use Heterogeneous things to catch repeated pattern, unless we have
; `:repeat true` as its attribute. I'll use HSequential as example, but it can
; also applies to HeterogeneousVector and HeterogeneousSeq
user=> (t/cf '[1 "a" 1 "a"] (HSequential [Number String] :repeat true))
[(HVec [(Value 1) (Value "a") (Value 1) (Value "a")]) {:then tt, :else ff}]

; it'll fail if it misses some repeated pattern, so following code will get
; type error
; user=> (t/cf '[1 "a" 1 "a" 1] (HSequential [Number String] :repeat true))

; but `:repeat true` is not very useful alone, so we add `<*` syntax in
; function type. What this syntax means is to wrap rest arguments into a
; vector and then type check it with its previous type. Note, currently we
; assume that type is one of HeterogeneousVector, HeterogeneousSeq and
; HSequential. It's better to use HSequential, because it's more general.
; So we annotate `hash-map` as
; (All [x y]
;   [(HSequential [x y] :repeat true) <* -> (Map x y)])
; https://github.com/xudifsd/core.typed/blob/repeat-support/src/main/clojure/clojure/core/typed/base_env.clj#L851

; And now we can type check `hash-map` purely on first class type, instead of
; special handler.
user=> (t/cf (hash-map 1 "a" 2 "b" 3 "c"))
(t/Map (U (Value 3) (Value 2) (Value 1)) (U (Value "c") (Value "b") (Value "a")))
user=> (t/cf (map (t/inst hash-map Number String) [1 2 3] ["a" "b" "c"]))
(t/NonEmptySeq (IPersistentMap java.lang.Number java.lang.String))
user=> (t/cf (map (t/inst hash-map Number String) [1 2] ["a" "b"] [4 5] ["d" "e"]))
(t/NonEmptySeq (IPersistentMap java.lang.Number java.lang.String))

; and will fail on type error
; user=> (t/cf (map (t/inst hash-map Number String) [1 2 3] ["a" "b" "c"] [4 5 6]))
; and
; user=> (t/cf (map (t/inst hash-map Number String) [1 2] ["a" "b"] [4 5] [\a \b]))
; this also applies to `assoc`, but I haven't added it yet.

; I'll implement `<...` syntax in function to support more accurate type check
; in `hash-map` and `assoc`, stay tuned to
; https://github.com/xudifsd/core.typed/commits/repeat-support
; for more information.

; HTH
; Di Xu