Squeak and type inference

John Duncan jddst19+ at pitt.edu
Wed Oct 27 05:29:56 UTC 1999


Actually, the uniqueness in clean is:

f :: !T -> ...

but I was merely talking about the first-order logical form of
uniqueness, as in: "The Swede is protestant." Russell showed that the
gross little formula below is what we mean. There is a Swede, he is
protestant, and all protestant Swedes are him. I screwed it up below.

(E x)[Sx & Px & (y)(Sy -> x=y)]

This is a brutal modification of Fitch's system for the internet:)

As you can tell, I'm taking Logic this term.
-John

> -----Original Message-----
> From: Lex Spoon [mailto:lex at cc.gatech.edu]
> Sent: Wednesday, October 27, 1999 12:14 AM
> To: squeak at cs.uiuc.edu
> Subject: RE: Squeak and type inference
>
>
> 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