[TYPES] HM(x) vs Theory of Qualified Types

[Martin Sulzmann]

Hi,

robert dockins writes:
 > [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
 > 
 > I have recently been reading some of the literature on HM(x), and I am 
 > attempting to fit it into my mental framework.  From an initial reading 
 > it appears somewhat similar to Mark P. Jones' Theory of Qualified Types, 
 >   but I have several times seen HM(x) referred to as a more general 
 > framework.  Does HM(x) fully subsume Qualified Types? Could someone on 
 > this list perhaps explain their exact relationship?
 > 
 > Robert Dockins

below I give a rough comparison. The short summary is this:
I don't think that HM(X) subsumes TQT (the theory of qualified types).
They're somewhat incomparable, at least the original formulations
of HM(X) and TQT are incomparable.
Here's why.

HM(X) formalizes (the folklore idea of) a general Hindley/Milner system
with constraints. In the original description [1,2], the constraint system
X is described in terms of a cylindric algebra which turns out to be
nothing more than a algebraic formulation of a first-order logic theory.
The predicate system of TQT [11] seems more general than a first-order
logic theory, though I'm not 100% sure here.

There are clear differences between HM(X) and TQT when it comes to
defining the semantic meaning of programs. The original HM(X)
description [1] contains a general type soundness result based on a 
denotational semantics. Later, Skalka and Pottier [4] gave a syntactic
type soundness result. In both cases, the semantics is call-by value.
On the other hand, the semantics of TQT [11] is explained in terms of
the dictionary-translation scheme [12] where the target semantics
is call-by name. If we ignore the call-by name vs value issue,
the crucial difference is that the meaning of HM(X) programs can be
explained in terms of a untyped semantics whereas the meaning of TQT
programs is tied to the type of a program.

Let's take a look at type inference.
HM(X) comes with a generic algorithm W style inference system
which yields principal types under some sufficient conditions
imposed on X [1,2]. There are lots of similar type inference results
for more specific systems. In particular, work by Remy and Pottier
[7,8,9,10] is important and relevant here. In case of TQT I only know 
one good reference [13].

HM(X) has been applied in a number of settings such as
program analysis [5], subtype systems [8,10] etc.
The main application of TQT seems to be type classes which
is of course a huge area in itself. I don't claim that TQT couldn't do
program analysis. Though, in case of program analysis it's very
convenient to have a HM(X) semantics which is independent of the type
given to a program. Another strength of HM(X) is to have a semantic
notation of constraints. Thus, we can easily simplify constraints.
Here's a classic example: a=c is equivalent to exists b. (a=b,b=c).

There are also hybrid formulations. For example, in [6] a
HM(X) style inference system is given but the semantic meaning
of programs is explained in terms of a TQT style dictionary
translation.

Ok, I'll stop here. My rather brief comparison is necessarily
incomplete. Please correct me if I'm wrong and add further references
if I've missed something.

-Martin


P.S.

In case of type inference for non-regular equational theories [14],
HM(X) helped to understand the problem [3] and could provide a neat
solution [2].

 
------------ references -------------------

[1]
M. Odersky, M. Sulzmann, and M Wehr. 
Type inference with constrained types. 
Theory and Practice of Object Systems, 5(1):35-55, 1999.

[2]
M. Sulzmann. 
A General Framework for Hindley/Milner Type Systems with Constraints. 
PhD thesis, Yale University, Department of Computer Science, May 2000.

[3]
M. Sulzmann, M. Mueller, and C. Zenger. 
Hindley/milner style type systems in constraint form. 
Research Report ACRC-99-009, University of South Australia, 
School of Computer and Information Science, 1999.

[4]
Christian Skalka and Francois Pottier. 
Syntactic Type Soundness for HM(X). 
Electronic Notes in Theoretical Computer Science, 75, 2003.

[5]
K. Glynn, P. J. Stuckey, M. Sulzmann, and H. Sondergaard. 
Boolean constraints for binding-time analysis. 
In Proc. of PADO'01, volume 2053 of LNCS, pages 39-63. Springer, 2001.

[6]
P. J. Stuckey and M. Sulzmann. 
A theory of overloading. 
In Proc. of ICFP'02, pages 167-178. ACM Press, 2002.

[7]
D. Remy
Extending ML Type System with a Sorted Equational Theory.    
Research Report 1766, Institut National de Recherche en Informatique
et Automatisme, 
Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992.

[8]
F. Pottier. 
Synthese de types en presence de sous-typage: de la theorie a la pratique. 
PhD thesis, Universite Paris 7, July 1998.

[9]
F. Pottier. 
A framework for type inference with subtyping. 
In Proceedings of the third ACM SIGPLAN International Conference on
Functional Programming (ICFP'98), pages 228-238, September 1998.

[10]
F. Pottier. 
A versatile constraint-based type inference system. 
Nordic Journal of Computing, 7(4):312-347, November 2000.

[11]
M. P. Jones
Qualified Types: Theory and Practice, 
Cambridge University Press, November 1994.

[12]
M. P. Jones
Coherence for qualified types, 
Research Report YALEU/DCS/RR-989, 
Yale University, New Haven, Connecticut, USA, September 1993.

[13]
M. P. Jones
Simplifying and Improving Qualified Types, 
In FPCA '95: Conference on Functional Programming Languages and
Computer Architecture, La Jolla, CA, June 1995.

[14]
A. Kennedy
Type Inference and Equational Theories
Research Report LIX/RR/96/09, LIX, Ecole Polytechnique, 1996.