[PRL] Type question...

Mitchell Wand wand at ccs.neu.edu
Mon Oct 8 12:53:18 EDT 2007


There were papers in the last two Erlang workshops.  The first one made it
to LtU.  --Mitch

On 10/8/07, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
>
> On Oct 8, 2007, at 12:18 PM, Mitchell Wand wrote:
>
> > OTOH, the Erlang community seems to be moving in the other
> > direction.  They have a notion of "success typing" that says
> > roughly, if the computation succeeds, then some property holds.  As
> > near as I can tell, this seems to confuse typing with flow
> > analysis. (Somebody here should probably write a oaper sorting all
> > this out.)
>
>
> We definitely need to check this out, because our upcoming POPL paper
> on Typed Scheme is also using flow-oriented reasoning to supplement
> the logic of (union, sub, poly) types. Any pointers? -- Matthias
>
>
>
> >
> > --Mitch
> >
> > On 10/8/07, Riccardo Pucella <riccardo at ccs.neu.edu> wrote:
> > >
> > > Pascal used to assign types to this kind of program :-)
> > > (not quite the (f f n) part) and I bet you can still get
> > > it thru the C type checker but I assume you mean "sound"
> > > type system (and so did everyone else who responded).
> >
> > If only because C has only a notion of a function type that does
> > not specify what the functions args and return types are. (At least
> > to a first approximation.)
> >
> > >
> > > I wish regular programmers could distinguish these
> > > two kinds of systems.
> >
> > I like to think of the distinction as between type systems that are
> > used to make sure you do not use values wrongly (sound type
> > systems), versus type systems that are used for conveying
> > representation information - and the latter is definitely what is
> > going on in C.
> >
> >
> > >
> > > Why don't you post this kind of question on a forum
> > > where you can evaluate the reactions of regular
> > > programmers. I wonder how much this idea of 'safety'
> > > has sunk in (and what this says about PL education
> > > at the undergraduate level. I used to cover Type
> > > Soundness in "311" aka "660". I doubt it is still
> > > mentioned.)
> >
> > I think Java has helped in that regard - at least for the average
> > programmer. They may not be able to put it into words that crisply,
> > but they have much more of a sense of soundness than the C
> > programmers (or Pascal programmers) of yore.
> >
> >
> > Cheers,
> > R
> >
> >
> > _______________________________________________
> > PRL mailing list
> > PRL at lists.ccs.neu.edu
> > https://lists.ccs.neu.edu/bin/listinfo/prl
> >
> >
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the PRL mailing list