untyped-vars and form checking (clojure.core.typed/cf)

[Jeroen van Dijk]

Hi all,

I have been playing a bit with core.typed to see what I could do with it and so far I'm pleasantly surprised by its power. 

Now I have a special use case in mind where I want to type check one function at a time without needing to include the body of the functions it relies on. I want to tell the type checker that these dependencies have been checked already and are ok. I have managed to get this working with `clojure.core.typed/check-ns` on namespace level, but this is too cumbersome for what I have in mind. To get this working inline I have only found `clojure.core.typed/cf` so far, but I haven't found a way to use untyped-vars here.

I would like to do something like this and have it pass type checking:

	(t/cf
	(let [a (fn [x] x)
	_ (t/ann ^:no-check a [Number -> Number])
	b (fn [x] (a 1))
	_ (t/ann-form b [Number -> Number])]
	(b 1)))

(https://gist.github.com/jeroenvandijk/e8192dfda79aceeb557f#file-desired_code-clj)

I'm not interested in all the extras that check-ns offers in this case (profiling, logging and such), I just want a success signal or some error information. Is this already possible?

Thanks,

Jeroen

[Ambrose Bonnaire-Sergeant]

Hi Jeroen,

Glad you're enjoying core.typed.

Try this idiom: (t/cast [Num :-> Num] (t/tc-ignore (fn [x] x)))

Turns out I'm also experimenting with inferring b's type based on its usage, not its definition. Here's how it works for vars. https://www.youtube.com/watch?v=zcxOWE7MuOY

That hasn't hit master branch yet, but is that something that would help here? Static safety is forfeited to infer annotations.

Thanks,

Ambrose

[Jeroen van Dijk]

Hi Ambrose,

Thanks, your suggestion does what I wanted! This is the resulting code:

(t/cf      

  (let [a (t/cast [Number :-> Number] (fn [x] x))

         b (fn [x] (a 1))

         _ (t/ann-form b  [Number -> Number])]

    (b 1)))

I think the inference feature is a great one, but that's not why I'm doing this. I have something else in mind. I want to create an incremental workflow where tests and type checks only run when you change a definition. I think the recent criticism of CircleCi towards core.typed is not specific against core.typed. When your code base grows everything gets slower. Midje and others have some hacks that try to infer what tests to run, but that never works perfectly. Often when running autotest, you have to wait for a minute (or more) for your tests to finish just because you made a tiny change in a function. I foresee the same problem with core.typed, when you focus on file/namespace level, no matter how fast the compiler gets, it will always get slower when the code base grows. I'm sure this is not a problem for most (smaller) projects.

So the idea of the above code is that you mock/cast the types of all dependent functions and only focus on the given body. This of course only works reliably when the dependent functions are always typed checked and these types are communicated to the incremental checker/tester/runner (no name for it yet).

Anyway maybe that was too much info, thanks for your suggestion!

Cheers,

Jeroen

Op woensdag 25 november 2015 16:15:16 UTC+1 schreef Ambrose Bonnaire-Sergeant:

[Ambrose Bonnaire-Sergeant]

That's a really cool idea!

Can you elaborate what heuristics midje uses? Could this be built into core.typed?

Thanks,

Ambrose

[Jeroen van Dijk]

I think how midje does it is described here https://github.com/marick/Midje/wiki/Autotest From a user perspective, it will re-run particular tests when an (indirect) namespace dependency has been changed. I think it uses clojure.tools.namespace for this. The downside is that it sometimes it runs too much, e.g when you make a change in a core file of your project, or too little, e.g. when you make a change in Record definition. For example, the latter happens when you use Stuart Sierra's Component. Your application code will require the protocol namespaces, but not the implementation one. So these dependencies are not found, and if so often in the wrong order causing protocol mismatches. I tend to "solve" this by evaluating my code via Cider and re-running the test file manually.

I'm guessing that the above could be useful for core.typed, but is really a heuristic and not a particular reliable one (as in the example of Component usage). So if you would do this for type checking you would possible find out type errors in a very late stage, i.e. when running the full type check on the project. But I guess it is better than not running the type checks at all because it takes too long.

Does have core.typed have something like autotest?

Thanks,

Jeroen