Tip:
Highlight text to annotate it
X
I think we can make a start.
I'm Ambrose, I'm from UWA
(University of Western Australia), actually a student.
I'm about to graduate with a
Bachelors degree in Computer Science, and my subject for my dissertation
was creating core.typed, aka. Typed Clojure
last year, but recently it's been accepted into Clojure contrib
last year, but recently it's been accepted into Clojure contrib,
as you can see from the Leiningen dependency.
If you want to follow along, and you're lucky enough to have internet, chuck this into your lein
This workshop's kind of about me (laughs).
You're gonna have to check out what I'm going to do.
Ok, a bit of background on core.typed,
if you didn't see the talk yesterday, so core.typed is an optional type checker
for Clojure, it's a particular kind of type checker called a gradual type checker,
and it's ancestry is
Typed Racket, which is gradual typing for Racket, and gradual typing
basically means that we've got typed and untyped code in the same program
and gradual typing can also accomodate some
ways, different ways, of ensuring interactions
between untyped and typed code are still sound at runtime.
So, core.typed implements the static checking
and has no runtime checking.
So, yea, it might have been developed for academic,
in an academic environment, but it's definitely intended for use.
Typed Racket is definitely practical and I've
copied all of Typed Racket and made it a bit more Clojurey
and I think it (core.typed) is getting there. It's not quite production ready, but
I'm not sure if the Google Summer of Code Projects
for Clojure have been announced yet, but I have submitted one
for core.typed, to improve documentation and basically get it up to
the point where I will say with a straight face that I'll recommend
it for production.
So this particular workshop, I hope you've had some Clojure experience
I won't exactly be explaining much
of the Clojure semantics. I won't
expect that you've even heard of core.typed
except maybe if you came yesterday. I think that's the case with most people.
Probably the case if they've heard of core.typed, it sounds cool, but they haven't tried it.
And this is one of the first
And this is one of the first
kind of extended
talks on core.typed. I really would love some feedback.
Please tell me everything sucks,
and I'll improve it.
This workshop's going to be me in vim the whole time
so what we're going to do, we're going to check out the type syntax
and how the typing scope works, and some of the special types
in core.typed, and how it integrates with Java.
Clojure runs on the JVM, so it has the same
at runtime we have classes and references
and these sorts of things. How does that look?
Rainbow parens probably not a good idea...
So the first
thing is kind of weird,
because in this workshop we're basically emulating a REPL environment, when really
the way you use core.typed, you get your full namespaces
of code and you add annotations inside it, and then you run
a top level function, called check-ns.
check-ns takes a symbol which is the namespace you want to check, or if you
give a namespace, it checks the current namespace.
You could imagine, you're working in a REPL
adding stuff to the namespace, and you can call check-ns
and it will give you type checking when you need it, in your REPL.
So it integrates quite well with REPL development.
Why this particular file is kinda weird, it's
not actually typed code, we're using a
macro call cf, which stands for check-form.
Basically what it does, here's an example (cf 1 Number), takes a form and
optionally a static type, and it blows up
if the form is not of that type. If it is of that type
it just prints the type.
it just prints the type. It's kind of a debugging/exploratory
way of working with core.typed.
So a bit of Clojure semantics, Clojure, when you write 1 or 1.1
or a number literal like that, you get Longs and Doubles
and core.typed understands this. So if we try and say
"check that 1 is a java.lang.Integer"
we get a whole bunch of redundant type error that I will fix :)
Usually when you get more than one type error
just in general in any language you usually want
the first error. There are research languages which actually just, for students
the first error. There are research languages which actually just, for students
who are learning programming, to just show the first error.
Quite useful. Anyway, ignore this (the bottom two errors).
Sorry, when you use cf here, you lose
the line number. We definitely get good line numbers when
we use check-ns.
We can see we're expecting a type of Integer, and we get a value of 1.
And that is a type error. We say, we want a
Long, and it (outputs) down here (bottom left of screen).
So it's saying, that's a Long, that's fine.
So the way the scoping works with types is that it reuses the way Clojure
globally scopes. Classes and vars
globally scopes. Classes and vars, things like that,
well, that's basically it really,
and you can see I've got an :import statement here (top), and what the :import statement does
is, if I type Seqable in my namespace, it now refers to clojure.lang.Seqable.
is, if I type Seqable in my namespace, it now refers to clojure.lang.Seqable.
So, every Clojure namespace comes
by default with the equivalent of import java.lang.*;
in Java. So all the java.lang
Classes are in scope there, so this is actually
java.lang.Long.
java.lang.Long.
You saw, it outputted "Long", but that's just because
core.typed prints types in the prettiest way we can print in the current namespace.
So, Clojure itself is implemented
in Java using interfaces, abstract classes,
it's just normal Java stuff, it's not
implemented with protocols. Basically, what I've done, I've
taken the classes
(if I can get a look back at the imports)
these are the kinds of things I'm talking about. So this is a Seqable interface
for things that
you can create immutable sequences from.
So, because it's immutable we can
parameterise Seqable by
one parameter, which is covariant. That basically means that
we can say that a vector [ 1 2 ] is
a (Seqable Number), even though it's also a (Seqable Long).
That's because [ 1 2 ]
the vector is immutable, no sorry
it's because the seqable that will be emitted is immutable.
We also look up the type environment
we use (I think I've got a call somewhere)
... to get a bit of perspective on the
type hierarchy in Clojure,
we've got an interface called
clojure.lang.IPersistentVector, and Clojure actually extends
IPersistentVector, and it implements these things (bottom of screen)
You can see it implements clojure.lang.Seqable.
Actually at runtime IPersistentVector is a clojure.lang.Seqable.
This is kind of like Java generics in that we have some extra "generics" on top that don't affect runtime or anything like that.
This is kind of like Java generics in that we have some extra "generics" on top that don't affect runtime or anything like that.
This is kind of like Java generics in that we have some extra "generics" on top that don't affect runtime or anything like that.
I don't actually attempt to
support Java Generics in core.typed, otherwise I probably would have got nothing done.
Just staring at a screen all year, doing nothing.
So, here's a list, we know that's a (Seqable Number)
and that's ok. And of course
this is where, remember, up the top, the types are in scope because of our imports,
this is where, remember, up the top, the types are in scope because of our imports,
Just normal Clojure stuff. core.typed reuses a lot of Clojure concepts.
We have our set syntax,
that's an IPersistentSet.
We've got Symbols, Keywords and Strings, kind of similar concepts,
but they're not parameterised
they're just normal Classes. String here is
java.lang.String, remember,
and we have clojure.lang.Symbol, and clojure.lang.Keyword.
Actually, Typed Clojure can also support
a type called a "singleton type". This is basically a type that only has one member.
So, a singleton type could just contain a single Symbol 'a.
We can say, "check the form
'a" and core.typed will say
it's a Value type, that's the Symbol 'a.
This is not anything sophisticated, it just gives you something more in your types.
A note on the syntax,
there can be multiple kinds of type information that come from an expression (see bottom left),
and some of it has to do with its runtime type, the (Value a), and this one in particular
is to do with a form's truthiness, the {:true tt, :false ff}.
This map here will tell me what will happen if
I pass this value to the conditional
position of an if statement. This basically says, "If I pass this value
'a to the test position of an if statement, like (if 'a .. ...), then
I will always go down the :then branch (tt), and I'll never go down the :else branch (ff).
This conforms with Clojure's idea of truthiness.
In Clojure only false and nil are false values.
We've seen this before.
So something with a bit more
interesting type is
an atom. An atom is a mutable
value in Clojure,
and kind of as an experiment, I've
split all mutable types to have
two type parameters. Usually you have
(if you're doing this in Scala or Java say)
you have one parameter which is
invariant. Instead of having one parameter that is invariant, I've split it
into two parameter. One is contravariant,
(the other is covariant), they both go in opposite directions.
Basically, (Atom w r) says "this atom can read types w,
and it can write types r".
The way it's setup there is
basically equivalent to have a single invariant parameter.
But of course, the most common case you want to use it
is as if it had a single invariant parameter. We don't really care what the difference is
between what we want to write and read with atoms.
So, core.typed supports type aliases,
and we have a type alias here (t/Atom1 m),
where t/ is a normal namespace alias
of clojure.core.typed (see top right ":as t")
So t/Atom1 is actually a var, so this will resolve
just like a normal var (here it's aliased).
In any case,
(Atom1 m) is the same as (Atom m m)
More concretely (that's a bogus example),
but we can say that
this (atom 1) atom here, treat it as if it's an atom
that can both read and write Numbers, and that's basically the
most common way you'd want to use Atom.
The reason I've split it out into two parameters, core.typed comes
with a, well it's not really experimental
but I haven't really seen it used in other serious languages,
but I try and provide a solution to
array covariance in Java.
It comes down to:
if you're getting an array
from Java, you don't know anything about
it just from it's type, and that's because of array covariance.
Basically, what we know is, the gist of it is
if I get an array from Java, it's not safe to write to it.
This kind of type (splitting of parameters) can
express that. So basically when you get an array that you don't want to write to
it's an (Array Nothing m), you can write Nothing to it.
(for some component type m).
That also means that we can write a function
that can abstract over
...this is probably easier to write.
Actually, I have an example somewhere.
So we have this `sum` function here,
which kind of looks like the kind of function (signature) you'd write in Java.
You say, ok, this function works on all Number[]
but in this case (core.typed), it's statically sound
because we're saying, in the body of `sum`, we cannot write to the array.
That's happening up here,
this is the array constructor
that has both read and write parameters.
(see line 5). my-integer-array can both read and write Integers.
We can pass it to sum (line 21), even though
the parameter type of `sum` is not an array type that can both read and write Integers,
we can still pass my-integer-array, because it's an (Array Integer). (Here (ReadOnlyArray Integer) expands to (Array2 Nothing Integer))
It's kind of technical.
I've taken that concept and applied it to everything that's mutable.
(in Typed Clojure). Just as an experiment.
As long as we have
type aliases, it seems to work pretty well.
We have the `seq` function, something interesting here,
the seq function only returns nil
if it's passed
a non-empty sequence. core.typed knows this
invariant. So this check will pass because, core.typed knows [1 2] is a non-empty sequence,
so we can assign this the type (ISeq Number). In core.type we strictly separate
nil from everything.
This is kind of a smart thing to know this is going to be an (ISeq Number)
and is basically saying "this expression can never be nil".
Functions right now are kind of a corner/special case.
There is a function (class) and a function interface (IFn) in
Clojure, but I'm not using it right now.
I've inherited some cruft from Typed Racket.
There are a couple of ways
to write functions. We can give the untyped version
(line 74), a function that takes an `a` and adds one to it,
but to annotate the parameters of that function
we change fn to fn> (line 75)
(fn> is clojure.core.typed/fn>)
and we can annotate
the parameter types.
Generalising the syntax, if we have more than one
parameter, we can go like that.
etc.
So the return type there (line 75) is inferred.
If we want to
have more expressive function types, instead of just giving
parameter types, we can also use
`cf`. I should probably clarify something.
There's a way to annotate a form with an expected type.
for an expression in core.typed.
And it's basically like this.
This particular form #(+ 1 %) is equivalent to (fn [a] (+ 1 %))
This anonymous function only line 76 is the same as line the function on 75.
We use ann-form/cf to annotate the anonymous function syntax.
(we give the full function type).
The way to read [Number -> Number], we have a parameter types
to the left of the ->, and the return type to the right of the arrow.
And sometimes there's some extra stuff on the right of the
return type.
Q: Is the return type of line 75 inferred?
A: Yes, that's figured out because
basically the way local type inference works is kind of top-down,
and we come from (fn> [a :- Number] ...), gather the type of `a`,
and we don't need to backtrack to find any
, to infer any more complicated types. We already know the type of +,
we know the type of 1, and `a`, so
we can infer the result type here.
The return type inferred in line 75 is the same as given in line 76.
Q: How do we know the type of +?
A: I have a set of base annotations for the clojure.core library.
+ is kind of interesting, because it inlines to a call to clojure.lang.Numbers/add
which is an internal method of the Clojure compiler.
I know about the inlinings as well (through annotations).
These base annotations are unchecked.
We are trusting clojure.core code
and I've done my best to model the invariants in the types.
It would be pretty inefficient to type check all of clojure.core each run, which is a
pretty basic strategy of type systems of this nature at least.
So we can get a bit more elaborate with our
argument types. We can say
(express) a function that takes any number of numbers,
and we just use the regular-expression-like * syntax
The type to the left of the star can appear 0 or more times.
This function takes any number of numbers and returns a number.
Q: Why doesn't (Number * -> Number) work?
A: Use vectors for function syntax: [Number * -> Number]
This is pretty cool, this is something I added recently.
We support keyword arguments and all the nuances
of destructuring. I think core.typed supports
all destructuring types.
Line 89, we use & to
Line 89, we use &
express keyword arguments.
Then you
put a hash-map after &, and this is a map of optional kw parameters.
(that we might want to pass to the function).
Line 89 says, the `a`s on line 87
could be nil, could be Number.
You don't necessarily need to supply them.
If I was calling that function, let's call it f,
this is a valid way of calling it.
If I wanted to say, all these keyword arguments were mandatory
(I've got another version here)
and this syntax may change it's
a bit ugly. We're saying we have no optional kw parameters {}
but we have 3 mandatory ones (:a, :b, :c).
We have to supply numbers for these three keyword arguments.
These destructuring calls
just work.
We also have dotted types
which I might get to later.
A very important aspect of Clojure
is the ability to use heterogeneous maps as
kind of ad-hoc objects, without having to declare things
in advance. This is pretty important to support from core.typed.
We have a heterogeneous map type.
In this context, a HMap is basically a map
with a set of known entries with keyword keys;
HMap knows which keywords (are) in the map, and also knows
which keyword entries *can't* be in the map.
These two pieces of information are useful in different contexts.
We can show the types here.
If we type check the empty hash-map {}
we get (CompleteHMap {}). This is just a
(I'm not sure if there's a way to express this directly in the types), this is basically saying
that "this is a complete hash-map" in that
all the keys that are present in the {} in (CompleteHMap {}), they are comprehensive.
There are no other entries. Next example.
So now we know it's a complete hmap
that doesn't have any keys except an
:a to a (Value 1).
Actually, '{:a Number} is sugar for (HMap :mandatory {:a Number}).
We should start here.
We have the HMap constructor that accepts :mandatory or/and :optional
keyword entries
... I'm being ambiguous about what I mean as keyword parameters...
Notice the similarity of HMap syntax and the keyword parameters.
Remember optional kw args come first, then :mandatory.
We can express this in the HMap constructor
and say, we expect this form
to be a HMap that has an :a entry
that maps to a Number,
and you can see (bottom left), it's inferred to be a PartialHMap,
basically means we don't know if the entries are comprehensive (there could be more).
There could be extra entries.
Q: You know about both the present and absent entries?
A: Yes, knowing both kinds of information means
core.typed knows that this expression will return nil.
Let's cross our fingers and try it.
Yes. (Bottom left)
So, if I annotate a less precise type,
to forget the knowledge of the absence of keys,
let's say we only know
that there's a mandatory :a with Number,
now we get back a less precise type (bottom left) Any.
I don't seem to stop for questions very well
please, just shout out (laughs).
I get a bit excited, sorry.
We have some basic support for assoc
, we can assoc on
to maps, and we also remember whether a HMap is complete.
Because {} is complete, we add a :b (!)
key, we also get a complete map back.
(that just has a :b entry).
We can also understand Clojure's trick of threading through a path of keywords
You can see here, this map has a path from :a to :b to :c.
core.typed can follow that (outputs (Value prize))
Similar kind of story for heterogenous vectors
we've got another
type syntax (a vector) with a preceeding quote
The quotes that are not
before square braces (line 123), they are sugar for singleton types.
'1 is the same as (Value 1).
You can see ... so many vectors! (bottom left). The type starts here (skip the first square brace)
so we have a heterogeneous vector (!), which has been inferred from line 122,
which has 3 entries
with these three Values.
We can call nth on the HVector .. "get on vector NYI" .. oh yeah ..
There's a little note saying that `get` on a vector is not implemented yet.
(laughs)
Basically `get` doesn't work the way it should. (It's less precise at the moment).
I've hardcoded cases for HMap with `get`.
As you can see, the (Value :cheese) is inferred as the 3rd element of the vector.
Here's something new coming from
Scala or Java, a general union
of types. And it comes pretty useful in Clojure
because it turns out, this is kind of how we think about Cloure code.
We start off with a pretty general type, and use type predicates to
refine it, and we (mentally) know maybe at this point in our branch
the binding is of a particular type, but maybe if we went a different branch, it's of a different type.
We don't necessarily always have to create new
bindings, we might just work with a binding `a`,
and we might want to use the same `a` all the way through our conditional.
We want to learn better types for that `a`
In this particular example,
we can see that it's valid to
give the symbol 'a
the type a union of nil, Symbol and Keyword.
We've assigned a slightly (more!) general type.
I'll go over unions later.
We have intersections, I don't think it's a good idea
to show, because they may go away very soon.
There's little tricks where core.typed knows whether
a sequence
is empty or not.
It's an idiom of Clojure
to call `seq` on a
seqable, right, and the result is either going to be nil,
or a non-empty sequence.
If we go down this branch (line 140), `my-seq` is not nil.
Imagine if `my-seq` had a union type
of nil and a non-empty sequence. Is it nil? No. So it's a non-empty sequence.
So if we call (first my-seq) down this branch, we're always getting back a number.
The actual refining of the type
only matters down the then branch, because we don't use any type information in the else branch.
We just return 0. The gist of that is we can say "This expression must return a Number",
and the checker has inferred that.
my-seq here is a union of nil and a non-empty sequence.
(of numbers).
The interesting bit is line 140.
How do we know that my-seq is non-empty?
.. and not nil.
This an example of expressing Clojure idioms with occurrence typing, coming up soon.
Q: What if you put something other than a number in the else branch, is that union result?
A: Yes, so we'll either get 1,2 or 3 back. (Actually the else branch is inferred as unreachable here
so 'a doesn't contribute to the type). This isn't as impressive as it might look, it's a bit dumb.
Because my-seq's component type ends up being (U '1 '2 '3)
We could be a bit cleaner here
with type generalisation. (Probably better to generalise to Long or Number here).
So Typed Clojure also supports polymorphism
Java has f-bounded polymophism, that basically means
that we can have type variables
with lower/upper bound, and also recursive bounds,
bounds that refer to the original type variable being bounded.
Turns out that lower/upper bounds aren't quite as useful I though they'd be,
I can't pinpoint the exact reason but
because we have unions and intersections,
these bounds aren't as important as a language like Scala,
where lower bounds are very useful.
.. lower bounds are not very useful in core.typed, we'll skip it.
Here is the identity function.
We have our type variable binder All,
it takes a number of type variables
and a type, and scopes the variables in the type as you would expect.
So that's just a simple indentity function.
We have type aliases,
here's a simple one.
Let MyInteger (line 152) be an abbreviation of (U Long Integer).
That's simple. If we want parameterised aliases,
we use a type function: a function on the type level.
So it takes a type and returns a type.
Well, really takes a number of types.
This type function takes a type `x`,
and we declare it's variance as covariant,
and the return type is (IPersistent x). The variance annotation there, basically means
that a
(ListOf Integer) is a subtype of (ListOf Number)
It's a bit funny to have to wrap this in `cf`,
but core.typed is pretty strict, it has a phase
that just collects types. Whenever you have global annotations/aliases,
you have to pass it to the type checker somehow. It's not enough to just eval it.
Even I forget this sometimes.
Q: You wouldn't normally use cf right?
A: Normal usage is just having def-alias on its own, check-ns picks it up.
We can also provide a set of typed namespace dependencies,
which are used to collect types in before checking. Basically, phase 1 is type collection,
going through the whole (typed) code base
(following typed dependencies), and phase 2 is the actual checking.
What next?
Any questions?
I think this a typed namespace... We can tell because
`cf` isn't everywhere. This is what real core.typed stuff looks like.
You have your normal Clojure code here
and then you have you annotations, (eg. line 9), not necessarily above the def,
but I like it because it fools me into thinking I'm using something like Haskell. (some laughs)
Typed Racket actually has more Haskelly syntax (: foo ..)
So (line 9) we're annotating foo, which
in this context is annotating
typed-workshop.annotations/foo. If we provide unqualified symbol, it resolves in the current ns.
We basically use these annotations
as an expected type for defn (eg. line 10). That's pretty important because
in Haskell we have inference, but in Clojure
, Typed Clojure, we don't have global inference, we have local inference.
So the rules: we need to annotate all vars
that are being used in a typed namespace.
We also need to annotate the parameters of local functions.
We saw that before.
That last point is a bit annoying.
Sometimes core.typed is really dumb with inference.
The local type inference algorithm isn't quite up to scratch at the moment.
I'm optimistic about getting better at inferring local functions, but I don't think
we're going to get very far getting rid of annotations like (line 9) in the next few years.
Top level annotations.
I think it's good practice to write the global type annotations here.
It makes us think about stuff, which is always good.
You can tweak
what core.typed checks,
but core.typed tries to help you not shoot yourself in the foot.
So we have the awful backdoor to core.typed
call tc-ignore, basically means
"core.typed is 0.1.* right now, there's going to be
Clojure idioms that I can't handle yet, use this until
I support them".
Say we accidentally wrap this in a tc-ignore (line 14).
Typed Clojure is going to grab the annotation (line 13), add it to the type env
then we come across
this call (line 19), and core.typed realises we haven't checked the definition of `forgot-check`.
So, the red line up the top, WARNING: Definition missing ...
is warning us of this. It's not a type error
to not check a definition, but we get an ugly warning.
Um.. clojure.core/iterate ? (Reading errors)
So, if we *don't* care about checking the definition
of a var, we add ^:nocheck metadata, which I'm about to do for iterate.
Because we got that
ugly warning before.
As I was saying before,
core vars are *not* checked.
Something also interesting, we can add our own clojure.core type annotations
, which will be frequent as core.typed is young, and not all clojure.core annotations are present.
Like here, I had to add my own type for iterate.
It's as easy as this really: add ^:nocheck
and then (qualify the var).
Iterate takes ... hopefully this is right ...
Yes, it takes a function
and an initial (value).
It takes a function from x to x [x -> x], and also takes an x,
and returns a lazy sequence of repeated calls to
(recursive calls) to that function.
You can use (iterate) like this.
Give me 30 items of this lazy sequence.
:nocheck isn't always good. (Line 25) Assume [Number -> Number], actually nil!
There's some flexibility here.
But you can get into trouble.
There's a problem
in core.typed, in that you can't infer
local lambdas
and can't infer local loops. You need to add annotations
This means any macro using a lambda or loop,
like loop, for, doseq, dotimes,
basically every macro out there :) needs to have a
wrapper.
Here's an awful one.
Here, `a` is going to be a bunch of numbers, and we
filter number that are not even.
The first thing we need to do for annotating a for loop,
is adding the return type's member type as an annotation.
This for loop returns a lazy sequence of AnyInteger.
t/AnyInteger here is a type alias: basically a union of
java.lang.{Long,BigInteger,Integer}, clojure.lang.BigInt etc.
It's everything that returns true if
you pass it to clojure.core/integer?.
This alias is helping me delay having to really work out how numbers work in Clojure :)
In the for loop, we need to provide two annotations.
First, the return type's member type
and also any loop variables.
Here, a :- AnyInteger says local binding `a` is going to be AnyInteger after it is bound.
We don't need to annotate the :when, because
:when expands out just to a normal `when`
Something interesting...
hmm, maybe not so interesting :P
I do hate these wrapper macros, and I promise I'll do something about them.
Here's doseq, some kind of thing
dotimes is hilarious because we don't need
to add annotations, but we
need the arrow anyway (the macroexpansion is troublesome).
Q: Does Typed Racket have this restriction?
A: Yes, Racket has like 200 loop forms, it's pretty hilarious.
They all need typed wrappers.
It's not quite that bad, but there's more than just for and doseq!
.. and loop.
loop> is a pretty important one,
This code's basically doing nothing.
It's taking numbers from nlist and just adding it to the accumulator.
And then give back a vector of [1 2 3].
But I'm going to use it to demonstrate
an interesting invariant
of core.typed.
...hmm I can't see the code.
Hmm, oh well. This error isn't the easiest thing to read, but basically what's happening is
we can see the function name (first line of error) which is clojure.core/next.
The actual call is here: (the line with in:) This is the fully macroexpanded form.
that we use for checking.
For some reason I've given the "next" (outer) form for good measure (see the second in:).
So basically what this part is saying
is clojure.core/next's type has
one arity. An arity that
takes an (Option (Seqable x)). An Option, all it is
is a union of nil and that (the argument to Option).
Our make believe Option type, it's kind of what we
think of as an Option type in Clojure.
So, we can either give nil or a (Seqable x).
So what did we give it...?
Ok. This (error) needs to give you a bit more information, because
`next` actually returns nil or it returns
the next sequence, but we're expecting a (Seqable Number) (see With Expected Type:)
So it's (core.typed) is a bit *** at that point.
Another TODO...
Any questions?
Alright, let's dig into
everything about nil.
So, nil is not
very useful in core.typed.
It's not a Seqable. It's not a List. It's not an Object.
And that's all there is to it. It is
(a subtype to) our Top type called Any.
Because of these facts,
we can actually guarantee that typed code does not have
NullPointerExceptions, which means we can give a type error
if we do something like this (line 17).
This is always going to blow up, or even if it (`a`) is a union containing
nil, there is potential for it to blow up here, so we give
a (error) like "Cannot invoke nil".
A pretty cool error to have at compile time.
And, the same
sort of error here (line 18).
It's not like in Common Lisp where nil is
a list or anything like that, and it's not like Java either,
because anything could be nil in Java.
So really I've tried to isolate the problem as much as I can.
We can guarantee we don't get NullPointerExceptions
in certain parts of our typed code.
Q: If we have a namespace without annotations
does that mean we have main types of Any? A: The rules are
You have to give a type for a var, but if we
a lambda/anonymous function that doesn't
have (for example line 18)
if we try and run this, then `a` is going to be Any here.
core.typed at least tries (to type check the function). The reason is
we can understand things like
this. We can use
.. where are my parens! ..
.. I wonder if this will compile/type check..
Oops.
The `a` here (line 18) is going to be Any, but the interesting thing is we can do a lot with that Any.
By kind of casting it, but not really.
By using assertions and conditionals.
So there's some
ways to debug our typed code
is that clear about nil, everyone happy?
We can add static assertions to our programs.
So, here's the weirdness of having
to add calls to `cf` around `ann`.
(line 9). So basically here (line 23) we're going to print the type environment
at this point.
Huh?
What is happening?
Silly vim! (some laughs)
Oh it's still in the wrong namespace! Oh well.
Why is this not working?
Let's move on to static assertions.
So small!
So this is kind of like
a pre-condition, but at compile time (line 20).
A "type pre-condition". So basically this is going to
to blow up because.. no it's not.
Wait, it *is* going to blow up. We've annotated (`a`) as Any,
so this is going to be
saying that "a is not a Number".
But adding code like this, I had
some code in an assignment I wrote
a cellular automata that had a grid, it was represented
as a vector of vectors. Then I changed it to be
a map, with a
keyword :grid
inside it. Basically I had (static) assertions that say
"grid is going to be (IPersistentVector (IPersistentVector Number)"
Once I changed the code
of the
.. no, once I changed the type of the Grid, all the functions
that used the grid complained.
That's just one way of
making your code a bit more robust (to changes).
I wish this worked..
That's not working.
How are we going for time? Half an hour.
Alright, we're going to move on to occurrence typing.
So occurrence typing is a
way to infer better types for local
variables as we progress along our code.
And there are two aspects to occurrence typing,
one is you attach filters/propositions
to functions
eg. (line 8) symbol? ('s type) looks like a normal function.
It takes Any, returns boolean. Then we have this funny thing here
which we say before
which expresses "what is true if we go down the then branch"
if we
pass this expression to an if statement, and "what is true
if we go down the else branch".
If we have something like (symbol? a) (line 20), then this 0 (in (is Symbol 0) line 8) is `a`.
0 refers to this Any, the first parameter.
So `a` come up and replaces this (0), so then
this particular expression, if you pass it to (the conditional of) an if statement says, then
if we're in the then branch, then `a` is a Symbol (is Symbol a). And
if we're down the else branch,
then `a` is *not* a Symbol (! Symbol a).
(function starting line 18) We don't know anything about `a` at (line 18), but we can infer we always return
a Symbol. The first case (symbol? a) updates the type
of `a` at this point (the branch on line 20).
And then we have (string? a), and here (branch on line 21)
we know that `a` is going to be a String, and it so happens that `symbol` takes a string.
So this branch is type correct.
Otherwise (line 22) we don't know much about `a`, so we return 'unknown.
So this is a contrived way of demonstrating
how these filters are being used (to update types down branches).
Any questions on that?
So we don't always have to use conditionals like this (line 26) to take advantage
of occurrence typing, we also
support pre-conditions. This (line 40) just expands out to an `assert`.
core.typed understands sequential asserts.
core.typed knows at line 41, we've already blown up (at runtime)
which means we don't need to worry about (type checking) it, *or* `a` is going to be a Number.
So we can use these propositions from
expression downwards (eg. sequentially in a `do`) and also inwards (like a conditional).
That's an improvement/enhancement
over Typed Racket's implementation.
Sam Tobin-Hochstadt, the author of Typed
Racket, conveniently told me how to do it, and it was very easy.
So I'm glad he proved it all (correct) for me, and I took all the credit (implementing it).
FIXME...
No. (laughs)
Vars. This is kind of surprising
.. core.typed really is
very strict about
whether a thing is mutable or not.
So a var in Clojure is mutable; you can change its value.
Usually what you do with a dynamic var, you bind it and then
just assume that it's immutable as we go down (progress in our program).
core.typed doesn't buy that. So this kind of expression
(line 14) is actually not (type) correct, because
there's no filters
on a mutable structure. We don't know
if we've gone down the then branch after testing the mutable structure
is not nil, we don't know if the value hasn't changed at this point.
So the key to occurrence typing working in this case
is
using when-let (line 20).
We convert the mutable structure (*the-number*) to a
immutable one, a local binding.
So now, what the when-let does, is actually test the number
and we know in this
.. hehe, you can see the bug.
Ah this isn't going to work is it. No.
My vim is not working.
I'm assuming that this when-let
creates a binding of the same type as *the-number*.
The local immutable binding (line 20) the-number should be used
at line 21 to please the type checker. (occurrence typing only works with immutable values).
Here's something cool.
I ported some of the contrib library algo.monads
which is a way of using monads
in Clojure.
There's a cool little thing
where we can combine macros
and annotating types.
So it turns out that if you have a
(TBH I forgot the details)
I worked on this last year with my dissertation. But the idea is that a monad fn
takes several implicit parameters. Like a `bind`, `return`,
..something like that.
This is kind of internal to how you use a monad function.
What we care about is the `m` here (line 293).
So you can see we're actually writing an ann-monadfn here (line 287)
and we're actually adding two type annotations.
The type here is a bit of boilerplate (line 276) to please
tools.macros' macrolet.
macrolet has particular bindings for syntax.
So that ann takes (annotates) m-join (to become (ann m-join Any))
We also annotate the (monad) function.
So really what's happening here, we have like 5
type, 5 arguments being here (`m`), so we put them (the types) in automatically (line 278-284).
What ends up happening (as a result of ann-monadfn), we have two (var) annotations
that are generated (from one form) with macros.
This is just showing how we can use macros to generate
types and to kind of get them out of our when we know
a bit more about our types than usual.
Any questions on that?
I'm sorry, I forgot the details on that. I just remembered "that was cool", I like it.
Q: Does that help you implement monads in Clojure?
A: I've been thinking about that recently.
I don't know much about that.
The next step for me with monads is trying to
type check Jim Duey's library protocol-monads.
Basically the inference in core.typed is not good enough to even hope
of doing something like Haskell, that needs to dispatch on the return type
of things. core.typed doesn't even change code.
Let alone know what the return type is going to be.
So there's a few things that need to happen: we need an extensible Clojure compiler, and then we need
some amazing research (laughs).
So core.typed/Typed Clojure
is can use Java interop freely.
Basically what happens is we
..let's get rid of these lines.. we can
we know the types of methods at compile time, just by looking up
the Java types.
There a few assumptions we have about Java, when interacting with Java.
Basically when you call a (Java) method from Clojure
if there isn't anything special, we default to
not allowing you to give a nil argument.
We always assume
we're very pessimistic, we assume we're getting back something that
could be nil. Constructors are a bit less
restrictive because constructors
as an invariant of Java, they can never return nil.
So we know that if we call a constructor we are going to get a non-nil value.
And same with parameters (non-nil).
And fields, anything goes with fields (nilable).
I'm just going to show you a bit of code that uses some Java interop.
So this is part of my cellular automata.
Basically I'm using
gnuplot to plot my
lattice, and this particular function
(line 16) just starts up a process for us
and gives us a lightweight map to
to work with here (line 21).
:out here is the OutputStream of the gnuplot process, that we can just throw things at,
and then :proc is the actual process.
So, the first thing to notice is that we've abstracted out
the details of what
this function returns with GnuplotP (line 8).
Which stands for, I guess, "gnuplot process". So it's going to be a map
with a :proc key that's a Process,
which is java.lang.Process,
and :out is a Writer, which is java.io.Writer.
The interesting things are these three lines (lines 11-13).
We know that, I think, we can call
java.lang.Runtime/getRuntime and never get nil.
(Line 11) what this :all is saying, is for all arities of getRuntime,
which may only be one, (it will never return nil).
The problem here is we're calling .exec (line 19) on a
(getRuntime), which would be a compile time type error with core.typed if it could be nil.
We need to add this annotation (line 11).
You end up accumulating a
whole bunch of assumptions about Java code.
Instead of comments on Java type assumptions, they are well structured. They are machine checked.. well not machine checked,
because we can't check the actual Java,
these are *definitely* just assumptions. I'm directing core.typed
to be as useful as possible
so we don't want core.typed to blow up at this .exec, because we *know* that getRuntime
never's going to return nil.
And we can do the normal
calling of constructors here (line 20). We've got the OutputStream of the process,
we can do (check) everything you can do in
Clojure normally.
This is a combination of, I guess, interop
and HMaps (lines 24-27). Our HMap here (`gnuplot`) we know the :proc key is a Process,
so this is interop call is always going to resolve property (line 27).
Any questions on that?
There's also nilable-param, which is another
directive to say "this particular parameter can be nil".
There's another one
called override-method, which you can do anything with.
That's kind of an internal thing (override-method).
You can definitely tune how useful
core.typed can be with
Java interop.
So of course the big hole here is "what if getRuntime
*actually* returns nil?", and there's basically nothing we can do about it
except extend
core.typed to add a runtime contract
and Typed Racket does this sort of thing,
You'd actually need a
way of inserting a contract around (.exec (getRuntime))
but there's currently no way to do that with the Compiler, so I haven't bothered
to even try.
You can annotate datatypes
and protocols.
The crucial thing to understand here is
I can only check what I can "see".
Right, if we start.. the guarantees that core.typed
gives you are only valid at the time that you
run it (type checking). If you start
implementing this protocol at runtime and you don't check it, you can't really do much.
That's basically the scope of how much
core.typed can help you, with respect to
dynamic loading of code.
So, something funny with protocols, it's another one of these
> functions where core.typed doesn't understand the macroexpansion (line 9).
But the macro also doesn't require any annotations.
The thing that's going on here, we've got an IAdd protocol,
that adds things, and here's its methods.
adder, (line 8).
It has an implicit first parameter, an IAdd,
takes a Number, returns a Number, and here's its definition (line 10).
So core.typed, does few things at this point.
It adds the annotation for the protocol, and it annotation for the (method's) var.
So there will be a typed-workshop.datatypes/adder var
and this var (reference) here (line 18) will have that type, as you'd expect.
Whenever we implement
the protocol we make sure that it conforms to the type.
Annotating a datatype, all you need to annotate your datatype is
the types of its fields.
It's the same syntax as fn>, where you just have a comma separating types.
You can see, ann-datatype (line 12) also
annotates the Java constructor,
ie. (Adder.), it also annotates the ->Adder constructor
and also map->Adder (correction: for records only, see ann-record)
So it tries to be as helpful as it can with annotating stuff.
That's about it with protocols and datatypes.
Any questions on that?
Blank slide. (some laughs)
I really like this, this is really cool.
So I've always wanted to typecheck the
Clojurescript compiler. If I sat down I could probably
do it at this point, I've done enough
work to get it done.
I just need to sit down and do it again. Wow my computer is slow.
Oh yea. I'm showing you
multimethods.
So this is kind of where multimethods and occurrence typing
meet.
So the multimethod takes one argument
and I've actually annotated that argument to be Expr (line 502).
Which is that massive type annotation I scrolled through before that I tried to hide.
Haha. That is an expression. So basically a union of
things like lambda, loop and other special forms.
So basically we take an expression (with emit) and return nil.
So emit has some side effect.
So the interesting thing here is the defmethods, the consumers
of this dispatch function (:op).
The dispatch function here is that an Expr, and returning the :op, and we can see if we go back up
to the type of Expr,
Expr is recursive type, where `x` is the
the original type, for example
here's the if statement: the :op is
(Value :if), it has a Form, which is just Any, we don't know anything about it,
and then :test is an Expr, :then
is an Expr, blah blah.
The idea here is, if we know that looking up :op
here gives us :if,
we know that everything else (in this union) is invalid/impossible at this point.
We can safely update (the binding of type Expr) to only be
this HMap: (line 65-72). That's basically what happens in the methods of
`emit`.
For example,
in here, core.typed can infer that this particular argument (line 651)
is going to be of :op :map.
And core.typed knows the types of simple-keys? keys vals.
Right now this support is basically limited to
just a single dispatch. The dispatch function
.. no.. it's limited in what
the dispatch function can return.
So the dispatch function here returns a keyword right.
If we wanted to do multiple dispatch, we could return a vector
of Classes, and we could use `isa?` to
dispatch on that. core.typed isn't quite up to that
at the moment.
5 minutes left. Any general questions on core.typed?
Q: A lot of people that use Haskell or Scala describe the experience of using
the type system as a tool
to design programs.
Are you aiming to do that with core.typed?
Does it lend itself to
checking things for correctness?
A: Yes,
it turns out that Clojure is a bit too dynamic
to really be good at the second thing.
At actually testing local properties.
But yea, definitely it's intended - you can design your programs
- you start, just write you types.
The mental model is just like Haskell.
I didn't actually see the Haskell Hole-Driven-Development (talk)
.. it's not in here..
Ah that's disappointing. Noisy hole, silent hole (laughs).
Come on, it's got to be in here somewhere..
Oh yea, here it is.
So if you haven't seen the Hole Driven-Development (HDD)
screencast, it's pretty cool. It's basically asking Haskell's type system
"what's the next thing you need to do"
and core.typed
can basically emulate this, by having something called a silent-hole.
Which blows up at runtime, but the type checker
just doesn't care about it, it just assumes it's correct.
Then we have a noisy-hole, which then the type checker tells you
"hey, you need to put this particular type in this position".
I'm sure this is very primitive HDD, but I though it was pretty cool.
Basically the idea is
these are just local (static) assertions (lines 22-24) that f is going to be
of this type, g is of that type etc.
If we put a noisy-hole in, then core.typed tells us "hey we found a hole" (line 48)
but we're really expecting a `c`.
I think it gets better.
No, you basically keep going, moving your holes
wherever you want them to go, and the type system will tell you
what types need to go in particular positions
.. I'm not sure how many languages can do that, it may be all of them.
But, I've only seen it done in Haskell.
I don't even know if I answered your question.
Q: I think you did.
Anyone else?
Q: You mentioned core.typed is a library, are there any advantages to providing a type system as a library?
A: Yea, so it's just a .jar, you don't need another compiler, you can just use (Clojure). The secret sauce is macros,
Typescript, I'm pretty sure it has its own
compiler.
The big difference is we don't need to throw away anything really,
we've already got our compiler.
But yea, I think that's one of the coolest things, that things like Typed Racket
and core.typed really are just a package
of stuff that you can just add wherever you like.
That's pretty cool stuff.
Q: Isn't adding such a forgiving type checker a problem?
A: I give the programmer full power to use type checking where they want, and where they don't want.
You could, yea,
make the type system not be any use at all. So the flexibility
of allowing you to use the rest of Clojure kind of comes at a price, that
core.typed is powerful enough
for you to make it basically useless. So it's about discipline,
if you want - if you're writing typed code
you need to follow a certain discipline, just like you would
writing in a statically typed language. The type system is there to
I guess kind of constrain you to a particular set of
expressions or ways to program.
It just so happens that I've tried to (support) everything except dynamic code loading
is basically what I'm trying to support.
Q: Can you declare how a function uses side effects?
A: No.
Ok, I think that's it. That'll do for me. Ok thank you.
(claps)