headers
kucan | 5 Feb 1993 17:34

question about typing power of F_omega


Is a theorem of the following kind known to hold for the type system
F_omega?

	For any integer n, there is an untyped term M_n such that M_n
	is not typable in F_n, but it is typable in F_n+1.

F_n is the fragment of F_omega that allows type constructors of
order up to n.

I know that F_3 can type more than F_2 (or sometimes denoted by F),
but I couldn't find any results about higher order fragments.

I would appreciate any reference to such results.

Thanks,

--Jakov Kucan
Permalink | Reply | 0 comments |
headers
Satish Thatte | 5 Feb 1993 19:00

Re: F-bounded polymorphism and the Cardelli-Curien-Ghelli algorithm


Giorgio's comment raises a question I need to ask too:

What is known about subtyping algorithms for the *prenex fragment*
(quantifiers outermost only) of F<: in the presence of
recursive types (with or without F-bounds)?

Satish
Permalink | Reply | 5 comments |
headers
pierce | 8 Feb 1993 11:50
Picon
Picon

FOmegaSub implementation available


A prototype compiler for the typed lamba-calculus FOmegaSub -- an
extension of Cardelli and Wegner's system Fsub [1] with type operators
in the style of Fomega -- is now available by anonymous FTP.

FOmegaSub forms the basis for a series of recent reports on type
theoretic foundations for object-oriented programming [2,3,4].  The
distribution includes a graded sequence of exercises introducing the
basic concepts of the calculus -- universal polymorphism, existential
types, subtyping, and type operators -- leading up to a full treatment
of object-oriented programming and several implementations of
inheritance.  Also included in the distribution are a user's manual
and some sample input files.

The compiler is available in both source and binary form (for sun4
processors).  The sources may be recompiled on any machine running
Standard ML of New Jersey, version 93.  To retrieve the files, proceed
as follows:

    ftp ftp.dcs.ed.ac.uk                [or 129.215.160.5]
    login: anonymous
    password: <your mail address>
    cd pub/bcp
    binary			        [don't forget this!]
    get fomega.sun4.tar.Z               

The sources are in the file checkers.src.tar.Z in the same directory.

Enjoy,
(Continue reading)

Permalink | Reply | 0 comments |
headers
ma | 7 Feb 1993 03:21
Picon

an update on "Formal parametric polymorphism"


This message is an update on "Formal Parametric Polymorphism", a 
paper by Luca Cardelli, Pierre-Louis Curien, and myself, presented 
at the recent POPL conference.  I will assume some familiarity with 
the paper.

In the version of the paper in the POPL proceedings, a rule is presented 
that equates quantification over types and quantification over relations, 
(Rel Eq Forall XW).  As the paper says, this rule is a source of 
semantic difficulties.  I mentioned in my talk at POPL that Ryu Hasegawa 
had very recently found an ingenious proof of inconsistency for our 
system with the rule (Rel Eq Forall XW).  

Since POPL, we have replaced the problematic rule with a weaker one, 
then checked that this weaker rule suffices for our results.  This 
variant equates quantification over types and over relations only 
in type expressions, and not in arbitrary relation expressions as 
(Rel Eq Forall XW).  We have sketched a proof of consistency for 
the modified system, with a semantics based on the parametric PER 
model of Bainbridge, Freyd, Scedrov, and Scott.  We hope to write 
the semantics properly in the course of this year; a very brief summary 
follows. 

We would be happy to send a full, updated version of our paper to 
interested parties.  This version includes the modified system with 
many results that could not fit in the POPL abstract, as well as 
an appendix with Hasegawa's clever example.  (We intend to offer 
this paper for general ftp in a couple of months.) 

-----------------------------------------------------------------
(Continue reading)

Permalink | Reply | 0 comments |
headers
Lawrence C Paulson | 9 Feb 1993 12:58
Picon

vacancy


              U N I V E R S I T Y   O F   C A M B R I D G E

                     Department of Computer Science

                           Research Assistant

A research assistant is required to work on the project "Types for Proofs
and Programs", ESPRIT Basic Research Project 6453.  Our group is concerned
with applying and developing the generic theorem prover Isabelle.  Within
this context, the researcher will have freedom to investigate a variety of
areas: inductive data types and recursion, proof search, user interfaces,
verification, synthesis, representation of theories, etc.  Our group is
well equipped with several SPARCstations and a SPARCserver 10, all with
ample memory.

Applicants should have a sound training in theoretical computer science,
logic, or mathematics.  Previous experience with automated theorem proving
would be desirable.

The starting salary is 12,638-15,563 pounds per annum, depending upon
qualifications and experience.  The post is available from 12 March 1993
until 30 November 1993, with possible re-appointment until 31 August 1995.

Please send your application, with full curriculum vitae and the names of
two referees, to Lawrence Paulson, Computer Laboratory, University of
Cambridge, Pembroke Street, Cambridge CB2 3QG, England (Tel: 0223 334623,
Fax: 0223 334678, Internet: lcp@...).  Applications are due by 19
February 1993.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Simonetta Ronchi | 10 Feb 1993 11:29
Picon
Favicon

Re: Typing Power of F_omega


Kucan asked the following question:

>Is a theorem of the following kind known to hold for the type system
>F_omega?
>
>	For any integer n, there is an untyped term M_n such that M_n
>	is not typable in F_n, but it is typable in F_n+1.
>
>F_n is the fragment of F_omega that allows type constructors of
>order up to n.
>
>I know that F_3 can type more than F_2 (or sometimes denoted by F),
>but I couldn't find any results about higher order fragments.

I dont know the answer to this question, but, in the paper:

Giannini P., Honsell F., Ronchi Della Rocca S.,
"Type Inference: some results, some problems"

which will appear in a special issue of Fundamenta Informaticae,
we state the following CONJECTURE:

	The class of terms typable in F_n, for n>3, coincides
	with the class of terms typable in F_3.

The conjecture is motivated by the following PARTIAL RESULT:

        Let D:A|-M:a be a derivation in F_n  and let n>3. If the 
	occurrences of type variables of order >3 in D satisfy
(Continue reading)

Permalink | Reply | 0 comments |
headers
mxh | 15 Feb 1993 15:40

Non Strictly Positive Datatypes in System F


Non Strictly Positive Datatypes for Breadth First Search
--------------------------------------------------------

It is known that in system F weak initial T-algebras for any
internally describable functor exist. For example natural numbers,
lists and trees can be coded that way. However, not only these
"algebraic" datatypes exist, but also the somewhat pathological ones
whose signature contains the recursive type variable in a doubly
negated position. An example is the following datatype

datatype R = C of (R->bool)->bool

or in system F

R = All C. (((C->bool)->bool)->C) -> C

where 

bool = All C. (C->C)->C

which Reynolds and Plotkin [ReyPlo] use in their proof of the
nonexistence of set-theoretic models for system F.

It seems to be widely believed that such positive but not strictly
positive datatypes are of no real use but the construction of
counterexamples. Consequently in various approaches to adding
inductive types to F or CoC they have been ruled out [CoqMoh].

Now, however, I've found a (sort of) reasonable program making
(Continue reading)

Permalink | Reply | 0 comments |
headers
Giuseppe Castagna | 17 Feb 1993 14:15
Picon
Picon

A decidable variant of Fsub


The Fsub subtyping rule for comparing quantified types [CG92]

                E |- T1 < S1        E, X<T1 |- S2 < T2 
                --------------------------------------            (S-All-Orig)
                   E |- All(X<S1)S2 <  All(X<T1)T2 

has often been the subject of discussion in this list and elsewhere.
Although it has a natural semantic interpretation, it is responsible
for the loss of many desirable syntactic properties of the type
system: the decidability of subtyping [P92,G92a], the existence of
greatest lower bounds for compatible (i.e. lower-bounded) sets of
types [G90], the minimal typing property for the most natural
formulation of bounded existential types [GP92], etc.  Thus, it is
reasonable to look for variants of this rule better properties.

The crux of the problem is that the upper bound of the bound variable
X in S2 changes from S1 in the rule's conclusion to T1 in the
right-hand premise.  This "re-bounding" of variables is syntactically
rather bizzarre; in particular, it invalidates a whole class of useful
arguments based on structural induction on types, where the case for a
type variable normally requires applying the induction hypothesis to
its upper bound.

The weaker "equal-bounds subtyping rule" from Cardelli and Wegner's
original Fun calculus [CW85]

                          E, X<S1 |- S2 < T2 
                   -------------------------------                 (S-All-Fun)
                   E |- All(X<S1)S2 <  All(X<S1)T2
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carl Gunter | 15 Feb 1993 17:46
Picon

errata for S&T


An errata list for the first printing of my textbook "Semantics of
Programming Languages: Structures and Techniques" is now available by
anonymous ftp.  I append the instructions below.  I would appreciate
learning of any additional problems by email or other means.

				--- sincerely, carl gunter

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

To obtain corrections for the first printing of
Semantics of Programming Languages: Structures and Techniques
* Connect to ftp.cis.upenn.edu (130.91.6.8) or research.att.com (192.20.225.2).
* Login as "anonymous" with your name as password
* Go to directory pub/papers/gunter (on ftp.cis.upenn.edu) or dist/carl
  (on research.att.com);  e.g.  "cd pub/papers/carl".
* Put ftp in binary mode ("binary").
* Transfer the relevant files in that directory ("mget SPL_errata.*").
Permalink | Reply | 0 comments |
headers
ma | 19 Feb 1993 00:00
Picon

Re: A decidable variant of Fsub


Your variant of Fsub is interesting.  Your rule (S-All-New) seems 
to say that 

    All(X<S1)S2 <  All(X<T1)T2 
            iff 
    (All(X<S1)S2)* <  (All(X<T1)T2)* 

where X does not occur in S1, T1, and A* is the "Pennsylvania translation" 
of A: 

    Top*         = Top
    (A -> B)*    = A* -> B*
    (All(X<A)B)* = All(X)(X->A*)->B*

(see Breazu-Tannen et al., Information and Computation, Vol. 93,  
no. 1).

With a bit of luck this may help in settling some of your questions, 
for example in claiming that no expressive power is lost with (S-All-New). 

Regards,
        Martin Abadi
Permalink | Reply | 0 comments |

Gmane