[PL-sem-jr] Another topic: unification

[Felix S Klock II]

PLjr-ites-

Seeing Dave's recent email calling for a presentation on GADTs reminded 
me of something.

I've recently been reading papers on (the undecidablity of) 
Semi-Unification and 2nd-Order Unification.

Going through the process of trying to solve an instance of 2nd-Order 
Unification made me realize what an interesting problem it was.

For example, let Type be the set of simple types generated by arrow and 
some collection of base type constants containing at least { A, B, C, D 
}.  Can you find some function F, taken from the domain Type to Type to 
Type, such that:
F( A -> B )( C -> D -> B )   =   F( B )( C ) -> D -> A -> A -> B

[[ This was adopted from Aleksy Shubert: 
http://www.mimuw.edu.pl/~alx/papers.php ]]

Also, there is much work in the area of defining useful decidable 
subclasses of 2nd-Order Unification.

So I would like to see someone give a talk on the research in 
Unification in general.  I'd be willing to help with the presentation, 
but I don't want to do it alone.

-Felix

----
"At a funeral, the real programmer is the one saying
  'poor George. And he almost had the sort routine working
  before the coronary.'"  -Real Programmers don't use Pascal