Subject: my type constraints
From: Vassily Litvinov (vass@cs.washington.edu)
Date: Tue Jan 23 2001 - 14:23:24 PST
After long hard work, I have separated out the constraint solving task
which is at the core of my type sytem. (I.e., a lot of things are/can be
expressed via solving constraints.) Below is a purified description of
the type system and constraint solving.
With the goal of making a preview for my Monday's presentation, I welcome
all feedback, including clarity of presentation and ideas about constraint
solving algorithm.
Vass
-------------------------------------------------------
The TYPE SYSTEM operates on the following notions:
type T ::= X // type variable
| tc(T1, ..., Tn) // type constructor, e.g., int, list(X), ...
| lub(T1, ..., Tn) // least-upper-bound, or intersection type
| glb(T1, ..., Tn) // greatest-lower-bound, or union type
| top | bottom // top and bottom types
(Each type constructor tc is only used according to its arity.)
constraint C ::= T1 <= T2
(This is a subtype constraint.)
subtype declaration D ::= forall X1...Xn (C1 & ... & Cn) => tc1(...)<=tc2(...)
(The types passed as arguments to tc1 and tc2 (omitted for brevity)
are allowed to refer to type variables X1...Xn.)
The subtyping is defined by the programmer via a set of conditional,
parametric subtype declarations. (It is not inferred by the typechecker.)
Multiple subtyping and conditional subtyping is allowed. Here are examples
of subtype declarations (assuming "int", "printable", "array", "collection"
are type constructors):
int <= printable
forall X. array(X) <= collection(X)
forall X (X<=printable) => collection(X)<=printable
Informally, a constraint holds when it can be inferred from the program
declarations by instantiating them, proving sub-constraints, and involving
general subtyping axioms (such as transitivity).
I haven't written down the formal definition when a subtype constraint holds.
For example, the above declarations could be interpreted as the following
Prolog program:
subtypes(int, printable).
subtypes(array(X), collection(X)).
subtypes(collection(X), printable) :- subtypes(X, printable).
extended with subtyping axioms, such as:
subtypes(X, X).
subtypes(X, Z) :- subtypes(X, Y), subtypes(Y, Z).
So that the goal
?- subtypes(array(int), printable)
is provable.
The CONSTRAINT SOLVING TASK, in the simplest case, sounds like this:
Given subtype declarations and a subtype constraint (not referring to any
type variables), does the constraint hold?
The most general form of constraint solving is this:
Given subtype declarations, does the following implication hold:
forall X1...Xn (C1...Cm => (exist X'1...X'n' such that C'1...C'm'))
where type variables X1...Xn and X'1...X'n' range over the Herbrand universe
of types and the constraints C1...Cm and C'1...C'm' do not refer to type
variables not bound by the corresponding quantifiers. (It is possible to
consider both "closed world" and "open world" systems, although we tend to
prefer "open world" approach.)
The constraint solving task is at the core of the type checking rules and
can also be used to perform type inference.
-------------------------------------------------------
This archive was generated by hypermail 2b25 : Tue Jan 23 2001 - 14:23:29 PST