Skip to content

Instantly share code, notes, and snippets.

@frenchy64
Created February 15, 2017 21:20
Show Gist options
  • Save frenchy64/e3dc37f4ae05ab288bcf170406e9b48e to your computer and use it in GitHub Desktop.
Save frenchy64/e3dc37f4ae05ab288bcf170406e9b48e to your computer and use it in GitHub Desktop.
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
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