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

y;;

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.

## 2 Comments

This is a great idea actually! I read somewhere that there was a haskell program for checking type inhabitation by using an intuitionistic propositional logic prover (surprisingly subtle to implement). You could then imagine adding data-types to your logic, or using linear logic or “relevant” logic to impose more constraints on the solutions required…

Aha: http://www.augustsson.net/Darcs/Djinn/

Cody,

That is a great idea! Yes, I thought about the problem from a proof-search perspective, but it was not so clear to me how to constrain the search to find inhabitation problems suitable for these exercises.

Aaron