Here’s the syntax for the simply-typed lambda calculus (STLC):
Here are the typing rules, written in the usual natural deduction style:
It turns out that these rules are not only enough to provide typechecking but also type inference if you feed them into Prolog, though that’s far from a coincidence. Type inference for STLC is possible, and Prolog was the result of decades of research into finding proofs (in this case a typing – a proof that a given term has a given type) for problems stated in this style. It’s even less of a coincidence because STLC admits principal typings – so all proofs that a term has a given type are equivalent.
Rewriting the Rules
Suppose we deliberately ignore the existance of Prolog (but not of unification, as it’ll turn out) – how can we write the rules to make it more obvious what to do?
In my previous post on constraint programming, I took the following term type as an object language and started doing meta-level work with it:
data Term = Term !Label ![Term]
I handled the meta level in a manner that isn’t particularly typeful:
data Term = Term !Label ![Term] | Metavar Integer
That’s okay for a quick and dirty solver, but there are better options if you want a bit more safety! Continue reading
In Introduction to Constraint Programming I made something of a mistake. It was a remarkably easy one to make, because I stepped outside the bounds of the type system’s help – and especially that of those who’ve declared interfaces before me.
In forthcoming posts I’m going to be making heavy use of constraint programming, so I’m going to do an intro to constraint programming as I see it first so everyone knows what I’m talking about before I start making controversial statements. The code’s all in Haskell, which is my usual language of choice. If you’re feeling pedantic, assume I’ve got the basics imported (Data.Map, Control.Monad etc) and hidden stuff that’d conflict with the only things that typecheck – there’s a full source file to play with at the bottom if you want to go further.
Some basic definitions
Constraint programming isn’t a paradigm itself, but it can be viewed as a "paradigm transformer" Continue reading
So I figured I should set up an academic/FP/etc blog and get writing again – preferably one where I didn’t have to do the sysadmin work. I also didn’t particularly want to hang on to the previous title I guess – I don’t think there’s anything wrong with my past self’s sense of humour, but I suppose I’m a bit more wary of reactions these days. Especially as I’m hoping to be talking about
restraintconstraint programming a lot!
I’ve not been too active with such things the last few years due to quite a collection of personal circumstances, but I’ve definitely got things to say if only I can get round to them. I don’t have a lot of in-person contact prodding me about such things, so a little online cheerleading would be a big help – hopefully I’ll have more up soon.