[TYPES] "Constraints as types" paradigm

[Martin Sulzmann]

Hi,

you also might want to check out

"A Theory of Overloading" by Stuckey/Sulzmann [ICFP'02]

Note that the underlying system is Hindley/Milner. The general
focuss is on how to make use of constraints
to describe the relations among program text and types.

Martin


 > [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
 > 
 > 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