[TYPES] Two technical reports on inference/translation methods of

[Martin Sulzmann]

Hindley/Milner with extensions
X-Mailer: VM 6.43 under 20.4 "Emerald" XEmacs  Lucid
Message-ID: <16823.63390.726206.233626 at sf0.comp.nus.edu.sg>

Hi,

the following two technical reports are available via 
http://www.comp.nus.edu.sg/~sulzmann/

A Unifying Inference Framework for Hindley/Milner with Extensions
by Peter J. Stuckey and Martin Sulzmann
National University of Singapore TR12/04

A Systematic Translation of Guarded Recursive Data Types 
to Existential Types
by Martin Sulzmann and Meng Wang
National University of Singapore TR22/04

Abstracts can be found below.

Comments are welcome.

- Martin


------------------------------------------------------------------

A Unifying Inference Framework for Hindley/Milner with Extensions
by Peter J. Stuckey and Martin Sulzmann
National University of Singapore TR12/04

Abstract:

We present a unifying framework for Hindley/Milner with extensions 
such as type annotations, type classes with existential types etc.
A novelty is that we can express a generalized form of  guarded 
recursive data types which allows us to model a limited form of 
dependent types. Type inference becomes a challenging problem.
We give a precise characterization of typability in terms of
solvability  of logic formulae. We introduce a novel solving 
procedure for formulae to support type inference. In general, 
principal solutions do not exist, hence, our solving procedure 
is only sound but not complete. However, we identify several 
instances of our system for which inference is complete.



A Systematic Translation of Guarded Recursive Data Types 
to Existential Types
by Martin Sulzmann and Meng Wang
National University of Singapore TR22/04

Abstract:

Guarded recursive data types (GRDTs) are a new language feature 
which allows to type check the different branches of case expressions 
under different type assumptions. We show that GRDTs can be translated 
to type classes with existential types (TCET). The translation to TCET 
might be problematic in the sense that common implementations such as 
the Glasgow Haskell Compiler (GHC) fail to accept the translated program.
We provide for a refined translation from TCET to existential types
(ET) based on a novel proof term construction method. The resulting ET 
program is accepted by GHC. Our work can be seen as the first formal 
investigation to relate the concepts of guarded recursive data types 
and (type classes with) existential types.