[TYPES] "Constraints as types" paradigm

[Manuel Fahndrich]

Jacques,

If you are not already aware of it, I suggest you look at Aiken and
Wimmers 93 FPCA paper on 
"Type Inclusion Constraints and Type Inference", where set expressions
and set constraints are used to express types. As far as I know, this
system has principal typings, but not principal types.

Manuel Fahndrich

-----Original Message-----
From: types-list-bounces+manuel=cs.berkeley.edu at lists.seas.upenn.edu
[mailto:types-list-bounces+manuel=cs.berkeley.edu at lists.seas.upenn.edu]
On Behalf Of Jacques Carette
Sent: Monday, March 22, 2004 1:29 PM
To: types at cis.upenn.edu
Subject: [TYPES] "Constraints as types" paradigm

[The Types Forum,
http://lists.seas.upenn.edu/mailman/listinfo/types-list]

I have heard some informal references to a "constraints as types"
paradigm.  I have however not been able to find a 
lot of concrete references.  I am aware of HM(X) by Odersky, Sulzmann
and Wehr, which certainly takes this idea part 
of the ways [and know of *some* of the follow-up papers].  One could
also consider Haskell's type classes as another 
examples of this idea.

However, I am only realy interested in this idea in the absence of an
underlying type system with 'principal types' -- 
otherwise there really is no point in moving to constraints, as closed
forms are usually more informative than 
implicit definitions, although they tend to be more verbose.  An
evocative analogy (for me!) is the difference between 
closed-form solutions to (differential, integral, ...) equations versus
a normalized form of the equations themselves; 
although people prefer closed-form solutions, it is algorithmically
much(!) easier to find properties of the 
'solution' from the original equations than from the closed-form
expression [is my Computer Algebra background showing 
yet?].

Are there people on this list who can turn the vague thoughts above into
precise references to written material?

Jacques Carette