This triangle function gives us simultaneous substitution.

I think, if I understand Thorsten Altenkirch, correctly I'm supposed to call the triangle `bind' and say `Oh look! A Kleisli triple!' Thorsten points out that there are a few more `useful properties' I didn't mention on the slide. Of course, the things which should hold do hold. Can you guess what they are?

I hope you don't mind me overloading the triangle, lifting it to positions also. The coherence property tells us, in particular, that if put t p and t have a unifier f, then

We know what that means about (f |> p), and hence about p.

Now that I'm overloading it, I might as well carry on and let |> map renamings too. For example, two slides on, I wrote (thin w) |>, when I should have written (leaf o (thin w)) |>, and I'm trying to sweep that mistake under the carpet. Of course, if we buy Luo-Soloviev-Bailey-Jones coercive subtyping, we can get away with it on the machine, as well on slides.

Next: the occur check | Prev: the tree syntax | Up: contents