Skip navigation

Category Archives: Teaching

Well, it’s been quite some time since I posted anything, because this was one busy semester (even without coffee spoons).  A lot has been going on here at U. Iowa to keep me from finding time for blogging.  One of the biggest things, which might be of interest to some, is the big bump in enrollment which expanded my undergraduate Programming Languages class by 50% from around 60 registered students to 90.  This is because it is a required class for majors, and our enrollments are up a lot, as at a lot of other places.  The shocker to me was just how much email the class generated.  There were 4 programming assignments, 12 short assignments, a midterm and a final.  Most of the emails for the class were, I believe (but have not tried to confirm) related to the programming assignments.  Since I keep all my email, I can tell you that the course generated around 1,075 emails, of which I personally wrote around 430.  For a class that runs 15 weeks (or 105 days), this comes out to be a little over 4 a day on average.  Seems like a lot.

Is it worth it?  Yes.  It is a very fun class to teach.  I try to cover some basic informal ideas from Programming Languages from an implementor’s point of view, using a functional programming language.  This has been OCaml for me for the past 4-5 years.  I did introduce Haskell and Coq, too, at the very end of the class.  I am actually toying with the idea of moving to Agda for Spring 2014, since Agda promises to give me the coding elegance of Haskell, in particular definition by recursive equations, as well as verification power as in Coq.  Many students, who have learned programming through Java and Python, found programming in OCaml to be a mind-blowing experience.  Imagine what it would be like in Agda!  Maybe even too mind-blowing?  We will see if I am brave enough to try the experiment.  I have to learn Agda first, which hopefully we’ll manage this summer.

One example assignment we did was to write a compiler from a high-level language (“rsketch”) similar in spirit to Logo, but using notation for regular expressions, to Processing.  This makes a nice connection back to the class, since I learned about Processing from a former student, JJ Meyer.  I quite liked these rsketch programs (students had to compete for “audience favorite” for 5 points), as well as many others (f is for forward, r n for rotation by n degrees, cr+ n for increasing the red component of the drawing color by n, l+ n for increasing the length of the segment to draw by n, etc.):

  ( f r 20 cr+ 4 w+ 1 l+ 1 cg+ 5 cb+ 3 f r 255 ) * 1200


  ( h ( f r 30 l+ 1 cb+ 1 ) * 80 l- 80 r 5 cg+ 30 ) * 120

This past week we held a mini-symposium here at U. Iowa.  Cody Roux, postdoc’ing with Jeremy Avigad at CMU, and Muhammad Nassar, a doctoral student working with Geoff Sutcliffe at U. Miami, were here for the week. We also had talks from a number of us here, and John Altidor, a doctoral student from U. Mass. Amherst who happened to be in Iowa City for the semester and joined our group for that time. I  talked a lot of type theory with Cody, and worked on StarExec in support of TPTP with Muhammad.  It was quite productive.  I really liked hearing about Cody’s research agenda on the structural theory of PTSs, where he looks to see what operations on PTSs preserve normalization.  This was very cool, and Cody had some great technical results and insights about things like why adding individual quantification to F_omega to formulate the Calculus of Constructions does not increase the proof-theoretic strength of the system.  This is work in progress, it seems — hopefully a paper will appear soon.

So, that’s a short update.  I have something more substantial to blog about soon, namely dualized type theory, which we — Harley Eades III, Ryan McCleeary, and I — are hard at work developing.  But that will have to wait till later in the week or next week.


The semester is well underway here at The University of Iowa.  I and the people I work with here are working away on a number of different projects in programming languages and type theory.  I had one little PL puzzle I thought I’d write about here.  I’m teaching, as I have done the past few springs, the undergraduate “Programming Language Concepts” class, required for CS majors here.  Figuring out what to do in such classes has attracted considerable attention in the past few years (if you never had a chance to take a look at the whitepapers for the 2008 SIGPLAN programming languages curriculum workshop, they make for interesting and even entertaining reading).  My solution to the conundrum is to  cover programming languages informally, from a language implementor’s perspective.  So we start off with grammars and finite automata, then talk about how to implement simple interpreters and type checkers, in OCaml.  Indeed, teaching OCaml is a major focus of the course.  We also take a look at some declarative paradigms like string rewriting (just a little) and Datalog.

The problem of incentives in academia is really a very vexing one.  There’s a lot to consider about incentives when it comes to research, though that’s a subject for another time.  I’ve thought a bit about incentives for students in classes, too.  I’m particularly interested in how to disincentivize cheating.  There are obvious short-term benefits for students who cheat (and don’t get caught), which of course, are heavily outweighed by the long-term costs, both in terms of personal morality, which is a major or even most important factor for success at honest endeavors in life (and maybe even among thieves), and also in terms of developing technical skills, which will help with getting and retaining good jobs.  Most students know all this, but are still tempted to cheat anyway.  How can we discourage this?

The obvious idea is to remove the short-term benefits of cheating.  I suppose this requires considering different cheating scenarios.  A simple one is the inappropriate collaboration.  Let’s imagine that two students of roughly equal skills decide to divide a homework assignment in two, so each can get a complete solution to turn in, while doing only half the work.  Group projects accept this as a reasonable model for homework, only to have to deal with the problem that not everyone does contribute equally.  But when you’re cheating, at least in this scenario, you don’t have a lot of incentive to share your work if you’re not getting something in return.  Sometimes people do this, hoping to gain social benefits such as the gratitude of the person they’re giving their work to.  But it would take a bit more than that, I think, to incentivize people to solve completely different homeworks for their classmates.  So if each student had his/her own individualized and unique assignment, cheating would be disincentivized, at least partly.

I’m trying to incorporate this idea into my class by randomly generating individualized homework problems from the student id of each member of the class.  This is not that easy.  I recently wrote a small OCaml program to generate OCaml type inhabitation problems randomly.  The goal is to produce types like

'a -> ((int * 'b) list) -> ((int list) * 'b)

and have the student write a total function of that type.  I wanted to incorporate polymorphism into the types (hence the ‘a and ‘b), and also a few basic OCaml type constructors like pairing (*) and lists.  I needed the types to be randomly generated, not too big, and with some parameters I could tune for easier or harder problems.  This turned out to be challenging, for several reasons.

First, it is entirely possible to write types which don’t have a solution according to the above requirements.  For example, any type with a type variable for the final output, which does not also show up in the input, is uninhabited by a total function.  For example, only diverging or aborting programs inhabit

'a -> 'b

Now, it is not too hard to avoid such types.  If your types are completely first-order, you just need to make sure that the output does not use type variables not found in one of the inputs.  I did want to have simple second-order types, at least for a few problems (I assigned 8 of these per student), but this could be easily achieved by disallowing type variables in the inputs of function types for arguments.  Actually, I allowed types like

'a -> ((int * 'a) -> 'b) -> 'b

where the first input is restricted to be just ‘a, and then ‘a is allowed in the input type for functional arguments.  Types like the above actually confused students, though, because the type for the second argument is itself actually uninhabited by a total program.  Some students thought that meant the whole type itself was uninhabited.  I’m ok with that confusion, because it helped highlight the game-theoretic nature of function types: the above type requires you to give me a function from pairs of ints and ‘a things to ‘b.  It’s not my problem if there are no such functions, since the burden of inhabiting that type is on the calling context.

Other issues that arose: I disallowed solutions that used recursion (to try to enforce totality without being too explicit about it), but that did not go far enough, because it is very easy to inhabit types in OCaml if you are allowed to have partial matches.  For example, to inhabit the monomorphic

(int * int) -> bool -> bool

you can write this partial function:

let f (1,2) true = false;;

That is really not what I had in mind, though it is still not a bad exercise. I wanted students to have to write something like

let f x y =
match x with
(x1,x2) -> (x1=x2+0) && y;;

This piece of code just uses the input arguments x and y in such a way that the OCaml type inferencer constraints them to have the proper types.

Another problem is that one can get away with overly general solutions that are very easy to write. For example, if you just use

let f x y = y;;

and then ask OCaml if f has the above type, it will say yes! Because the above type is an instance of the more general type that this code has, which is

'a -> 'b -> 'b

Finally, some students thought that the output they returned had to depend on all the inputs. This makes the problem quite a bit harder than it needs to be. It is otherwise sufficient just to use the input variables enough to constrain their types, and then throw away the intermediate result by using a dummy let, as in this code of type int -> ‘b -> ‘b:

let f x y =
let _ = x+0 in

Could we set up the problem so that all inputs must be used to obtain the output? That seems doubtful, at least if we have the requirement that all functional argument types must be inhabited themselves by a total function. If we don’t use polymorphism — and hence parametricity — we aren’t going to be able to force arguments to get used.

One last thing about this idea of randomly generating type-inhabitation problems for class: several students told me they enjoyed solving these. I think that’s because the problems really took on the form of puzzles, and everybody likes a good puzzle. So I definitely plan to try randomly generating puzzle-like problems for subsequent homeworks. It may help disincentivize cheating, and it could be fun for students and myself alike.