I'm a 3rd year PhD student at Indiana
University working with
I am interested in programming language research, especially
that which relates to type theory, formal verification, and
gradual typing. My
work has involved an extension to
which adds support for some basic dependent types.
Occurrence Typing Modulo Theories, with David Kempe and Sam Tobin-Hochstadt, at PLDI 2016.
Design and Evaluation of Gradual Typing in Python, with Michael M. Vitousek, Jeremy G. Siek, and
Jim Baker, at DLS 2014.
Linking the Past: Discovering Historical Social Networks from Documents and
Linking to a Geneological Database, with Douglas J. Kennard and William A. Barret, at HIP 2011.
The more things change, the more they stay the same… at least for these updates! =)
TL;DR Typed Racket has a whole bunch of new parts under the hood for v6.8—hopefully as a user you can’t tell (unless of course it’s because your program type checks faster)!
If you’re a little curious about “how the sausage is made” (or what new ingredients they contain…?) read on!
PLT Redex is a great tool for tinkering with and examining various aspects of programming languages. Although it can be used to programmatically generate mathematical figures for papers and the like (awesome!), the actual machinery for doing so is a little lower level than you want 99% of the time.
To alleviate this, I developed a package (typeset-rewriter) with a few simple tools that make it much easier to build the rewriters redex natively supports.
Although Typed Racket (TR) can currently typecheck a large number
of common idioms found in Racket code, reasoning about direct and indirect
usages of aliasing has escaped its grasp... until now!
Coq’s support for dependent types mean that type checking not only
catches trivial errors like passing an integer to a function expecting
a string, but it can also check and verify types which represent
properties regarding the functional behavior of the a program.
I thought it would be edifying to use this capability to write a
verified version of quicksort (i.e. a quicksort with types that
specify its behavior), and it was!
This post is a collection of simple C code snippets and roughly equivalent Racket code.
Hopefully if you’re coming from a C background (or similar) and you’re struggling to make sense of Racket code, these examples will assist in clearing the fog.
What is the type of a function which returns the first element of a list? One possible (and likely common) answer would be:
This (typed racket syntax) says first is a function from a list of X’s to an X (where X is any type). However, we really know that, although its type is ((Listof X) -> X), if we pass an empty list of X we will not get an X, but a runtime error of some sort (e.g. no values). The type then isn’t really giving us a guarantee of what it will do for us… it’s just telling us what it will try to do for us if it doesn’t fail.
“No. Try not. Do… or do not. There is no try.” - Master Yoda
There is a parallel in math: some functions are not defined for all possible input values (e.g. f(x)=1/x). These are called partial functions (as opposed to total functions). It is common practice to reserve the term “function” for total functions in math, while in programming partial functions are ubiquitous and there is little effort to distinguish between the two. If only there was some way that the types could reflect this possibility…