Karl Crary | 11 Aug 20:45 2008
Picon

[TYPES/announce] WMM'08 call for participation

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

Apologies for the cross-posting.

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

                        CALL FOR PARTICIPATION

                  3rd Informal ACM SIGPLAN Workshop
                      on Mechanizing Metatheory

               http://www.seas.upenn.edu/~sweirich/wmm/

                      Victoria, British Columbia
                          September 20, 2008

                      Co-located with ICFP 2008.

Researchers in programming languages have long felt the need for tools
to help formalize and check their work. With advances in language
technology demanding deep understanding of ever larger and more
complex languages, this need has become urgent. There are a number of
automated proof assistants being developed within the theorem proving
community that seem ready or nearly ready to be applied in this domain
-- yet, despite numerous individual efforts in this direction, the use
of proof assistants in programming language research is still not
commonplace: the available tools are confusingly diverse, difficult to
learn, inadequately documented, and lacking in specific library
facilities required for work in programming languages.
(Continue reading)

Brian Hulley | 26 Aug 03:55 2008

Typing extensible records without row variables?

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

Hi,
Many of the papers I've read that deal with the typing of extensible 
records use the concept of "row variables" ([1] [2] [3] [4]). Therefore 
if we use the syntax(*):

     'val r = {[title = "Duma"] [genre = Drama]}

to bind a record with 2 fields to (r) and

     {[certificate = U] :: r}

to denote the extension of (r) by a new field, with row variables the 
extension operator has type:

     {[_ : _] :: _} :
         'forall (l : LABEL) (t : *) (r : ROW) .
             Lab[l] -> t -> Rec[r] -> Rec{| [l : t] :: r |}

where {| [l : t] :: r |} denotes the row r extended by the label/type 
association, and (Rec) is a built-in type constructor of kind (ROW -> 
*). (Curried application is denoted by glued square brackets which can 
be omitted if the argument is itself a bracketed form, and keywords 
always start with a prime.)
For brevity the above can be written:

     {[_ : _] :: _} :
         Lab[l] t Rec[r] -> Rec{| [l : t] :: r |}
             | [l : LABEL] [t : *] [r : ROW]
(Continue reading)

Matthias Blume | 26 Aug 05:40 2008

Re: Typing extensible records without row variables?

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

On Aug 25, 2008, at 8:55 PM, Brian Hulley wrote:

> 3) While it is obviously useful to have extensible records it is not  
> at
> all clear to me whether or not extensible variants are similarly  
> useful
> since there are other ways of achieving extensiblility in functional
> programming e.g. by adding new combinators to a combinator library and
> keeping the underlying representation variant completely hidden.

In our ICFP'06 paper[*] we suggest that extensible variants (actually:  
extensible cases)
might be a useful programming concept that integrates gracefully into  
an ML-
(or Haskell-) like language after all.

ou might also be interested in having a look at our upcoming APLAS  
paper[**],
where we point out that the same idea not only straightforwardly  
extends to the
typing of exceptions (a fact that has been exploited several times in  
previous work
on exception analysis by other authors), but also can be taken as a  
starting point
for a language design that (a) rules out any uncaught exceptions, and  
(b) integrates
well with the notion of extensible records and cases.

(Continue reading)

Brian Hulley | 26 Aug 14:48 2008

Re: Typing extensible records without row variables?

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

Matthias Blume wrote:
> 
> On Aug 25, 2008, at 8:55 PM, Brian Hulley wrote:
> 
>> 3) While it is obviously useful to have extensible records it is not at
>> all clear to me whether or not extensible variants are similarly useful
>> since there are other ways of achieving extensiblility in functional
>> programming e.g. by adding new combinators to a combinator library and
>> keeping the underlying representation variant completely hidden.
> 
> In our ICFP'06 paper[*] we suggest that extensible variants (actually: 
> extensible cases) might be a useful programming concept that integrates
>  gracefully into an ML- (or Haskell-) like language after all.

Thanks - I found the above useful especially for the way extensible 
variants are given meaning at the term level by splitting the usual case 
construct into match + cases and making the cases part the first class 
dual of extensible records. Also of special interest is the fact that 
the "lacks" predicates of various other papers I'd read are directly 
incorporated into the kind of the row variable so that everything is 
dealt with in the same place instead of being represented by a special 
kind *and* a special predicate, and of course the details of how all 
this is implemented efficiently, and some other points too.

In terms of integration, if these variants are to replace the normal 
non-extensible datatype variants of ML/Haskell, there is still (afaics) 
the issue of syntactic convenience vs theoretical completeness of the 
duality due to the fact that the extensible variant constructors must 
(Continue reading)


Gmane