[TYPES/announce] 3WFTop proceedings: EXTENDED DEADLINE 29 Feb 2008

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

  -------------------------------------------------------------------------
    Extended Deadline: Proceedings Third Workshop on Formal Topology
  -------------------------------------------------------------------------
          Special Issue of Annals of Pure and Applied Logic
  -------------------------------------------------------------------------
  ======== EXTENDED DEADLINE ===== Friday 29 February 2008 ================
  -------------------------------------------------------------------------
          Submissions by email to: Andrej.Bauer@...
  ------------------------------------------------------------------------

The Third Workshop on Formal Topology was held in Padua in May 2007:

www.3wftop.math.unipd.it

The proceedings of this workshop will be published as a special issue of the 
Annals of Pure and Applied Logic, with the following guest editors:

Andrej Bauer, Thierry Coquand, Giovanni Sambin, Peter Schuster.

These proceedings are open for high-level research papers on topics from or 
closely related to formal topology: that is, from constructive and/or 
point-free topology including applications.

-------------------------------------------------------------------------

[TYPES/announce] Small Workshop: DEPENDENTLY TYPED PROGRAMMING

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi everybody,

it is now possible to register for the small workshop on Dependently
Typed Programming in Nottingham - see http://sneezy.cs.nott.ac.uk/ 
darcs/DTP08/

The workshop is taking place 18-20 February in Nottingham at the NCSL
conference centre. This is on campus but much nicer than the usual
student accomodation!

We have two invited speakers: Lennart Augustsson and Xavier Leroy.

For more details see the webpage: http://sneezy.cs.nott.ac.uk/darcs/ 
DTP08/

Please register soon, there is a limit of accomodation at NCSL - we  
will have
to confirm our reservation Monday, 21/1/07.

Cheers,
Thorsten

------------------------------------------------------------------------ 
---------------------------------------------------

paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Colleagues,

We are pleased to share with you a new paper about integrating
gradual typing and unification-based type inference (which
underlies the Hindley-Milner type system). This was one of
those systems where the algorithm was easy to come up
with, but the type system was somewhat tricky.

http://ece.colorado.edu/~siek/pldi08gradual.pdf

Any comments or suggests are most welcome.

The paper is under review for PLDI 2008**.

Best regards,
Jeremy Siek & Manish Vachharajani

**The review was double blind, but the reviews have already been
submitted and the identities of the authors revealed.

____________________________________
Jeremy Siek <jeremy.siek@...>
http://ece.colorado.edu/~siek/
Assistant Professor
Dept. of Electrical and Computer Engineering
University of Colorado at Boulder

Re: paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

This is a welcome work on gradual typing.

Now, please pardon me for using this thread to note something relevant to dynamic and gradual typing, which
I haven't seen said elsewhere:

Any language with a dynamic or gradual type system is necessarily either partial (potentially
non-terminating), or aparametric (admitting programs that violate the parametricity property,
described in http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html).

This is the case because a dynamically typed fragment of a program may coerce a value of unknown type to a
specific type required in a context, such as coercing x to a numeric type in x+1.

A coercion which fails may provide a means such as exception-handling or returning an appropriately typed
indicator value (such as the integer value 0) which the program can observe and act upon.  In this case, the
language is aparametric, as it allows extracting information from a value of universal type.  But
parametricity is a valuable security property in languages: a pure function with a parameter of
universally quantified type guarantees that it cannot inspect that parameter, but can only place it
somewhere in its result value.

If failed coercions always cause an unrecoverable program abort, then it's observably equivalent to any
other divergent outcome.  Hence the language doesn't necessarily violate parametricity, but it is
certainly partial.

Because gradual typing, total programming, and parametricity are all desirable features in a language, I
wanted to note that a type system can soundly support all three in the following way:

Re: paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Tim,

If you set it up carefully, it is possible to mix polymorphic functions 
with gradual typing and maintain parametricity.  Here is a paper that 
discusses the key idea in the context of contracts:

Relationally-parametric polymorphic contracts
A Guha, J Matthews, RB Findler, S Krishnamurthi - Proceedings of the 
2007 symposium on Dynamic languages, 2007 - portal.acm.org

Also look out for forthcoming papers on this topic by Jacob Matthews, 
Amal Ahmed, Robby Finder, and Philip Wadler (all together and in various 
combinations).

Cheers,  -- P

Tim Sweeney wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hello,
> 
> This is a welcome work on gradual typing.
> 
> Now, please pardon me for using this thread to note something relevant to dynamic and gradual typing,
which I haven't seen said elsewhere:
> 
> Any language with a dynamic or gradual type system is necessarily either partial (potentially
non-terminating), or aparametric (admitting programs that violate the parametricity property,

Re: paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Parametricity has indeed been a stumbling block for our work on Typed  
Scheme -- a full-fledged practical and sound implementation of  
gradual static typing for a production programming language (see POPL  
2008 for the paper, with Sam Tobin-Hochstadt). We are working with  
the rest of PLT though, and Jacob Matthews  <at>  UChicago (with Amal)  
plus others have made good progress on this:

    ESOP 2008: Parametric polymorphism through run-time sealing,
    or Theorems for low, low prices! (Jacob Matthews and Amal Ahmed)
    is probably the best citation for your purposes.

We intend to build on this for the integration of parametric  
polymorphism at module boundaries. -- Matthias

On Jan 17, 2008, at 5:40 PM, Tim Sweeney wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Hello,
>
> This is a welcome work on gradual typing.
>
> Now, please pardon me for using this thread to note something  
> relevant to dynamic and gradual typing, which I haven't seen said  
> elsewhere:
>
> Any language with a dynamic or gradual type system is necessarily  

[TYPES/announce] Midlands Graduate School 2008

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

		   Call for Participation

	Midlands Graduate School in Computer Science
                14-18 April 2008

           School of Computer Science, University of Birmingham

The Midlands Graduate School (MGS) in the Foundations of Computing
Science provides an intensive course of lectures on the Mathematical
Foundations of Computing. It has run annually since 1999, and is
hosted by the Universites of Birmingham, Leicester, and Nottingham in
rotation. The lectures are aimed at PhD students, typically in their
first or second year of study. However, the school is open to anyone
who is interested in learning more about the mathematical foundations
of computing, and all such participants are warmly welcomed. We also
very much welcome students from abroad. We gratefully acknowledge
financial support by ESPRC.

The following courses will be offered:

Basic Courses:

Category Theory (Neil Ghani, University of Nottingham)
Operational Semantics (Roy Crole, University of Leicester)
Typed Lambda Calculus (Paul Levy, University of Birmingham)

Advanced Courses:

Re: paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Tim, Matthias, Phil,

On Jan 18, 2008, at 7:54 AM, Matthias Felleisen wrote:

>
> Parametricity has indeed been a stumbling block for our work on  
> Typed Scheme -- a full-fledged practical and sound implementation  
> of gradual static typing for a production programming language (see  
> POPL 2008 for the paper, with Sam Tobin-Hochstadt). We are working  
> with the rest of PLT though, and Jacob Matthews  <at>  UChicago (with  
> Amal) plus others have made good progress on this:
>
>    ESOP 2008: Parametric polymorphism through run-time sealing,
>    or Theorems for low, low prices! (Jacob Matthews and Amal Ahmed)
>    is probably the best citation for your purposes.
>
> We intend to build on this for the integration of parametric  
> polymorphism at module boundaries. -- Matthias

Yes, I'd recommend both the above paper and the DSL 2007 paper Phil  
mentioned in the following
email.

Also, I'd like to point out a closely related issue (perhaps a  
different view on the same issue).
Casts could allow programmers to introspect on a type, thereby  
breaking parametricity.
For example, if one were allowed to write (using the notation of  

Re: paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Tim Sweeney wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hello,
> 
> This is a welcome work on gradual typing.
> 
> Now, please pardon me for using this thread to note something relevant to dynamic
> and gradual typing, which I haven't seen said elsewhere:
> 
> Any language with a dynamic or gradual type system is necessarily either partial
> (potentially non-terminating), or aparametric (admitting programs that violate
> the parametricity property, described in
> http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html).
> 
> This is the case because a dynamically typed fragment of a program may coerce a
> value of unknown type to a specific type required in a context, such as coercing
> x to a numeric type in x+1.
> 
> A coercion which fails may provide a means such as exception-handling or returning an
> appropriately typed indicator value (such as the integer value 0) which the program
> can observe and act upon.  In this case, the language is aparametric, as it allows
> extracting information from a value of universal type.  But parametricity is a valuable
> security property in languages: a pure function with a parameter of universally
> quantified type guarantees that it cannot inspect that parameter, but can only place
> it somewhere in its result value.

Parametricity is one way to achieve this security property, but it can also

Re: paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Philip Wadler wrote:
> If you set it up carefully, it is possible to mix polymorphic functions 
> with gradual typing and maintain parametricity.  
    It is also worth noting that it is possible to develop a 
generalization of the parametricity theorem that holds in languages with 
runtime type analysis, and should be applicable to languages with adhoc 
polymorphism and other sorts of dynamic type tests. 

In the polymorphic lambda-calculus, no expression is allowed to depend 
upon how an abstract type may be instantiated.  The first key insight is 
that this property is merely one end of a spectrum.  At the other end of 
the spectrum, any expression in a term may depend on the instantiation 
of any possible abstract type.  In between, some expressions may be 
depend on the instantiation of some abstract types.  I expect most 
programs using runtime type analysis, etc. fall somewhere in this part 
of the spectrum.

The second key insight is that in the polymorphic lambda-calculus this 
dependency relationship (or rather the lack of dependency) is implicit.  
Therefore, if we augment the type system to make it possible to express 
the dependencies between abstract types and expressions explicitly, it 
is possible to reason about these other points in the spectrum.  
Information-flow type systems are an example of a class of type systems 
that makes dependencies between expressions explicit by labeling types.  
Therefore, one way that the dependencies could be made explicit is to 
augment the type system of the polymorphic lambda-calculus with 
information-flow labels on both types and kinds.