[ANN] core.typed 0.5.1 - Improved auto-annotation performance, CircleCI Workflow

[Ambrose Bonnaire-Sergeant]

Hi,

Announcing the release of core.typed 0.5.1.

[org.clojure/core.typed "0.5.1"]

...
; for very recent releases
:repositories {"sonatype-oss-public" "https://oss.sonatype.org/content/groups/public/"}

; for slim jars, follow version string with: :classifier "slim"

I fixed a bug I described here that meant annotations for cljs.compiler couldn't be generated. Now they can, and they're not half bad! The generated types correctly infers the :op AST is recursive. This information is currently lost in the generated specs, because I don't yet know how to handle spec's global registry well in the inference algorithm (and that pretty much destroys any usage of s/keys).

I also generate annotations for a variety of projects on every commit, using CircleCI workflows. For example, see the artifacts here. If you're interested in how the workflow is written, see here.

More details are in the change log.

Thanks,

Ambrose

[Nick Jones]

 Thanks Ambrose.

Keep up the good work, core.typed is still helping me find bugs.

  

[Ambrose Bonnaire-Sergeant]

I'm glad to hear, thanks Nick.

[Jeroen van Dijk]

Hi everyone,

I think I found a specific use case where core.typed could be helpful. I would appreciate any feedback and maybe some points to get started.

At our company we have been working on an internal library to create AWS Cloudformation templates. These are essentially really big blobs of json. In the past we have extracted a Prismatic Schema by scraping the AWS docs. Now there is some more formal (though incomplete) schema and I've created clojure specs for validation. Since validation errors on the AWS side can be minutes away, sometimes even hours (yes, really), this works a lot better than having no validation. However I think the experience could be even better if there would complete type checking. E.g. in Cloudformation it is allowed to refer to some declaration elsewhere (via refs). Without type checking this is where simple validation is just not good enough.

So I'm thinking about generating a type system around these templates. I would like to generate the types from the data of the schema or the data i scraped (I've created an intermediate data layer for this). I would like to be able to extend or correct types in another namespace while gaining experience with the actual constraints (the formal specs and documentation is not complete). 

Does it sound like core.typed is a fit for the described use case? And if so, what would be a good approach here to generate and use these types? Are there examples of a domain specific type system like this?

Any suggestions or comments are appreciated. Thanks in advance.

Kind regards,

Jeroen van Dijk

[Ambrose Bonnaire-Sergeant]

Hi Jeroen,

On Thu, Sep 13, 2018 at 4:55 AM, Jeroen van Dijk <jeroentj...@gmail.com> wrote:

I would like to generate the types from the data of the schema or the data i scraped (I've created an intermediate data layer for this).

How is your intermediate data layer represented? core.typed likes nested keyword maps (they look something like this).

E.g. in Cloudformation it is allowed to refer to some declaration elsewhere (via refs). Without type checking this is where simple validation is just not good enough.

I don't follow. Could you elaborate, perhaps with some pseudocode to give an impression of what you want verified?

  

I would like to be able to extend or correct types in another namespace while gaining experience with the actual constraints (the formal specs and documentation is not complete).

I'm not entirely sure what you mean but top-level types are collected at runtime, so checking, tweaking types, then rechecking

in the same REPL session is supported.

 

Are there examples of a domain specific type system like this?

Spec-tacular comes to mind. It generates core.typed annotations from high-level specifications.

Thanks,

Ambrose

[Jeroen van Dijk]

Hi Ambrose,

Thank you for your quick and useful response. I realise that I'm only half way in understanding my actual problem.

How is your intermediate data layer represented? core.typed likes nested keyword maps (they look something like this).

The intermediate layer is basically a cleaned up edn version of this data. I'm mostly using it as a way to debug before I convert it to end goal (so far that has been clojure.spec). But the data that we want to produce (a cloudformation template) consists of nested keyword maps mostly. 

I don't follow. Could you elaborate, perhaps with some pseudocode to give an impression of what you want verified?

So a simplified Cloudformation template looks something like this:

{:MyEC2Instance {:Type "AWS::EC2::Instance"

                 :Properties {:VpcId "vpc-id-here"}}}

This is very basic and probably best validated with clojure.spec. Especially with expound you can get really helpful error messages.

However it get's more complicated when you want to use Cloudformation references to resources declared elsewhere in the template. This is definitely something you want when you make something serious:

{:MyVPC {:Type "AWS::EC2::VPC"

         :Properties {:Subnet "..."}}

 :MyEC2Instance {:Type "AWS::EC2::Instance"

                 :Properties {:VpcId {:Ref :MyVPC}}}}

The best thing we can do with clojure.spec is saying that :VpcId can be a string or a Ref map. Ideally my validator would know that we expect a VpcId here which is either a string or a reference to a Cloudformation definition of type "AWS::EC2::VPC". This requires keeping track of references and knowing what type they have.

I'm not entirely sure what you mean but top-level types are collected at runtime, so checking, tweaking types, then rechecking

in the same REPL session is supported.

What I mean here is that with clojure.spec I can redefine a spec at runtime any level when I see my generated version wasn't precise. I think this is the same as what you are saying.

Spec-tacular comes to mind. It generates core.typed annotations from high-level specifications.

Great! I'll have a look and learn :)

Thank you so much.

Jeroen

 

Thanks,

Ambrose