Squeak and type inference
Lex Spoon
lex at cc.gatech.edu
Wed Oct 27 00:14:12 UTC 1999
Oh, I missed the "uniquely quantified" part of your query. It's not
mentioned in the Cardelli and Wegner paper I cited, so it's more than I
know anything about :)
> Tx = x is a Type
> Px = (predicate)
> (E x)[Tx & (y)(Ty&Py -> x=y)]
Yikes! This is the definition of a uniquely quantified type? Is (y)
the same as "for all y" ?
Especially after looking at things like this, it would seem that the
prettiest syntax of all is when you don't have to write something down
at all :) Types for optimizations inside a compiler--fine. Types for
doing formal proofs of correctness--fine. Types just because people
want to make programming more of a challenge--bonkers.
Lex
>
> :) John
>
>
> > -----Original Message-----
> > From: Lex Spoon [mailto:lex at cc.gatech.edu]
> > Sent: Wednesday, October 27, 1999 12:12 AM
> > To: squeak at cs.uiuc.edu
> > Subject: Re: Squeak and type inference
> >
> >
> > Heheh, this is straight off the qualifying exam I'm taking in
> > a couple of weeks! Have you read the excellent summary by
> > Cardelli and Wegner?
> >
> > Luca Cardelli and Peter Wegner. "On Understanding Types,
> > Data Abstraction, and Polymorphism". ACM Computing Surveys 1985.
> >
> >
> > My understanding is that universally quantified types
> > are just about the same as parameterized types. Thus, a
> > C++ template is a universally quantified type, eg Stack is
> > universally quantified, while Stack<integer> is an instatiation
> > of that type and is *not* universally quantified.
> >
> > To give a non-C++ example, consider the function identity:
> >
> > fun identity(x) = x
> >
> > It's type is "Forall[a] a->a", that is, "for any type a,
> > a function mapping an a to an a
> >
> > Before you can use a univ. quantified item, you must instantiate
> > it like this:
> >
> > int_identity = identity[int]
> >
> > Now int_identity is a version of the generic identity which only
> > accepts int's. The type of int_identity is simply int->int.
> >
> >
> > Existential types I'm not so clear on myself, sorry. Their
> > *purpose*
> > is to define packages which can hide implementation details. The
> > type of a package would be an existential type; you are only allowed
> > to take advantage of features of the package declared in
> > the existential
> > type, even if the package has more features hidden inside.
> >
> > However, I'm not real clear on how the details work which implement
> > this purpose..... Hopefully it will become clear by the
> > time I take my
> > exam :)
> >
> > Really, *most* of this type theory stuff is quite simple if you
> > know how to program. But there's a significant overhead in learning
> > to wade through all the symbols!
> >
> >
> > Lex
> >
> >
> > PS -- I've been reading comp.lang.functional lately, and it sure
> > is nice not to have to worry about all these wierd kinds of types
> > when programming in Smalltalk. In programming Smalltalk, types
> > are usually more like "this is a dictionary-like
> > thing"--things that,
> > for good and ill, computers and mathematicians cannot deal with :)
> >
> >
> >
> > >
> > > Perhaps you have read enough to help me understand uniquely,
> > > existentially and universally quantified types. That is one major
> > > aspect of type calculus that I am having trouble with, but which
> > > appears to show much potential for both genericity and efficiency.
> > >
> > > -John
> > >
> >
> >
More information about the Squeak-dev
mailing list
|