Does anyone know if Hindley-Milner type inference has been characterized in
a non-operational way? I mean either some sort of canonical correspondence
(as the simply typed lambda-calculus with intuitionistic natural deduction)
or some statement that describes it in terms of a universal property, like
in category theory. For that matter, is there any work at all which has
characterized the notion of type inference (not just H-M) for functional
and/or related languages in a declarative manner, perhaps in terms of proof
theory?
Thanks in advance.
If I receive many substantial private responses, I will post a summary
later.
--FC
