Re: more closed-world chatter

On May 12, 1:55 am, Jon Heggland <jon.heggl..._at_idi.ntnu.no> wrote:
> Marshall wrote:
> > On May 11, 4:03 am, Jon Heggland <jon.heggl..._at_idi.ntnu.no> wrote:
> >> Marshall wrote:
> >>> If we are joining X with DUM, then there are necessarily no
> >>> attributes in common, so we would not expect to perturb
> >>> the attribute types from X.
> >> So you won't consider each type of the result to be additionally
> >> constrained by "and false", thus leading to the bottom type?
>
> > Oh, um, uh, yeah, that would work.
>
> I'm not really convinced one way or the other myself. I'll read up on
> what D&D have to say on the matter, but the join-subtype thang sounds
> more reasonable than the AND FALSE-bottom one.
>
> > I don't have the clarity on this issue yet that I need to.
> > I'm used to thinking about traditional type systems
> > but I'm trying to transition to thinking about more
> > general constraint systems, and sometimes I confuse
> > myself.
>
> So you suggest a type system where types are sets, defined by
> constraints (or enumerations? You could formulate an enumeration as a
> constraint, I guess);

Right.

At the lowest level, you can just identify a set of values, and constrain a variable to only be able to take on values of that set. (This is basically what typical type systems do.) But further, you could specify general constraints in the form of any boolean expression. Technically the term "constraints" should only apply to variables, but we could use the exact same mechanism to "tag" constants with boolean expressions as well, to facilitate reasoning about code.

> and may have names (for convenience), but don't
> need them;

Right. Sets (including relations) are first class entities.

> subtypes/supertypes are implicit, based on set inclusion; and
> other types may be constructed/inferred/expressed as intersections,
> unions and differences between other types?

Yes! Although it is not at all clear to me yet how well this will work.

> And the type of A in "T where A = 'J'" is the set { 'J' }, if the type
> of A in T includes 'J', and { } otherwise?

Mmmm, well in general I think of these constraints as static entities only, so inferred constraints are determined by the expressions, not the runtime values.

> Sounds interesting, but undecidable, and not restrictive enough for my
> taste. :)

Definitely interesting (if I say so myself); definitely undecidable.

As to "not restrictive enough" I hear you! My intention, though, is that you can make it as restrictive as you want. You can dial the compiler's restrictions down to where you have a dynamic language, and use no constraints, or dial it up to the point where you have a language that is actually significantly *more* restrictive than is usual. You could, perhaps, decide you want a termination proof of your program or else; the compiler would then accept only those programs for which it could infer a termination proof, or for which a termination proof was supplied. At that point the language is sufficiently restricted as to no longer be Turing complete.

Marshall Received on Sat May 12 2007 - 17:06:34 CEST