core.typed

automatic pre- and post-conditions for unchecked code

Details

  • Type: Enhancement Enhancement
  • Status: Closed Closed
  • Priority: Minor Minor
  • Resolution: Completed
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • Labels:
    None

Description

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.

Activity

Hide
Cees van Kemenade added a comment -

Note:
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.

Show
Cees van Kemenade added a comment - Note: 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.
Hide
Cees van Kemenade added a comment -

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.
Cool!

Show
Cees van Kemenade added a comment - 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. Cool!
Hide
Ambrose Bonnaire-Sergeant added a comment -

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

Show
Ambrose Bonnaire-Sergeant added a comment - Added clojure.core.typed/pred in 0.2.34. This is about as good as it's going to get for now.
Hide
Cees van Kemenade added a comment -

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.

Show
Cees van Kemenade added a comment - 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.
Hide
Ambrose Bonnaire-Sergeant added a comment -

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.

Show
Ambrose Bonnaire-Sergeant added a comment - 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.

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved: