Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Loop inference
(ns clojure.core.typed.test.rt-infer.loop
{:lang :core.typed
:core.typed {:features #{:runtime-infer}}}
(:require [clojure.core.typed :as t]))
(defn b [coll]
(loop [c coll
out []]
(if (seq c)
(recur (next c) (conj out (inc (first c))))
out)))
(b [1 2 3 4 5])
; (t/check-ns)
;Type Error (clojure/core/typed/test/rt_infer/loop.clj:6:1) Loop requires more annotations
;in: (loop* [c coll out []] (if (clojure.core/seq c) (recur (clojure.core/next c) (clojure.core/conj out #)) out))
;
;
;ExceptionInfo Type Checker: Found 1 error clojure.core/ex-info (core.clj:4725)
(ns clojure.core.typed.test.rt-infer.loop
{:lang :core.typed
:core.typed {:features #{:runtime-infer}}}
(:require [clojure.core.typed :as t]))
;; Start: Generated by clojure.core.typed - DO NOT EDIT
(declare)
(t/ann b [(t/Vec Long) :-> (t/Vec Long)])
;; End: Generated by clojure.core.typed - DO NOT EDIT
(defn b [coll]
(loop [ ^{::t/ann (t/U nil (t/Coll Long) (t/Vec Long))}
c coll
^{::t/ann (t/Vec Long)}
out []]
(if (seq c)
(recur (next c) (conj out (inc (first c))))
out)))
(b [1 2 3 4 5])
;(check-ns)
;=> :ok
@whilo

This comment has been minimized.

Copy link

whilo commented Feb 17, 2017

You are doing really great work! I hope the Clojure community starts to appreciate static formal validation more, there is no reason LISP has to neglect static typing and validation techniques. I find spec's openness aspect (w.r.t. hash-maps) appealing, but core.typed has that as well, so I am not sure why it is not appreciated more. Do you think the annotations between spec and core.typed can be unified to a certain degree (a bit in the direction what spectrum tries to do)?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.