Frank A. Christoph <[EMAIL PROTECTED]> writes:
> 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?
For typed term graphs, I am providing a declarative typing system
without any notion of type inference in (BibTeX below):
http://diogenes.informatik.unibw-muenchen.de:8080/
kahl/PAPERS/Kahl-1997d_UFDeclTy_colour.ps.gz -- For colour media
kahl/PAPERS/Kahl-1997d_UFDeclTy_bw.ps.gz -- For monochrome media
This type system does not cover Hindley-Milner let-polymorphism,
but extends parametric polymorphism in other ways.
It can be seen in action in the term graph programming
and program transformation system HOPS:
http://diogenes.informatik.unibw-muenchen.de:8080/kahl/HOPS/
Best regards,
Wolfram
=======================================================================
@TechReport{Kahl-1997d,
author = {Wolfram Kahl},
title = {A Framework for User-friendly Declarative Typing Systems},
institution = {Fakult\"at f\"ur Informatik,
Universit\"at der Bundeswehr M\"unchen},
year = 1997,
number = 9704,
address = {D-85577 Neubiberg},
month = DEC,
abstract = {Advanced type systems frequently pose problems to the
user, as can already be observed with the still
rather simple type systems currently in use
e.g.\null{} in Haskell or ML: error messages
signaling type errors frequently give complex types
and little clue where the real source of the error
is.
We present a class of typing systems that are
designed for online use, preventing input of
untypeable constructs and guiding the user through
the construction of programs with complex
types. Since this implies making explicit the
relation between programs and their types, the
choice formalism for this purpose is that of term
graphs, where much more program structure can
usefully be made explicit than in linear notations.
After presenting a framework for the definition of
typing systems in term graphs, we discuss the
advantages of this approach and sketch applications
to e.g.\null{} polytypic programming.}
}
