Clojure Gazette 135: Transients with Core Typed

Transients with Core Typed

Issue 135 - August 03, 2015

Hi!

I was fortunate enough to interview Akhilesh Srikanth who has been working on a Google Summer of Code project. His project is to be able to safely type transients.

Please enjoy the issue!

Rock on!

PS Want to be more attractive? Subscribe !
PPS Want to advertise to smart, talented, attractive Clojure devs ?

Sponsor: Homegrown Labs

Unit tests exercise the individual parts of your system. And acceptance tests make sure the business requirements are met. If you're worried about how much failure in production will cost in your complex, distributed, and unpredictable system, Homegrown Labs can help build your confidence. Homegrown Labs specializes in Simulation Testing, which tests your system as a whole by simulating a realistic workload. Please support the Gazette by visiting Homegrown Labs and signing up to learn more about Simulation Testing at the bottom of the page.

LispCast: How did you get into Clojure?

Akhilesh Srikanth: I've been aiming to become a good polyglot programmer for a while now. I've been experimenting with a bunch of new functional programming languages out there (Scala, Idris and Erlang), and I thought getting better at Clojure was the next step for me. I've been doing Scala for over a year now, I was in fact a GSoC student for Scala last year, and coming from a statically-typed background, I wanted to experiment with the idea of optional typing and develop a better understanding of type systems in the process and working on Typed Clojure, in my opinion, was the logical step forward.

LC: Can you describe your project?

AS: To summarize, Typed Clojure ( core.typed) currently doesn't support type checking for Clojure's transient data structures and its functions (assoc!, conj!, etc). My GSoC project aims to add support to type check these Clojure constructs. Transients in Clojure provide for optimizations in functional data structures by allowing local mutation within code fragments that need to be efficient, resulting in lesser memory allocation and faster execution times. Now because of this property where they behave like mutable collections, we want to ensure that transients aren't used once they are updated (otherwise we could lookup values at different times and get different results). Using a type system to statically guarantee this property is definitely a promising way to tackle this problem. I'm currently working on encoding the type system with the idea of Uniqueness types which solves the above mentioned problem. This involves me doing a lot of Clojure while learning a whole bunch of new ideas regarding type systems, which I thoroughly enjoy. :)

LC: What are the main challenges?

AS: Well, to start off, understanding the behavior of transients and how they integrate into the type system because of the property that they aren't persistent collections was initially tricky. Transients are actually immutable collections which aren't persistent and creating a new version should invalidate the old one, which is where the idea of linear/uniqueness types fits in. Turns out incorporating this idea into core.typed involves a lot of corner cases which are quite tricky to handle, but should hopefully work out at the end.

LC: Typed Clojure is getting some really powerful features. How has it been working inside the type system?

AS: Yes, Typed Clojure has (is getting) some really interesting features.

It had support for generics and higher-kinded types for a while now which provide some powerful abstractions while designing large applications. It also supports occurrence typing, which allows the type system to ascribe precise types to terms based on control flow predicate checks, which I think is really cool.

In terms of future directions, here are some features that Typed Clojure users can expect:

1. Support for gradual typing, which preserves static invariants of well-typed code outside of the compile-time sandbox of the type checker in statically typed languages. To get a better idea of what I'm talking about, do refer to this excellent blog post by Ambrose Bonnaire Sergeant, my mentor for this project.

2. Support for refinement types, which allows users to generate new types that aren't combinations of existing types which satisfy some predicate, which allows for writing more expressive types while writing code.

3. Enhanced support for dependent types, where types are predicated on values. This is a very interesting idea to ensure correctness in code, wherein program properties that we care about can be encoded within types and if those properties of interest are violated, the type system tells us at compile time that we're wrong.

4. Support for uniqueness types (which I'm currently working on), which provides for statically enforced memory management, and provides for safe memory usage without the intervention of a garbage collector.

Apart from this, core.typed has recently got a REPL, which allows for writing typed code within the REPL. I definitely see an interesting road ahead for Typed Clojure!

LC: How can people contribute to your work? Where can they follow its progress?

AS: I've been meaning to write up a few blog posts to help people new to Typed Clojure get started using it and for developers to get started contributing, but for now, I think the core.typed wiki is probably the best place to go to for anyone wishing to get started.

You can follow the project's progress in my fork of core.typed .

LC: How can people follow you online, if they want to?

AS: I'm @spicytango on Twitter, that's probably the best place to follow me.

LC: What does Clojure eat for breakfast?

AS: Interesting...probably a bunch of parentheses mixed with some awesome sauce from Rich Hickey's kitchen!

LC: Thanks for the interview!