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