<< Back to previous view

[CTYP-107] automatic pre- and post-conditions for unchecked code Created: 19/Feb/14  Updated: 20/Jul/14  Resolved: 27/Feb/14

Status: Closed
Project: core.typed
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Enhancement Priority: Minor
Reporter: Cees van Kemenade Assignee: Ambrose Bonnaire-Sergeant
Resolution: Completed Votes: 0
Labels: None


Currently it is fairly difficult to use core.typed to achieve/ensure production quality code. Often it happens that part of your own code does not pass the core.typed checker. Of course you can add the :no-check to your function, but in that case all type-checking is bypassed for this function and it can inject arbitrary data into the rest of your program (the type-signature is not enforced anymore.

It would be possible to prevent this issue if core.typed offered the opportunity to derive pre- and post-conditions based on the type-signature. This way unchecked code would use run-time checking as a fall-back scenario to prevent unchecked code could inject arbitrary data into the rest of your program (like the schema-library by prismatic, but using the core.typed annotations instead of schemas).
One step beyond would be to:
1. Use dynalint for the unchecked code (if this is possible)
2. Generate wrappers with pre- and post-conditions for external libaries.

Comment by Ambrose Bonnaire-Sergeant [ 19/Feb/14 7:08 AM ]

This is highly desirable. Typed Racket does an excellent job, so it's simple enough to follow their lead.

The biggest issue is actually the time it takes to load the type checker. I don't want to impose this on anyone who isn't generating contracts from types.

I've pondered writing a simpler intermediate AST representation of types that requires no further loading of the type system. It would look very much like the output of tools.analyzer or CLJS analysis. When a global annotation is added, it would be converted to an AST (very cheaply). Converting this AST to a contract would be less robust than using the type manipulating utilities of the full type checker, but the idea is that a type contract might generate incorrectly, but a "check-ns" always tells you after the fact.

It sucks, but some people rely on the zero load-time of core.typed (it's a pretty sweet property too!).

In short, I've thought a lot about this, and it's a glaring missing component in a gradual type system.

Comment by Cees van Kemenade [ 19/Feb/14 1:37 PM ]

I can imagine the dilemma. Core-typed has zero slow-down as all checking is taken off-line. I can image that the launch of the type-system at runtime is a significant overhead. To prevent this overhead the preparations of the type-checking should be brought to compile-time. Your suggestion of generating AST representations does this.

I was considering generation of source-code at compile time to generate ordinary pre- and post-conditions, or to wrap a function symbol with some checks. However, it seemed to be less than trivial to locate where the ann-macro store the type-annotations. I suppose the limited documention on this type of internal.

I guess the manual insertion of clojure pre- and post-conditions on unchecked functionscurrently is the best way out for the time being.

Comment by Ambrose Bonnaire-Sergeant [ 27/Feb/14 8:46 AM ]

Added clojure.core.typed/pred in 0.2.34. This is about as good as it's going to get for now.

Comment by Cees van Kemenade [ 28/Feb/14 2:31 AM ]

Thanks, this is a great tool to implement a postcondition for a function that has a ^:no-check directive. This way you can prevent that unchecked functions insert incorrect data into your process-flow.

Comment by Cees van Kemenade [ 04/Mar/14 2:58 PM ]

When using this I noticed that (core.typed/pred T) returns an internal error when your type is (Seqable X) or your type contains a (Seqable X) somewhere at a nested level.

However, doing the transformation (Seqable X) --> (core.typed/Coll X)
works nicely.

Generated at Fri Feb 24 14:01:54 CST 2017 using JIRA 4.4#649-r158309.