William D Clinger scripsit:
> If this is to be considered, then I would suggest
> going further and requiring any two enumeration-type
> objects whose universes represent the same set of
> symbols to be eqv? and interchangeable with respect
> to all of the enumeration-set operations.
I discussed that idea with some other participants on #scheme
before proposing it. Structural equivalence such as you propose
was my original idea, but I came to be convinced that nominal
equivalence was better. Here's an edited transcript of that
discussion:
jcowan: I'm trying to make up my mind whether sets of enumerated values
should belong to both extensional and intensional types.
jcowan: That is, is it enough to make two sets comparable that they
share the same universe of symbols, or should they be required to
also have a common descent?
jcowan: (This is analogous to the difference between structural and
nominal typing.)
Riastradh: What do you mean by `required to have a common descent'?
alaricsp: I think that arguments about different type systems really
boil down to different type systems working best in different areas,
and therefore would seek to find a type system that encompasses
others :-)
alaricsp: Also, it's interesting to ask what you want from a type system.
jcowan: Type systems are only analogues here.
jcowan: Suppose I have a make-enumeration meta-constructor that accepts
a list of symbols and returns an enumeration-type object.
jcowan: Then I have a make-enumeration-set construction that accepts a
type object and a list of symbols and returns the set with those
symbols
in it.
alaricsp: At one level, asserting arbitrary predicates on variables
at various points in a program can be considered a type system, if
not one that's very amenable to compiler deduction (eg, inferring
types at points in the program where they're not specified, realising
that the implementation can assume useful things about values and
avoid runtime checks, etc).
alaricsp: jcowan: Yep, go on
jcowan: (The underlying implementation of a set is a bit vector,
of course)
alaricsp: Are you asking if the set a,b,c out of a,b,c,d,e,f should be
considered equal to a,b,c out of a,b,c,d,e,f,g?
jcowan: No.
jcowan: I'm asking if enum-types with equal universes should be considered
interchangeable or not.
jcowan: If yes (structural typing) then I can compare my sets with yours
as long as we agree on the universe.
alaricsp: Well, that depends on what the user wants. And different users
may want different things. You either need to provide both options,
or decide which option most users will want :-)
jcowan: If no (nominal typing) then our sets are incommensurable unless
we share the same enum-type object.
jcowan: Another way to ask it: should enum-type objects be interned?
alaricsp: Most people, I'd imagine, would want (make-set-type '(a b c))
and (make-set-type '(c b a)) to be comparable.
alaricsp: But sometimes, you do want types to be disjoint, eg for reasons
of hygiene.
Riastradh: jcowan, if you are going to the trouble of an enumeration
abstraction, I recommend the analogue of nominal typing.
Riastradh: Otherwise you might as well just use symbols, rather than
enumerands.
jcowan: The abstraction is of sets of symbols.
jcowan: So the symbols themselves are structural: you can use x1 (say)
in multiple different enum-types.
jcowan: alaricsp: What "reasons of hygiene" do you have in mind?
Riastradh: Yes, but if you are providing a context for the meaning of
the symbol, that context should mean something.
jcowan: Hmm.
alaricsp: Sometimes you want to create a type that's disjoint from
all others - for example, when annotating arbitrary third-party
data structures. One might take a network of lists of symbols and
other lists and stuff and want to annotate the lists with a set of
flags by replacing some lists l with (cons flag-set l), but if you
cannot guarantee your annotation type is distinct to everything else,
you can run into trouble
* jcowan notes that in the bit-vector implementation nominal typing
falls out naturally, whereas in the list implementation structural
typing falls out naturally.
alaricsp: (define stable-door-state-type (make-enum '(top-open
bottom-open))
alaricsp: (define big-window-state-type (make-enum '(top-open
bottom-open))
alaricsp: Stable doors (and larger windows) have independent upper and
lower 'flaps'
alaricsp: The classic case of 'type hygiene', I guess, is where one wants
to implement something like a promise so that (list? (delay
...)) and (lambda? (delay ...)) and (vector? (delay ...)) all
return false. Which is why SRFI structures are explicitly defined
as disjoint from all other types. It lets you hide the internals
of your implementations, and prevents people car-ing into things
they shouldn't.
jcowan: Yes, I'm not against nominal typing in general. I simply wonder
if it's justified in this particular case. The doors and windows
example isn't quite convincing by itself.
* alaricsp considers (make-set-type ...) and (make-disjoint-set-type
...) options
Riastradh: The nominal typing approach is less error-prone; mistakes
are more easily reported.
Riastradh: But I'm still a little unclear on your intended usage.
jcowan: I am too.
jcowan: People tend to express small finite sets by extension, and it
seems strange to say that (given sets of letters),
jcowan: {a, b, c} \union {a, e, i, o, u} might be legitimately an error
rather than {a}.
alaricsp: Yes
jcowan: Bad enough that they are incommensurate because one comes from
a universe of letters and the other from a universe of vowels,
but that can't be helped.
jcowan: But if they come from the same (in the structural sense) universe?
jcowan: Historically the advantage of structural typing is its
transparency and generality, but with constructors and Haskell views
("deconstructors") the annoyances of nominal typing are much reduced
and its safety advantages are retained.
* jcowan grumbles.
jcowan: I suppose I will go with nominal typing, then.
alaricsp: *nod*
--
John Cowan cowan at ccil.org http://ccil.org/~cowan
You cannot enter here. Go back to the abyss prepared for you! Go back!
Fall into the nothingness that awaits you and your Master. Go! --Gandalf
Received on Sun Jun 10 2007 - 19:39:04 UTC