From Giuseppe.Castagna at ens.fr  Wed Jan  4 16:22:10 2006
From: Giuseppe.Castagna at ens.fr (Giuseppe Castagna)
Date: Wed, 04 Jan 2006 22:22:10 +0100
Subject: [TYPES] Limited use of negation types?
In-Reply-To: <43AC14F9.4070800@inria.fr>
References: <43AB49BD.6030507@freeshell.org> <43AC14F9.4070800@inria.fr>
Message-ID: <43BC3C82.9040302@ens.fr>

Alain Frisch wrote:
 > I'm pretty sure this is not what you have in mind, but my LICS 2002
 > paper _Semantic Subtyping_ describes a type system with a classical
 > (set-theoretic interpretation) of negation types. The negation of (t ->
 > s) is just the set of values which are not of type (t -> s), where the
 > type of an abstraction is explicitly given in its prototype (and cannot
 > change during evaluation).
 >
 > http://www.cduce.org/papers/lics02.ps.gz
 >
 > The paper is rather dense. Let me know if you want more information.
 >
 > -- Alain

If you want less a dense paper, actually an introduction to the paper Alain 
cited above, you can check one of this year's ICALP/PPDP joint invited talks:

A Gentle Introduction to Semantic Subtyping

by Alain and myself and included in the PPDP 2005 proceedings. You can also find 
it here.

http://www.di.ens.fr/users/castagna/papers/icalp-ppdp05.pdf

Cheers

---Beppe---

From paramr at gmail.com  Sat Jan  7 00:50:13 2006
From: paramr at gmail.com (Param Jyothi Reddy)
Date: Fri, 6 Jan 2006 21:50:13 -0800
Subject: [TYPES] A doubt in AUTOMATH type system
Message-ID: <fe0f45360601062150q2e1ede19u9309f861586d62d7@mail.gmail.com>

Hi,
I am trying to understand how automath lines could be interpreted in
PTS. in this regard i got stuck at the following. Any help would be
appreciated.

Can someone help me understand the meaning of p:PROP in the following Line:
@[sigma:TYPE][p:[x:sigma]PROP]
l_all:=p:PROP

in the paramters we have said that p:[x:Sigma]PROP. So how can p be
type fo PROP.

It is used as follows:
@[sigma:TYPE][p:[x:sigma]PROP][a1:l_all(sigma,p)][s:sigma]
l_alle:=<s>a1:<s>p

If i interpret paramters in definition of l_all as lambda then
l_all(sigma, p) reduces to p hence disallowing a1 : l_all(sigma, p).
Interpreting paramters as product is not possible because the body is
not correctly typed.

Regards,
Param

From svb at doc.ic.ac.uk  Thu Jan 12 10:57:49 2006
From: svb at doc.ic.ac.uk (Steffen van Bakel)
Date: Thu, 12 Jan 2006 15:57:49 +0000
Subject: [TYPES] Electronic publications
Message-ID: <1137081469.43c67c7da0d7e@www.doc.ic.ac.uk>

Sir,
I hope you would post the next message on the types list.

Hi,

I was wondering if any of you of an alternative to ENTCS to get
workshop proceedings published.  Elsevier has managed to antagonise
many of us, and I was kind of hoping some other medium would exist.

Many thanks,
Steffen van Bakel 

From jbw at macs.hw.ac.uk  Fri Jan 13 06:56:39 2006
From: jbw at macs.hw.ac.uk (Joe Wells)
Date: Fri, 13 Jan 2006 11:56:39 +0000
Subject: [TYPES] Electronic publications
In-Reply-To: <1137081469.43c67c7da0d7e@www.doc.ic.ac.uk> (Steffen van Bakel's
	message of "Thu, 12 Jan 2006 15:57:49 +0000")
References: <1137081469.43c67c7da0d7e@www.doc.ic.ac.uk>
Message-ID: <87fynsjq88.fsf@colinux.macs.hw.ac.uk>

Steffen van Bakel <svb at doc.ic.ac.uk> writes:

> I was wondering if any of you of an alternative to ENTCS to get
> workshop proceedings published.  Elsevier has managed to antagonise
> many of us, and I was kind of hoping some other medium would exist.

You could try BCS's eWIC (electronic workshops in computing) series.
I have only heard of this, so I don't know if it is any better.

-- 
Joe

From gopalan at cs.umn.edu  Mon Jan 23 00:37:04 2006
From: gopalan at cs.umn.edu (Gopalan Nadathur)
Date: Sun, 22 Jan 2006 23:37:04 -0600
Subject: [TYPES] Electronic publications
In-Reply-To: <1137081469.43c67c7da0d7e@www.doc.ic.ac.uk>
References: <1137081469.43c67c7da0d7e@www.doc.ic.ac.uk>
Message-ID: <43D46B80.7030406@cs.umn.edu>

> I was wondering if any of you of an alternative to ENTCS to get
> workshop proceedings published.  Elsevier has managed to antagonise
> many of us, and I was kind of hoping some other medium would exist.


I would like to suggest using CoRR, the Computing Research Repository 
for this purpose. You will find more information about this repository at

http://arxiv.org/corr/home.

This repository is here to stay and hence your proceedings will have an 
archival quality while still allowing you to keep the informal feel to 
papers from a workshop. Some time ago, Professor Mirek Truszczynski put 
together instructions for creating proceedings within the structure of 
CoRR. You will find these instructions at

http://www.cs.kuleuven.ac.be/~dtai/projects/ALP/electronic_publishing.html.

I believe that these instructions are still accurate. Based on the fact 
that your query is addressed to types, I think that the Programming 
Languages area or the Logic in Computer Science area may be the likely 
candidates for your proceedings. There are, of course, a wide variety of 
choices as should become clear from looking at the welcome page for the 
repository.

Cheers,
-Gopalan Nadathur

From eijiro.sumii at gmail.com  Tue Jan 24 19:17:19 2006
From: eijiro.sumii at gmail.com (Eijiro Sumii)
Date: Wed, 25 Jan 2006 09:17:19 +0900
Subject: [TYPES] logical relations
Message-ID: <a4d0794e0601241617v133f1cb3nde6681afe091fd71@mail.gmail.com>

Hello,

I am trying to find who coined the term "logical relations" and the
names "fundamental/main/basic theorem/lemma" (or any combination of
them) for what reason.  I tried to read the original papers, but some
(many?) of them are not quite easy to obtain now...  Does anybody
know?

Thanks,

        Eijiro

From nick at microsoft.com  Wed Jan 25 04:35:09 2006
From: nick at microsoft.com (Nick Benton)
Date: Wed, 25 Jan 2006 01:35:09 -0800
Subject: [TYPES] logical relations
Message-ID: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>

Gordon Plotkin "Lambda definability and logical relations" 1973, I
think.

  Nick

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu
[mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Eijiro
Sumii
Sent: 25 January 2006 00:17
To: types at cis.upenn.edu
Cc: sumii at ecei.tohoku.ac.jp
Subject: [TYPES] logical relations

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

Hello,

I am trying to find who coined the term "logical relations" and the
names "fundamental/main/basic theorem/lemma" (or any combination of
them) for what reason.  I tried to read the original papers, but some
(many?) of them are not quite easy to obtain now...  Does anybody
know?

Thanks,

        Eijiro

From geoffw at cis.upenn.edu  Wed Jan 25 14:16:24 2006
From: geoffw at cis.upenn.edu (Geoffrey Alan Washburn)
Date: Wed, 25 Jan 2006 14:16:24 -0500
Subject: [TYPES] logical relations
In-Reply-To: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>
References: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>
Message-ID: <43D7CE88.7020707@cis.upenn.edu>

Nick Benton wrote:
> Gordon Plotkin "Lambda definability and logical relations" 1973, I
> think.
>   

    As far as I have been able to determine, this particular paper is an 
Edinburgh technical report that does not currently exist in a digital 
form.  What would be the best to obtain a copy of  this document?  Is 
there a revised version that was published in a journal?

-- 
[Geoff Washburn|geoffw at cis.upenn.edu|http://www.cis.upenn.edu/~geoffw/]


From naumann at cs.stevens.edu  Wed Jan 25 16:55:06 2006
From: naumann at cs.stevens.edu (David Naumann)
Date: Wed, 25 Jan 2006 16:55:06 -0500 (EST)
Subject: [TYPES] logical relations
In-Reply-To: <43D7CE88.7020707@cis.upenn.edu>
References: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>
	<43D7CE88.7020707@cis.upenn.edu>
Message-ID: <Pine.NEB.4.64.0601251654380.23793@eylenbosch.cs.stevens-tech.edu>

I believe a later version is "Lambda-definability in the full type
hierarchy", in the Curry Festschrift (Seldin and Hindley, eds, 1980).

My copy was obtained by a quaint ritual involving Xerox and the climbing 
of stairs in a large building.


On Wed, 25 Jan 2006, Geoffrey Alan Washburn wrote:

> Date: Wed, 25 Jan 2006 14:16:24 -0500
> From: Geoffrey Alan Washburn <geoffw at cis.upenn.edu>
> To: Nick Benton <nick at microsoft.com>
> Cc: sumii at ecei.tohoku.ac.jp, types at cis.upenn.edu,
>     Eijiro Sumii <eijiro.sumii at gmail.com>
> Subject: Re: [TYPES] logical relations
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Nick Benton wrote:
>> Gordon Plotkin "Lambda definability and logical relations" 1973, I
>> think.
>>
>
>    As far as I have been able to determine, this particular paper is an
> Edinburgh technical report that does not currently exist in a digital
> form.  What would be the best to obtain a copy of  this document?  Is
> there a revised version that was published in a journal?
>
> -- 
> [Geoff Washburn|geoffw at cis.upenn.edu|http://www.cis.upenn.edu/~geoffw/]
>



From eijiro.sumii at gmail.com  Thu Jan 26 00:11:01 2006
From: eijiro.sumii at gmail.com (Eijiro Sumii)
Date: Thu, 26 Jan 2006 14:11:01 +0900
Subject: [TYPES] logical relations
In-Reply-To: <Pine.NEB.4.64.0601251654380.23793@eylenbosch.cs.stevens-tech.edu>
References: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>
	<43D7CE88.7020707@cis.upenn.edu>
	<Pine.NEB.4.64.0601251654380.23793@eylenbosch.cs.stevens-tech.edu>
Message-ID: <a4d0794e0601252111r38e0b9eap769520caf8f8294f@mail.gmail.com>

Dear all,

Thank you very much for all the replies (both private and public). 
Many of them have pointed out the lambda-definability papers by
Plotkin.  I managed to get a copy of the one in Curry Festschrift
(thanks to my colleagues).

HOWEVER, according to my quick "eye grep" of this paper, it does not
seem to contain the words "logical relations" nor
"main/basic/fundamental lemma/theorem" anywhere, so I still do not
know the answer to the "for what reason" part of my question.  Perhaps
I should try harder to get the 1973 tech report (as well as other
original papers by Tait and Statman).

By the way, there was also a similar question back in 1988 in Types

  http://www.seas.upenn.edu/~sweirich/types/archive/1988/msg00052.html

and a reply by Prof. John Mitchell

  http://www.seas.upenn.edu/~sweirich/types/archive/1988/msg00061.html

but even he does not seem to have known a clear answer...!

        Eijiro

P.S.  A few people asked me why I am asking.  The primary reason is my
own curiosity, but this time my question was also inpired by a student
who loves to know.

From U.Reddy at cs.bham.ac.uk  Thu Jan 26 04:50:55 2006
From: U.Reddy at cs.bham.ac.uk (Uday Reddy)
Date: Thu, 26 Jan 2006 09:50:55 +0000
Subject: [TYPES] logical relations
In-Reply-To: <a4d0794e0601252111r38e0b9eap769520caf8f8294f@mail.gmail.com>
References: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>
	<43D7CE88.7020707@cis.upenn.edu>
	<Pine.NEB.4.64.0601251654380.23793@eylenbosch.cs.stevens-tech.edu>
	<a4d0794e0601252111r38e0b9eap769520caf8f8294f@mail.gmail.com>
Message-ID: <17368.39807.213604.722229@gromit.cs.bham.ac.uk>

Eijiro Sumii writes:

> HOWEVER, according to my quick "eye grep" of this paper, it does not
> seem to contain the words "logical relations" nor
> "main/basic/fundamental lemma/theorem" anywhere, so I still do not
> know the answer to the "for what reason" part of my question.

Here is my guess as to "for what reason":

The correspondence between type systems and logics has been known
since Curry's time.  Since logical relations are built using that
correspondence (times as conjunction, -> as implication and so on.)
it was appropriate to call them "logical" relations, i.e., families of
relations obtained by treating type constructors as logical connectives.

Claudio Hermida tried to squeeze out this correspondence more formally
and succeeded to a large degree:

@PhDThesis(Hermida-thesis,
        Author = "Hermida, C.",
        Title = "Fibrations, Logical Predicates and Indeterminantes",
        School = "Aarhus University",
        Year = "1993"
        )

Cheers,
Uday

From jeffrey.sarnat at yale.edu  Thu Jan 26 05:05:55 2006
From: jeffrey.sarnat at yale.edu (Jeffrey Sarnat)
Date: Thu, 26 Jan 2006 05:05:55 -0500 (EST)
Subject: [TYPES] logical relations
In-Reply-To: <a4d0794e0601252111r38e0b9eap769520caf8f8294f@mail.gmail.com>
References: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>
	<43D7CE88.7020707@cis.upenn.edu>
	<Pine.NEB.4.64.0601251654380.23793@eylenbosch.cs.stevens-tech.edu>
	<a4d0794e0601252111r38e0b9eap769520caf8f8294f@mail.gmail.com>
Message-ID: <Pine.LNX.4.63.0601260423320.607@ajax.its.yale.edu>

A little bit of further digging reveals this message, which seems to 
confirm the "Gordon Plotkin coined the term" hypothesis:

http://www.seas.upenn.edu/~sweirich/types/archive/1989/msg00047.html

I've never seen the technical report he's referring to either, but you can 
count me among the people who would love to get their hands on a copy of 
it.

Also, Statman's 1985 Information and Control paper makes use of the term 
"fundamental theorem of logical relations," although I can't say if he's 
the first to give it a name. His notation is somewhat nonstandard (for me 
at least), but it's a fun paper nonetheless.

As far as I can tell, the first use of the concept of a logical relation 
is usually attributed to Tait's 1967 JSL paper "Intensional interpretation 
of functionals of finite type I." You can actually get an electronic copy 
of this paper (and pretty much every other JSL paper, as far as I know) 
through jstor, but the writing is pretty dense. There are numerous other 
papers that make essential use of logical relations (including Girard's 
original reducibility candidates proof) in the "Proceedings of the Second 
Scandinavian Logic Symposium" (published in 1971), but as far as I can 
remember they all use terminology to the effect of "computability 
predicate" and "reducibility candidate" and do not give a special name for 
the main/fundamental/basic lemma/theorem.

 	Jeff

On Thu, 26 Jan 2006, Eijiro Sumii wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> Thank you very much for all the replies (both private and public).
> Many of them have pointed out the lambda-definability papers by
> Plotkin.  I managed to get a copy of the one in Curry Festschrift
> (thanks to my colleagues).
>
> HOWEVER, according to my quick "eye grep" of this paper, it does not
> seem to contain the words "logical relations" nor
> "main/basic/fundamental lemma/theorem" anywhere, so I still do not
> know the answer to the "for what reason" part of my question.  Perhaps
> I should try harder to get the 1973 tech report (as well as other
> original papers by Tait and Statman).
>
> By the way, there was also a similar question back in 1988 in Types
>
>  http://www.seas.upenn.edu/~sweirich/types/archive/1988/msg00052.html
>
> and a reply by Prof. John Mitchell
>
>  http://www.seas.upenn.edu/~sweirich/types/archive/1988/msg00061.html
>
> but even he does not seem to have known a clear answer...!
>
>        Eijiro
>
> P.S.  A few people asked me why I am asking.  The primary reason is my
> own curiosity, but this time my question was also inpired by a student
> who loves to know.
>

From streicher at mathematik.tu-darmstadt.de  Thu Jan 26 07:40:59 2006
From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher)
Date: Thu, 26 Jan 2006 13:40:59 +0100 (CET)
Subject: [TYPES] logical relations
Message-ID: <200601261240.k0QCexj3016707@fb04209.mathematik.tu-darmstadt.de>

I don't know who used which term first. But a logical relations technique
was first used by W.Tait in his proof for strong normalisation for the
typed \lambda-calculus. It was a unary logical relation, i.e. a 
"logical predicate". I guess this this the source for the term "logical".

Another source is Laeuchli's paper from 1970 who proved for Set^Z (i.e. sets
with an iso and equivariant maps between them) that all interpretations of
proofs are premutation invariant. He used this for showing that all 
interpretations of a type are inhabited iff there is a proof for the
corresponding proposition.

As I heard by rumour Lauchli's result inspired Gordon Plotkin to introduce
an appropriate generalisation of permutation-invariance, namely logical
realtions, for characterising \lambda definability. He din't f ully succeed.
Much later there was a paper by Jung & Tiuryn (TLCA 1993) where using Kripke
logical relations they finally arrived at this goal.

I think the "fundamental lemma" is called the  "fundamental lemma" because
it tells you the fundamental fact about logical relations namely that
syntactically definable elements are invariant under every logical relation
under which that constants are invariant. "Invariance Lemma" might be a more
telling name but history decided otherwise.

Thomas Streicher

From james.cheney at gmail.com  Thu Jan 26 08:47:16 2006
From: james.cheney at gmail.com (James Cheney)
Date: Thu, 26 Jan 2006 13:47:16 +0000
Subject: [TYPES] logical relations
In-Reply-To: <43D7CE88.7020707@cis.upenn.edu>
References: <2967212019EB7B4D990E06E1AC2F23190632A008@RED-MSG-60.redmond.corp.microsoft.com>
	<43D7CE88.7020707@cis.upenn.edu>
Message-ID: <814253dd0601260547l6a954472xe40f83f1e48b5ac5@mail.gmail.com>

On 1/25/06, Geoffrey Alan Washburn <geoffw at cis.upenn.edu> wrote:
>
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
> Nick Benton wrote:
> > Gordon Plotkin "Lambda definability and logical relations" 1973, I
> > think.
> >
>
>     As far as I have been able to determine, this particular paper is an
> Edinburgh technical report that does not currently exist in a digital
> form.  What would be the best to obtain a copy of  this document?  Is
> there a revised version that was published in a journal?
>


This doesn't immediately help, but the Edinburgh University Library is
planning on scanning all of its CS/AI technical reports (including ones
damaged/lost in the 2002 South Bridge fire for which replacements are
available).  So at some point in the not too distant future the above report
should be available online.

--James

From coquand at cs.chalmers.se  Thu Jan 26 09:50:33 2006
From: coquand at cs.chalmers.se (Coquand)
Date: Thu, 26 Jan 2006 15:50:33 +0100 (CET)
Subject: [TYPES] logical relations
Message-ID: <63845.129.16.224.206.1138287033.squirrel@webmail.chalmers.se>

 As a complement to the reference to Tait's 1967 article, one can add
the paper
(from notes of a course by Statman, 1985)

 R. Gandy
 On the axiom of extensionality, part I
 Journal of Symbolic Logic, 36-48, 1956

which gives an interpretion of extensional type theory in intensional
type theory using logical relations (the extensional equality being
defined for higher types by induction).

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

 A similar question: who introduced first the term "computational
adequacy theorem" for Theorem 3.1 of the "LCF considered as a programming
language" paper??

               Thierry Coquand



From rwh at cs.cmu.edu  Thu Jan 26 12:01:20 2006
From: rwh at cs.cmu.edu (Robert Harper)
Date: Thu, 26 Jan 2006 12:01:20 -0500
Subject: [TYPES] logical relations
In-Reply-To: <a4d0794e0601241617v133f1cb3nde6681afe091fd71@mail.gmail.com>
References: <a4d0794e0601241617v133f1cb3nde6681afe091fd71@mail.gmail.com>
Message-ID: <E2B7B529-2E01-4157-9C7E-D41EDF5E96FC@cs.cmu.edu>

I asked Rick Statman about this, here is his reply:

Actually, the phrase "logical relations" comes from Mike Gordon.
It was told to me by Gordon Plotkin in 1974 who heard it from Mike.
I coined the phrase "fundamental theorem".
I thought the the phrase "logical realtion" was appropriate since
these relations are closed under the logical operations (suitably
defined).

Bob Harper

On Jan 24, 2006, at 7:17 PM, Eijiro Sumii wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Hello,
>
> I am trying to find who coined the term "logical relations" and the
> names "fundamental/main/basic theorem/lemma" (or any combination of
> them) for what reason.  I tried to read the original papers, but some
> (many?) of them are not quite easy to obtain now...  Does anybody
> know?
>
> Thanks,
>
>         Eijiro


From dts at inf.ed.ac.uk  Mon Jan 30 10:15:58 2006
From: dts at inf.ed.ac.uk (Don Sannella)
Date: Mon, 30 Jan 2006 15:15:58 +0000
Subject: [TYPES] logical relations
Message-ID: <17374.11694.16719.649756@lambieletham.inf.ed.ac.uk>

On Thu, 26 Jan 2006 11:13:07 +0000, Uday Reddy wrote:
 > The correspondence between type systems and logics has been known
 > since Curry's time.  Since logical relations are built using that
 > correspondence (times as conjunction, -> as implication and so on.)
 > it was appropriate to call them "logical" relations, i.e., families of
 > relations obtained by treating type constructors as logical connectives.
 >
 > Claudio Hermida tried to squeeze out this correspondence more formally
 > and succeeded to a large degree:
 >
 > @PhDThesis(Hermida-thesis,
 >         Author = "Hermida, C.",
 >         Title = "Fibrations, Logical Predicates and Indeterminantes",
 >         School = "Aarhus University",
 >         Year = "1993"
 >         )

Correction: Edinburgh University.

While I'm here, an advertisement: people who are interested
in logical relations might like to have a look at a variant
called "prelogical relations" which have most of the useful
properties of logical relations, including the basic lemma,
but which compose, unlike logical relations.  See

@article{prelogical-relations,
	author = {Furio Honsell and Donald Sannella},
	title = {Prelogical Relations},
	journal={Information and Computation},
	year = {2002},
	volume = {178},
	pages = {23--43},
	pdf = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel-long.pdf}}

(Shorter version in Proc. CSL 1999.)  A categorical version of the
same thing is

@inproceedings{lax-logical-relations,
	author = {Gordon Plotkin and John Power
                 and Donald Sannella and Robert Tennent},
	title = {Lax Logical Relations},
	booktitle = {Proc.\ 27th Intl.\ Colloq.\ on Automata,
                 Languages and Programming},
	location = {Geneva},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	volume = 1853,
	pages = {85--102},
	year = 2000,
	pdf = {http://homepages.inf.ed.ac.uk/dts/pub/laxlogrel.pdf}}

Don Sannella

From eijiro.sumii at gmail.com  Wed Feb  1 06:35:30 2006
From: eijiro.sumii at gmail.com (Eijiro Sumii)
Date: Wed, 1 Feb 2006 20:35:30 +0900
Subject: [TYPES] logical relations
In-Reply-To: <17374.11694.16719.649756@lambieletham.inf.ed.ac.uk>
References: <17374.11694.16719.649756@lambieletham.inf.ed.ac.uk>
Message-ID: <a4d0794e0602010335m7f472771t5d44a4782213cf5f@mail.gmail.com>

Dear all,

Thanks again for the responses - I have received a private message
from Prof. Gordon Plotkin (thanks to Phil) and he confirms that the
_idea_ (using relations) was suggested to him by Mike Gordon but the
_name_ ("logical relations") was his.

Of course, as many people pointed out, this idea itself can be tracked
back much further, but that would be another (much longer) story...!

        Eijiro

From m.a.smith at eris.qinetiq.com  Wed Mar  8 05:47:15 2006
From: m.a.smith at eris.qinetiq.com (Michael Anthony Smith)
Date: Wed, 08 Mar 2006 10:47:15 +0000
Subject: [TYPES] Query: Types for post-development analysis?
Message-ID: <440EB633.9000604@eris.qinetiq.com>

I have been a (silent) member of the types list for several years, as I 
am interested in monitoring (and hopefully using) developments in type 
theory. I certainly make use of (reasonably) strongly types 
specification and programming languages in my work, which is regularly 
involving the analysis of third party designs/code. Within this context 
it is often hard to use developments in the type-theory, as they appear 
(at least to me) to be aimed at designing solid development languages 
and frameworks.

I know that type systems are used to design languages (and frameworks) 
that have a given collection of desirable properties, whether this be 
the traditional "shape" correctness or for some other concern such as 
guaranteeing various concurrency or security properties. I also am aware 
of the link between type theories and abstract interpretation. What I 
was wondering if anyone here knows of the application of type theories 
to the post-development analysis context?

Thanks,

Anthony.



From m.a.smith at eris.qinetiq.com  Thu Mar  9 05:20:57 2006
From: m.a.smith at eris.qinetiq.com (Michael Anthony Smith)
Date: Thu, 09 Mar 2006 10:20:57 +0000
Subject: [TYPES] Query: Types for post-development analysis?
In-Reply-To: <440EB633.9000604@eris.qinetiq.com>
References: <440EB633.9000604@eris.qinetiq.com>
Message-ID: <44100189.7070808@eris.qinetiq.com>

Clarification and Summary (so far)

I have already had several useful replies to this original posting 
(thanks). But, from some of these replies it is clear that it is worth 
clarifying my use of the "post-development analysis context", thus I am 
enclosing a description that I sent individually to one of the list members.

By "the post-development analysis context" I mean the analysis of an 
existing product (program), typically by a third party (such as a 
certifier) who has to satisfy themselves that the product meets certain 
criteria (such as showing the absence of bypassing a security manager or 
exception free execution).  It is assumed that such third parties have 
little control over the development process or languages used to 
implement a product.  They may even have little sight of the development 
documentation (or even the source code).  But for the purposes of my 
initial question, lets assume that both the design documentation and 
source code are available.

Having said this, another member of the list provided their own 
interpretation, which is also valid, namely, "someone has already 
written a program in a weakly-typed language but then [wants] to analyze 
that program for further properties using types? ".

Thanks for your responses, I am now in the process of following up the 
pointers you have given me. In summary, the (public*) pointers include:
@ Work on index type systems (independently invented by Christopher 
Zenger and Hongwei Xi in the 90's).
@ The *PURe Project (*Program Understanding and Re-engineering: Calculi 
and Applications)  which apply formal methods "in-reverse". Project 
homepage http://wiki.di.uminho.pt/wiki/bin/view/PURe
@ "Anno Domini", which used types to analyze COBOL programs for 
year-2000 issues. From Type Theory to Year 2000 Conversion Tool  
http://citeseer.ist.psu.edu/eidorff99annodomini.html
@ Raghavan Komondoor, G. Ramalingam, Satish Chandra, John Field, 
"Dependent Types for Program Understanding", in the Proceedings of TACAS 
2005, LNCS 3440, Springer Berlin / Heidelberg, 2005. (analyzing COBOL 
programs).
@ Jeff Foster's (UMD) CQual language, which does "type qualifier" 
inference to find security flaws and other things in C programs. CQual 
homepage http://www.cs.umd.edu/~jfoster/cqual/
@ Necula's (UC Berkeley) CCured project that does another kind of type 
inference for the purpose of making C programs memory safe. Project home 
page http://manju.cs.berkeley.edu/ccured/ 
<http://freshmeat.net/redir/ccured/37987/url_homepage/ccured> (Tool 
available from http://freshmeat.net/projects/ccured/).

*I have only included those pointers that I believe were referencing 
publicly available information. And I have removed the names of the 
correspondents as I have not asked their permission to quote them. 
(Having said this, I will happily give credit if they like; this can be 
done in hindsight, whereas mentioning them publicly cannot easily be 
retracted).

Thanks for your help,

Anthony.

Michael Anthony Smith wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> I have been a (silent) member of the types list for several years, as I 
> am interested in monitoring (and hopefully using) developments in type 
> theory. I certainly make use of (reasonably) strongly types 
> specification and programming languages in my work, which is regularly 
> involving the analysis of third party designs/code. Within this context 
> it is often hard to use developments in the type-theory, as they appear 
> (at least to me) to be aimed at designing solid development languages 
> and frameworks.
>
> I know that type systems are used to design languages (and frameworks) 
> that have a given collection of desirable properties, whether this be 
> the traditional "shape" correctness or for some other concern such as 
> guaranteeing various concurrency or security properties. I also am aware 
> of the link between type theories and abstract interpretation. What I 
> was wondering if anyone here knows of the application of type theories 
> to the post-development analysis context?
>
> Thanks,
>
> Anthony.
>
>
>
>
>   

From mwh at cs.umd.edu  Thu Mar  9 09:36:40 2006
From: mwh at cs.umd.edu (Michael Hicks)
Date: Thu, 9 Mar 2006 09:36:40 -0500
Subject: [TYPES] Query: Types for post-development analysis?
In-Reply-To: <44100189.7070808@eris.qinetiq.com>
References: <440EB633.9000604@eris.qinetiq.com>
	<44100189.7070808@eris.qinetiq.com>
Message-ID: <5D2C5647-9552-4B40-BDF6-AA15BB7FD395@cs.umd.edu>

Many, if not all, of these are examples of so-called "type-based  
analysis" in which reasoning about a program is set up as a type  
system rather than as a problem in model checking, abstract  
interpretation, data flow analysis, etc.  Jens Palsberg has a page on  
this topic that contains pointers to many papers (though it appears  
somewhat dated): http://www.cs.ucla.edu/~palsberg/tba/

There is a survey paper he wrote on this topic that is quite  
accessible: http://www.cs.ucla.edu/~palsberg/tba/papers/palsberg- 
paste01.pdf

-Mike


On Mar 9, 2006, at 5:20 AM, Michael Anthony Smith wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Clarification and Summary (so far)
>
> I have already had several useful replies to this original posting
> (thanks). But, from some of these replies it is clear that it is worth
> clarifying my use of the "post-development analysis context", thus  
> I am
> enclosing a description that I sent individually to one of the list  
> members.
>
> By "the post-development analysis context" I mean the analysis of an
> existing product (program), typically by a third party (such as a
> certifier) who has to satisfy themselves that the product meets  
> certain
> criteria (such as showing the absence of bypassing a security  
> manager or
> exception free execution).  It is assumed that such third parties have
> little control over the development process or languages used to
> implement a product.  They may even have little sight of the  
> development
> documentation (or even the source code).  But for the purposes of my
> initial question, lets assume that both the design documentation and
> source code are available.
>
> Having said this, another member of the list provided their own
> interpretation, which is also valid, namely, "someone has already
> written a program in a weakly-typed language but then [wants] to  
> analyze
> that program for further properties using types? ".
>
> Thanks for your responses, I am now in the process of following up the
> pointers you have given me. In summary, the (public*) pointers  
> include:
> @ Work on index type systems (independently invented by Christopher
> Zenger and Hongwei Xi in the 90's).
> @ The *PURe Project (*Program Understanding and Re-engineering:  
> Calculi
> and Applications)  which apply formal methods "in-reverse". Project
> homepage http://wiki.di.uminho.pt/wiki/bin/view/PURe
> @ "Anno Domini", which used types to analyze COBOL programs for
> year-2000 issues. From Type Theory to Year 2000 Conversion Tool
> http://citeseer.ist.psu.edu/eidorff99annodomini.html
> @ Raghavan Komondoor, G. Ramalingam, Satish Chandra, John Field,
> "Dependent Types for Program Understanding", in the Proceedings of  
> TACAS
> 2005, LNCS 3440, Springer Berlin / Heidelberg, 2005. (analyzing COBOL
> programs).
> @ Jeff Foster's (UMD) CQual language, which does "type qualifier"
> inference to find security flaws and other things in C programs. CQual
> homepage http://www.cs.umd.edu/~jfoster/cqual/
> @ Necula's (UC Berkeley) CCured project that does another kind of type
> inference for the purpose of making C programs memory safe. Project  
> home
> page http://manju.cs.berkeley.edu/ccured/
> <http://freshmeat.net/redir/ccured/37987/url_homepage/ccured> (Tool
> available from http://freshmeat.net/projects/ccured/).
>
> *I have only included those pointers that I believe were referencing
> publicly available information. And I have removed the names of the
> correspondents as I have not asked their permission to quote them.
> (Having said this, I will happily give credit if they like; this  
> can be
> done in hindsight, whereas mentioning them publicly cannot easily be
> retracted).
>
> Thanks for your help,
>
> Anthony.
>
> Michael Anthony Smith wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list ]
>>
>> I have been a (silent) member of the types list for several years,  
>> as I
>> am interested in monitoring (and hopefully using) developments in  
>> type
>> theory. I certainly make use of (reasonably) strongly types
>> specification and programming languages in my work, which is  
>> regularly
>> involving the analysis of third party designs/code. Within this  
>> context
>> it is often hard to use developments in the type-theory, as they  
>> appear
>> (at least to me) to be aimed at designing solid development languages
>> and frameworks.
>>
>> I know that type systems are used to design languages (and  
>> frameworks)
>> that have a given collection of desirable properties, whether this be
>> the traditional "shape" correctness or for some other concern such as
>> guaranteeing various concurrency or security properties. I also am  
>> aware
>> of the link between type theories and abstract interpretation. What I
>> was wondering if anyone here knows of the application of type  
>> theories
>> to the post-development analysis context?
>>
>> Thanks,
>>
>> Anthony.
>>
>>
>>
>>
>>


From Y.Luo at kent.ac.uk  Thu Mar 16 12:28:02 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Thu, 16 Mar 2006 17:28:02 -0000
Subject: [TYPES] Eliminators in type theory
Message-ID: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>


I would like to understand  how powerful the eliminators of inductive types
can be in type theory.

Suppose a type system has the type of natural numbers ONLY, that is, we have
only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
computation rules.

Can we define fib function in such a system? Note that we don't have pairs
and function types.

fib 0 = 1
fib 1 = 1
fib (n+2) = fib n + fib (n+1)

In such a  system, we know some functions can be defined, for example,
plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
If we add the type of pairs, then more efficient fib can be easily defined.

Thanks,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent



From txa at cs.nott.ac.uk  Fri Mar 17 05:17:20 2006
From: txa at cs.nott.ac.uk (Thorsten Altenkirch)
Date: Fri, 17 Mar 2006 10:17:20 +0000
Subject: [TYPES] Eliminators in type theory
In-Reply-To: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
Message-ID: <441A8CB0.8080703@cs.nott.ac.uk>



Yong Luo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> I would like to understand  how powerful the eliminators of inductive types
> can be in type theory.
> 
> Suppose a type system has the type of natural numbers ONLY, that is, we have
> only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
> computation rules.

This is a functional representation of arithmetic, i.e. Goedel's system T. All functions 
provable total in arithmetic can be defined. Adding dependent types doesn't affect the 
strength of the system, nether does the addition of pairs (whether dependent or not).

T.

> 
> Can we define fib function in such a system? Note that we don't have pairs
> and function types.
> 
> fib 0 = 1
> fib 1 = 1
> fib (n+2) = fib n + fib (n+1)
> 
> In such a  system, we know some functions can be defined, for example,
> plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
> If we add the type of pairs, then more efficient fib can be easily defined.
> 
> Thanks,
> 
> Yong
> ==============================
> Dr. Yong Luo
> Computing Laboratory
> University of Kent
> 
> 

-- 
Dr. Thorsten Altenkirch		   phone : (+44) (0)115 84 66516
Lecturer			   http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT	   University of Nottingham

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.


From Y.Luo at kent.ac.uk  Fri Mar 17 05:52:55 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Fri, 17 Mar 2006 10:52:55 -0000
Subject: [TYPES] Eliminators in type theory
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
	<441A8CB0.8080703@cs.nott.ac.uk>
Message-ID: <00c601c649b0$f2689610$0000fea9@ad.kent.ac.uk>

I am not sure the system I specified is the same as the system T, and would
like to know how the fib function can be defined by the type of natural
numbers without introducing any other types.

Yong

>
> Yong Luo wrote:
> > [ The Types Forum,
http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >
> >
> > I would like to understand  how powerful the eliminators of inductive
types
> > can be in type theory.
> >
> > Suppose a type system has the type of natural numbers ONLY, that is, we
have
> > only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
> > computation rules.
>
> This is a functional representation of arithmetic, i.e. Goedel's system T.
All functions
> provable total in arithmetic can be defined. Adding dependent types
doesn't affect the
> strength of the system, nether does the addition of pairs (whether
dependent or not).
>
> T.
>
> >
> > Can we define fib function in such a system? Note that we don't have
pairs
> > and function types.
> >
> > fib 0 = 1
> > fib 1 = 1
> > fib (n+2) = fib n + fib (n+1)
> >
> > In such a  system, we know some functions can be defined, for example,
> > plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
> > If we add the type of pairs, then more efficient fib can be easily
defined.
> >
> > Thanks,
> >
> > Yong
> > ==============================
> > Dr. Yong Luo
> > Computing Laboratory
> > University of Kent
> >
> >
>
> -- 
> Dr. Thorsten Altenkirch    phone : (+44) (0)115 84 66516
> Lecturer    http://www.cs.nott.ac.uk/~txa/
> School of Computer Science & IT    University of Nottingham
>
> This message has been checked for viruses but the contents of an
attachment
> may still contain software viruses, which could damage your computer
system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
>


From abel at informatik.uni-muenchen.de  Fri Mar 17 08:11:32 2006
From: abel at informatik.uni-muenchen.de (Andreas Abel)
Date: Fri, 17 Mar 2006 14:11:32 +0100
Subject: [TYPES] Eliminators in type theory
In-Reply-To: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
Message-ID: <441AB584.30504@informatik.uni-muenchen.de>

Pairs can be simulated by with higher-order primitive recursion.  For 
instance, the following (Haskell) functions 'iter' and 'fib' are 
definable in type theory with function spaces, natural numbers, and 
eliminators alone.

iter :: Int -> Int -> Int -> Int
iter k l 0     = k
iter k l (n+1) = iter l (k+l) n

fib :: Int -> Int
fib = iter 0 1

fibs = [ fib i | i <- [0..]]

test = take 15 fibs
-- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]

Maybe you have to reformulate your question, such that the eliminators 
can only produce something of base type, e.g., inductive type, but not 
function type.  Then, the Ackermann function is not definable.

Cheers,
Andreas

Yong Luo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> I would like to understand  how powerful the eliminators of inductive types
> can be in type theory.
> 
> Suppose a type system has the type of natural numbers ONLY, that is, we have
> only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
> computation rules.
> 
> Can we define fib function in such a system? Note that we don't have pairs
> and function types.
> 
> fib 0 = 1
> fib 1 = 1
> fib (n+2) = fib n + fib (n+1)
> 
> In such a  system, we know some functions can be defined, for example,
> plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
> If we add the type of pairs, then more efficient fib can be easily defined.
> 
> Thanks,
> 
> Yong
> ==============================
> Dr. Yong Luo
> Computing Laboratory
> University of Kent
> 
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/

From abel at informatik.uni-muenchen.de  Fri Mar 17 10:23:16 2006
From: abel at informatik.uni-muenchen.de (Andreas Abel)
Date: Fri, 17 Mar 2006 16:23:16 +0100
Subject: [TYPES] Eliminators in type theory
In-Reply-To: <441AB584.30504@informatik.uni-muenchen.de>
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
	<441AB584.30504@informatik.uni-muenchen.de>
Message-ID: <441AD464.4050501@informatik.uni-muenchen.de>

Sorry, I misread your message the first time.  You said you have neither 
pair nor function types.

Anyway, pairs of natural numbers can be coded using the old trick

   pair x y = 2^x * 3^y

This is primitive recursive (i.e., definable using Elim_Nat), and fst 
and snd should be codable primitive recursively as well.  Then, fib is 
definable using primitive recursion, but do not ask me about efficiency ;-)

Andreas


Andreas Abel wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Pairs can be simulated by with higher-order primitive recursion.  For 
> instance, the following (Haskell) functions 'iter' and 'fib' are 
> definable in type theory with function spaces, natural numbers, and 
> eliminators alone.
> 
> iter :: Int -> Int -> Int -> Int
> iter k l 0     = k
> iter k l (n+1) = iter l (k+l) n
> 
> fib :: Int -> Int
> fib = iter 0 1
> 
> fibs = [ fib i | i <- [0..]]
> 
> test = take 15 fibs
> -- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]
> 
> Maybe you have to reformulate your question, such that the eliminators 
> can only produce something of base type, e.g., inductive type, but not 
> function type.  Then, the Ackermann function is not definable.
> 
> Cheers,
> Andreas
> 
> Yong Luo wrote:
> 
>>[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>>
>>I would like to understand  how powerful the eliminators of inductive types
>>can be in type theory.
>>
>>Suppose a type system has the type of natural numbers ONLY, that is, we have
>>only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
>>computation rules.
>>
>>Can we define fib function in such a system? Note that we don't have pairs
>>and function types.
>>
>>fib 0 = 1
>>fib 1 = 1
>>fib (n+2) = fib n + fib (n+1)
>>
>>In such a  system, we know some functions can be defined, for example,
>>plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
>>If we add the type of pairs, then more efficient fib can be easily defined.
>>
>>Thanks,
>>
>>Yong
>>==============================
>>Dr. Yong Luo
>>Computing Laboratory
>>University of Kent
>>
>>
> 
> 
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/

From U.Berger at swansea.ac.uk  Fri Mar 17 10:32:59 2006
From: U.Berger at swansea.ac.uk (Ulrich Berger)
Date: Fri, 17 Mar 2006 15:32:59 +0000
Subject: [TYPES] Eliminators in type theory
In-Reply-To: <441AB584.30504@informatik.uni-muenchen.de>
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
	<441AB584.30504@informatik.uni-muenchen.de>
Message-ID: <441AD6AB.8090400@swansea.ac.uk>

Even if you disallow function types as result type of an elimination,
coding of two numbers into a single one as well as the corresponding 
projections can be defined (old stuff in books on computability theory 
or logic).

Uli

Andreas Abel wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Pairs can be simulated by with higher-order primitive recursion.  For 
> instance, the following (Haskell) functions 'iter' and 'fib' are 
> definable in type theory with function spaces, natural numbers, and 
> eliminators alone.
> 
> iter :: Int -> Int -> Int -> Int
> iter k l 0     = k
> iter k l (n+1) = iter l (k+l) n
> 
> fib :: Int -> Int
> fib = iter 0 1
> 
> fibs = [ fib i | i <- [0..]]
> 
> test = take 15 fibs
> -- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]
> 
> Maybe you have to reformulate your question, such that the eliminators 
> can only produce something of base type, e.g., inductive type, but not 
> function type.  Then, the Ackermann function is not definable.
> 
> Cheers,
> Andreas
> 
> Yong Luo wrote:
> 
>>[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>>
>>I would like to understand  how powerful the eliminators of inductive types
>>can be in type theory.
>>
>>Suppose a type system has the type of natural numbers ONLY, that is, we have
>>only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
>>computation rules.
>>
>>Can we define fib function in such a system? Note that we don't have pairs
>>and function types.
>>
>>fib 0 = 1
>>fib 1 = 1
>>fib (n+2) = fib n + fib (n+1)
>>
>>In such a  system, we know some functions can be defined, for example,
>>plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
>>If we add the type of pairs, then more efficient fib can be easily defined.
>>
>>Thanks,
>>
>>Yong
>>==============================
>>Dr. Yong Luo
>>Computing Laboratory
>>University of Kent
>>
>>
> 
> 
> 

From jonathan.seldin at uleth.ca  Fri Mar 17 14:15:41 2006
From: jonathan.seldin at uleth.ca (Jonathan Seldin)
Date: Fri, 17 Mar 2006 12:15:41 -0700
Subject: [TYPES] Eliminators in type theory
In-Reply-To: <441AD6AB.8090400@swansea.ac.uk>
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
	<441AB584.30504@informatik.uni-muenchen.de>
	<441AD6AB.8090400@swansea.ac.uk>
Message-ID: <FBBA9E69-E490-41A7-B8C4-9D2F722F8FC3@uleth.ca>

If you are talking about a functional language that includes pure  
lambda-calculus, you might be interested in the discussion in Curry,  
Hindley, and Seldin, Combinatory Logic, vol. II (North-Holland,  
1968), section 13D.  Here R is Elim_Nat.  Definitions of Elim_Nat and  
pairs are given in terms of an iterator (called Z), which takes each  
numeral to its corresponding Church numeral (\xy.x(x(...(xy)...)),  
where there are n x's after the dot), and since this iterator can  
easily be defined in terms of Elim_Nat, the definitions would work in  
the proposed system.  This shows, I think, that fib could be defined  
in the proposed system without the numerical coding of pairs.

But this contains no information about efficiency.

On 17-Mar-06, at 8:32 AM, Ulrich Berger wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Even if you disallow function types as result type of an elimination,
> coding of two numbers into a single one as well as the corresponding
> projections can be defined (old stuff in books on computability theory
> or logic).
>
> Uli
>
> Andreas Abel wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list ]
>>
>> Pairs can be simulated by with higher-order primitive recursion.  For
>> instance, the following (Haskell) functions 'iter' and 'fib' are
>> definable in type theory with function spaces, natural numbers, and
>> eliminators alone.
>>
>> iter :: Int -> Int -> Int -> Int
>> iter k l 0     = k
>> iter k l (n+1) = iter l (k+l) n
>>
>> fib :: Int -> Int
>> fib = iter 0 1
>>
>> fibs = [ fib i | i <- [0..]]
>>
>> test = take 15 fibs
>> -- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]
>>
>> Maybe you have to reformulate your question, such that the  
>> eliminators
>> can only produce something of base type, e.g., inductive type, but  
>> not
>> function type.  Then, the Ackermann function is not definable.
>>
>> Cheers,
>> Andreas
>>
>> Yong Luo wrote:
>>
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>>> types-list ]
>>>
>>>
>>> I would like to understand  how powerful the eliminators of  
>>> inductive types
>>> can be in type theory.
>>>
>>> Suppose a type system has the type of natural numbers ONLY, that  
>>> is, we have
>>> only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and  
>>> its two
>>> computation rules.
>>>
>>> Can we define fib function in such a system? Note that we don't  
>>> have pairs
>>> and function types.
>>>
>>> fib 0 = 1
>>> fib 1 = 1
>>> fib (n+2) = fib n + fib (n+1)
>>>
>>> In such a  system, we know some functions can be defined, for  
>>> example,
>>> plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
>>> If we add the type of pairs, then more efficient fib can be  
>>> easily defined.
>>>
>>> Thanks,
>>>
>>> Yong
>>> ==============================
>>> Dr. Yong Luo
>>> Computing Laboratory
>>> University of Kent
>>>
>>>
>>
>>
>>

Jonathan P. Seldin                                     tel: 403-329-2364
Department of Mathematics and Computer Science  jonathan.seldin at uleth.ca
University of Lethbridge                              seldin at cs.uleth.ca
4401 University Drive                    http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4



From jonathan.seldin at uleth.ca  Fri Mar 17 14:18:45 2006
From: jonathan.seldin at uleth.ca (Jonathan Seldin)
Date: Fri, 17 Mar 2006 12:18:45 -0700
Subject: [TYPES] Oops
Message-ID: <42A97625-DC5B-470F-ADB6-69B91D3D5D65@uleth.ca>

In my previous message, I should have given the date for Combinatory  
Logic, vol. II as 1972, not 1968.

I might also mention that the section of the book involved was mainly  
Curry's work.

Jonathan P. Seldin                                     tel: 403-329-2364
Department of Mathematics and Computer Science  jonathan.seldin at uleth.ca
University of Lethbridge                              seldin at cs.uleth.ca
4401 University Drive                    http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4



From jonathan.seldin at uleth.ca  Sun Mar 19 13:36:04 2006
From: jonathan.seldin at uleth.ca (Jonathan P. Seldin)
Date: Sun, 19 Mar 2006 11:36:04 -0700
Subject: [TYPES] Eliminators in type theory
In-Reply-To: <002901c64a85$87f00e00$8118738d@chene>
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk>
	<441AB584.30504@informatik.uni-muenchen.de>
	<441AD6AB.8090400@swansea.ac.uk>
	<FBBA9E69-E490-41A7-B8C4-9D2F722F8FC3@uleth.ca>
	<002901c64a85$87f00e00$8118738d@chene>
Message-ID: <83306617-D133-4A7A-803B-19E65D9B8921@uleth.ca>

Dear Sergei,

Thank you for calling my attention to this.

However, the answer to Yong is still contained in Cjombinatory Logic,  
vol II.  In section 13D2 (pp. 277-279), Curry considers three pairing  
combinators D.  All three have types of the form A -> A -> B -> A for  
a type B which depends on the particular pairing combinator and any  
type A (including the type of natural numbers).  (The type B is  
related to the projection functions.)  With any of these pairing  
combinators, it should be possible to define fib.  (The problem that  
Curry reported with these pairing combinators was that they only had  
types if the first and second element of the pair had the same  
type.)  This shows that the numerical coding of pairs is not necessary.

In section 13D4 (pp. 285ff), Curry defines the class of functions he  
calls prorecursive to be those whose defining terms have types in his  
system, and in Theorem 13D1 (pp. 285-6), he proves that all primitive  
recursive functions are prorecursive using Elim_Nat restricted to  
output type Nat.  He goes on to assert that he has a proof that all  
doubly recursive numerical functions are prorecursive, and presents a  
conjecture that all n-recursive functions are in this class.  He does  
not explicitly say there that he has used Elim_Nat only with output  
of type Nat, but I have his notes here, and I can check his proof.

On Mar 18, 2006, at 5:14 AM, Sergei Soloviev wrote:

> Dear Jonathan,
>
> as far as I understand Yong, he considers typed lambda-calculus and  
> does not permit Elim_Nat
> with values in any other type than Nat, and in this situation it  
> seems not clear how to define iterator Z.
>
> Best regards,
>
> Sergei Soloviev
> IRIT
> Universite Paul Sabatier
> Toulouse
>
> (I did work for some time with Zhaohui Luo and his student Yong Luo.)
>
> ----- Original Message ----- From: "Jonathan Seldin"  
> <jonathan.seldin at uleth.ca>
> To: "type-list" <types-list at lists.seas.upenn.edu>
> Sent: Friday, March 17, 2006 8:15 PM
> Subject: Re: [TYPES] Eliminators in type theory
>
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list ]
>>
>> If you are talking about a functional language that includes pure
>> lambda-calculus, you might be interested in the discussion in Curry,
>> Hindley, and Seldin, Combinatory Logic, vol. II (North-Holland,
>> 1968), section 13D.  Here R is Elim_Nat.  Definitions of Elim_Nat and
>> pairs are given in terms of an iterator (called Z), which takes each
>> numeral to its corresponding Church numeral (\xy.x(x(...(xy)...)),
>> where there are n x's after the dot), and since this iterator can
>> easily be defined in terms of Elim_Nat, the definitions would work in
>> the proposed system.  This shows, I think, that fib could be defined
>> in the proposed system without the numerical coding of pairs.
>>
>> But this contains no information about efficiency.
>>
>> On 17-Mar-06, at 8:32 AM, Ulrich Berger wrote:
>>
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
>>> types-list ]
>>>
>>> Even if you disallow function types as result type of an  
>>> elimination,
>>> coding of two numbers into a single one as well as the corresponding
>>> projections can be defined (old stuff in books on computability  
>>> theory
>>> or logic).
>>>
>>> Uli
>>>
>>> Andreas Abel wrote:
>>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
>>>> types-list ]
>>>>
>>>> Pairs can be simulated by with higher-order primitive  
>>>> recursion.  For
>>>> instance, the following (Haskell) functions 'iter' and 'fib' are
>>>> definable in type theory with function spaces, natural numbers, and
>>>> eliminators alone.
>>>>
>>>> iter :: Int -> Int -> Int -> Int
>>>> iter k l 0     = k
>>>> iter k l (n+1) = iter l (k+l) n
>>>>
>>>> fib :: Int -> Int
>>>> fib = iter 0 1
>>>>
>>>> fibs = [ fib i | i <- [0..]]
>>>>
>>>> test = take 15 fibs
>>>> -- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]
>>>>
>>>> Maybe you have to reformulate your question, such that the
>>>> eliminators
>>>> can only produce something of base type, e.g., inductive type, but
>>>> not
>>>> function type.  Then, the Ackermann function is not definable.
>>>>
>>>> Cheers,
>>>> Andreas
>>>>
>>>> Yong Luo wrote:
>>>>
>>>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
>>>>> types-list ]
>>>>>
>>>>>
>>>>> I would like to understand  how powerful the eliminators of
>>>>> inductive types
>>>>> can be in type theory.
>>>>>
>>>>> Suppose a type system has the type of natural numbers ONLY, that
>>>>> is, we have
>>>>> only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and
>>>>> its two
>>>>> computation rules.
>>>>>
>>>>> Can we define fib function in such a system? Note that we don't
>>>>> have pairs
>>>>> and function types.
>>>>>
>>>>> fib 0 = 1
>>>>> fib 1 = 1
>>>>> fib (n+2) = fib n + fib (n+1)
>>>>>
>>>>> In such a  system, we know some functions can be defined, for
>>>>> example,
>>>>> plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
>>>>> If we add the type of pairs, then more efficient fib can be
>>>>> easily defined.
>>>>>
>>>>> Thanks,
>>>>>
>>>>> Yong
>>>>> ==============================
>>>>> Dr. Yong Luo
>>>>> Computing Laboratory
>>>>> University of Kent
>>>>>
>>>>>
>>>>
>>>>
>>>>
>>
>> Jonathan P. Seldin                                     tel:  
>> 403-329-2364
>> Department of Mathematics and Computer Science   
>> jonathan.seldin at uleth.ca
>> University of Lethbridge                               
>> seldin at cs.uleth.ca
>> 4401 University Drive                    http://www.cs.uleth.ca/ 
>> ~seldin/
>> Lethbridge, Alberta, Canada, T1K 3M4
>>
>

Jonathan P. Seldin                                     tel: 403-329-2364
Department of Mathematics and Computer Science  jonathan.seldin at uleth.ca
University of Lethbridge                              seldin at cs.uleth.ca
4401 University Drive                    http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4



From ohori at riec.tohoku.ac.jp  Sun Mar 19 21:58:00 2006
From: ohori at riec.tohoku.ac.jp (Atsushi Ohori)
Date: Mon, 20 Mar 2006 11:58:00 +0900 (JST)
Subject: [TYPES] SML# alpha release
Message-ID: <20060320.115800.971159580.ohori@riec.tohoku.ac.jp>

Dear types list colleagues,

I thought some of you might be interested in our new language, SML#,
whose alpha release is now available at:

  http://www.pllab.riec.tohoku.ac.jp/smlsharp/

SML# is a conservation extension of the Definition of SML with few
moderate but practically important features, including
interoperability, record polymorphism, and rank1 polymorphism.

Its compiler heavily uses type information to achieves these features,
especially interoperability.

I appreciate any comments, criticism, suggestions.

	Best regards,
	Atsushi Ohori
	Research Institute of Electrical Communication
	Tohoku University

From soloviev at irit.fr  Mon Mar 20 11:30:41 2006
From: soloviev at irit.fr (Sergei SOLOVIEV)
Date: Mon, 20 Mar 2006 17:30:41 +0100
Subject: [TYPES] Eliminators in type theory
In-Reply-To: <42A97625-DC5B-470F-ADB6-69B91D3D5D65@uleth.ca>
References: <42A97625-DC5B-470F-ADB6-69B91D3D5D65@uleth.ca>
Message-ID: <200603201730.41693.soloviev@irit.fr>

(I have already sent it to Yong Luo)

it can be done using more simple coding of pairs <x,y> = (x+y)(x+y+1)/2 +y 
and corresponding projections p1 and p2
(about their definitions I'll speak below).

Assume that <x, y> and p1, p2 are already defined using Elim_Nat. Then we 
may define the function F(x) = <fib(x), fib(x+1)>
using Elim_Nat because F(x+1) = <fib(x+1), fib(x+2)> = <fib(x+1), fib(x)+ 
fib(x+1)>= <p2(F(x)), p1(F(x))+p2(F(x))>
and fib(x) will be p1(F(x)).

Concerning the definitions of <...>, p1, p2, I will not go into definition 
of multiplication *, division (integer) by 2, call it
div2, substraction (where we pose n-m=0 if m>=n) using Elim_Nat (this is 
easy - but it will take space). Plus + you have already defined. I already 
defined pred.

<x, y> = (div2 ((x+y)*(x+y+1)))+y

To define projections we define

d = Elim_Nat(S0)(\p:Nat.\r:Nat.0)      (dn =1 if n=0 and 0 otherwise)

d' = Elim_Nat(0)(\p:Nat.\r:Nat.S0)     (d'n =0 if n=0 and 1 otherwise)

k=  Elim_Nat 0 (\p:Nat\r:Nat. (r+(d((Sr)*(SSr)- 2*(Sp)))))    (enumeration 
of pairs, if you put them on the plan xy is done along
the diagonals y= -x+kn and kn is the number of a diagonal where the pair of 
number n is placed)

for the pair number 0 k0 =0,
for the pairs 1 and 2 k1=k2=1,
k3=k4=k5 = 2 etc



Now

p1 = Elim_Nat 0 (\p:Nat\r:Nat. (((dr)*(S(kp)))+((d'r)*(pred r))))

p2 = \n:Nat.(kn - (p1)n)


I copied these definitions from our old text with David Chemouil, there may 
be some small
arithmetical errors, but essentially it is like this.
>

soloviev at irit.fr
Sergei SOLOVIEV

From nobrowser at gmail.com  Tue Mar 21 00:12:48 2006
From: nobrowser at gmail.com (Ian Zimmerman)
Date: Mon, 20 Mar 2006 21:12:48 -0800 (PST)
Subject: [TYPES] SML# alpha release
In-Reply-To: <20060320.115800.971159580.ohori@riec.tohoku.ac.jp>
References: <20060320.115800.971159580.ohori@riec.tohoku.ac.jp>
Message-ID: <87lkv4pei9.fsf@ahiker.homeip.net>


Atsushi> I thought some of you might be interested in our new language,
Atsushi> SML#, whose alpha release is now available at:

Atsushi>   http://www.pllab.riec.tohoku.ac.jp/smlsharp/

Atsushi> SML# is a conservation extension of the Definition of SML with
Atsushi> few moderate but practically important features, including
Atsushi> interoperability, record polymorphism, and rank1 polymorphism.

Atsushi> Its compiler heavily uses type information to achieves these
Atsushi> features, especially interoperability.

Sorry, I know I should just look at the website, but it has been a
very long day and I am too tired to do it.  So 2 questions:

"interoperability" - with what?

"heavily uses type information" - does that mean _runtime_ type
information?  That would be a significant departure indeed from the
design of SML ...

-- 
A true pessimist won't be discouraged by a little success.

From greg at eecs.harvard.edu  Tue Mar 21 09:08:53 2006
From: greg at eecs.harvard.edu (Greg Morrisett)
Date: Tue, 21 Mar 2006 09:08:53 -0500
Subject: [TYPES] SML# alpha release
In-Reply-To: <87lkv4pei9.fsf@ahiker.homeip.net>
References: <20060320.115800.971159580.ohori@riec.tohoku.ac.jp>
	<87lkv4pei9.fsf@ahiker.homeip.net>
Message-ID: <442008F5.3050801@eecs.harvard.edu>

Ian Zimmerman wrote:
> "interoperability" - with what?

A cursory glance at the web site reveals that the compiler
represents scalar values natively (i.e., doesn't tag them as in
SML/NJ or O'Caml) and uses a factored bit-field representation
for records & arrays to support native layouts.  Hence, passing
many data values to/from C (or Java) doesn't require data
conversions.  In that sense, SML# seems to make interoperability
with C/C++ or Java much simpler than other ML compilers.

> "heavily uses type information" - does that mean _runtime_ type
> information?  That would be a significant departure indeed from the
> design of SML ...

Huh?  In what sense does the design of SML dictate that you
should throw away all of the type information you collect
at compile time?

All ML implementations use run-time type information.  They
just represent it and use it differently.  All of them need some
form of type information to support accurate garbage collection.
Most compilers use tags (a la Lisp) to represent
this information at run-time.  Some (e.g., Tolmach's, TIL's,
Minamide's, etc.) have done so-called tag-free collectors which
really just factor the tags out into separate representations.  Only
the original Kit compiler did memory management in a truly tag-free
fashion (but it had bad leaks compared to a tracing collector, so
they've added support for tracing on top of the regions, and hence
tags again.)

Some compilers use the tags to also support polymorphic equality,
while others represent that information "procedurally"
in a style similar to Haskell type class dictionaries.  (Whether
type information is encoded with representation bits, a pointer
to a vtable, or a pointer to a type-specific method doesn't
matter---they're all making it possible to do some form of
run-time type dispatch.)

Some compilers go to an extreme (e.g., TILT) and pass representations
of types to polymorphic functions at run-time so that data
representations, calling conventions, etc. can be specialized.

SML# just goes further in its use of the run-time type representation
information to support things like interoperability (see above),
polymorphic record selection and the other features added to the
language.

-Greg

From martini at cs.unibo.it  Wed Mar 22 11:03:59 2006
From: martini at cs.unibo.it (Simone Martini)
Date: Wed, 22 Mar 2006 17:03:59 +0100
Subject: [TYPES] Expressivity of primitive recursion (was: Eliminators in
	type theory)
Message-ID: <F6C9D622-7E15-4F97-83EC-68A74CE5546E@cs.unibo.it>

I would like to make a side-remark on the thread on eliminators.

The thread focussed on what could be done
with higher-order types and the inductive type of natural
numbers.

In particular Seldin pointed out that Curry had a proof
that all primitive recursive functions get a type in a system
where Elim_Nat is used only with output of type Nat.
It would indeed be interesting to see if this restriction
could be enforced also for the representability of n-recursive  
functions,
since this is a huge class of functions, well beyond (first-order)  
primitive
recursion.

However, bounding the recursion rank is not the only way of limiting
the expressive power of higher-order recursion.

Another approach consists in tailoring the use of duplication, without
altering the higher-order nature of recursion. This has been  
investigated
for some time in fragments of Goedel's T
(e.g., by Hofmann, Bellantoni, Niggl, Schwichtenberg, etc.).

A recent paper by Ugo Dal Lago
(The geometry of linear higher-order recursion, in Lics 2005)
shows that the usual formulation of T, but with the contraction
restricted only to base types (natural numbers) exactly characterizes
first-order primitive recursion.

-sm
---------------------------------------------------
Simone Martini                          tel: +39 051 2094979
Universita' di Bologna                  fax: +39 051 2094510
Dip. di Scienze dell'Informazione
Mura Anteo Zamboni, 7
40127 Bologna BO                        www.cs.unibo.it/~martini
Italy



From Y.Luo at kent.ac.uk  Thu Mar 23 07:38:13 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Thu, 23 Mar 2006 12:38:13 -0000
Subject: [TYPES] Eliminators in type theory
References: <009d01c6491e$fa26ef60$0000fea9@ad.kent.ac.uk><441AB584.30504@informatik.uni-muenchen.de><441AD6AB.8090400@swansea.ac.uk><FBBA9E69-E490-41A7-B8C4-9D2F722F8FC3@uleth.ca><002901c64a85$87f00e00$8118738d@chene>
	<83306617-D133-4A7A-803B-19E65D9B8921@uleth.ca>
Message-ID: <016101c64e76$a68158c0$a0290c81@ad.kent.ac.uk>

Dear all,

Thanks for your reponse to my question. I have got a few different
definitions of the fib function. All the definitions looks quite different
from the original one. So I still have anther question.

>From the definitions, we can prove that fib (n+2) is equal to fib n + fib
(n+1) for all n. However, they are not definitionally (or computationally)
equal to each other. In other words, if n is a variable, then fib (n+2)
cannot be reduced to fib n + fib (n+1). So, my question is the following.

Suppose that we have a normal type system, for example, a type system with
Nat, Pairs and function type with their eliminatiors and computation rules.
Can we define the fib function such that fib (n+2) can be reduced to fib n +
fib (n+1) where n is a variable?

Regards,

Yong


From Y.Luo at kent.ac.uk  Thu Mar 30 07:06:24 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Thu, 30 Mar 2006 13:06:24 +0100
Subject: [TYPES] Definable programs in type theories
Message-ID: <03c701c653f2$5ddd67e0$a0290c81@ad.kent.ac.uk>

Dear all,

Last time I asked a question about the fib function, "can we define the fib
function in a normal type system (eg. Martin-Lof's type theory, Luo's UTT),
and such that fib (n+2) and fib n + fib (n+1) are computationally (or
definitionally) equal to each other?"

I have got some responses and the answer seems to be "No", although it
cannot be proved. I am wondering whether anyone has any idea about the
proof.

When we talk about definability of functions (or programs), we must be clear
what we mean by two functions (or two programs) are the same. For example,
one may ask "can you define the QuickSort in the system?". We cannot simply
answer "Yes" based on the fact that we can define another sorting program.

Regards,

Yong





From Y.Luo at kent.ac.uk  Tue Apr 25 10:39:27 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Tue, 25 Apr 2006 15:39:27 +0100
Subject: [TYPES] A type theory with partially defined functions and pattern
	matching
Message-ID: <044401c66876$0e092db0$a0290c81@ad.kent.ac.uk>

Since many have come to discuss partially defined functions and pattern
matching after I gave the talk in TYPES2006 last week.

There is a new version you can download from my home page if you are
interested. Comments and suggestions are welcome.

http://www.cs.kent.ac.uk/people/staff/yl41/TPF.ps

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent


From scd at doc.ic.ac.uk  Tue Apr 25 16:21:04 2006
From: scd at doc.ic.ac.uk (Sophia Drossopoulou)
Date: Tue, 25 Apr 2006 21:21:04 +0100
Subject: [TYPES] completeness of subtype judgments
Message-ID: <444E84B0.3070107@doc.ic.ac.uk>

Dave Clarke and I have been wondering whether there is any work
on the completeness of type systems, in the presence of subtyping
and rather intricate types.

We have a way of defining what completeness is, but proving it for
a  particular system seems daunting.

Here is how we would define completeness of a type system:

      1) Define a judgment \Gamma |- T <: T? with the obvious meaning

      2) Define the denotation of a type T for a given stack S
         and heap H, as
                             [[T]]_{S,H}
         as the set of all values with type T in S and H.
        (We need to consider the stack S because we have path-dependent
         types, i.e.  T may mention entities from S.)

      3) Define a judgment \Gamma |- S, H to express when a
         stack S and heap H agree with an environment \Gamma.

      4)  The subtyping system is complete, iff
          \forall \Gamma, T and T?
              (\forall S, H:
               \Gamma |- S,H => [[T]]_{S,H} \subset [[T?]]_{S,H} )
              =>
              ( \Gamma |- T <: T? )

Our question is whether there are alternative formulations of
completeness, and, more importantly, whether there is work proving
such completeness.

Cheers and thanks,

Dave Clarke and Sophia Drossopoulou

-- ===================================================================
Sophia Drossopoulou Department of Computing,
http://www.doc.ic.ac.uk/~scd/index.html

From cbj at it.uts.edu.au  Tue Apr 25 19:51:00 2006
From: cbj at it.uts.edu.au (Barry Jay)
Date: Wed, 26 Apr 2006 09:51:00 +1000
Subject: [TYPES] ....pattern matching
In-Reply-To: <044401c66876$0e092db0$a0290c81@ad.kent.ac.uk>
References: <044401c66876$0e092db0$a0290c81@ad.kent.ac.uk>
Message-ID: <444EB5E4.2090703@it.uts.edu.au>

Speaking of pattern matching,

it is more than just a convenience. By allowing any term to be a 
pattern, one can obtain new forms of polymorphism that allow generic 
queries (updating, searching, etc) to treat query parameters as 
arguments, and to apply queries to arbitrary data structures. A pure 
(untyped) version of pattern calculus was presented at ESOP last month 
(joint work with Delia Kesner). An overview and various papers 
(including an improved version of pure calculus) can be found at   
http://www-staff.it.uts.edu.au/~cbj/patterns/

The terms of the pure pattern calculus are given by

t ::= x  |  t t  |   t -->_theta  t

where p -->_theta s is a case with pattern p, body s and binding 
variables theta. The only reduction rule is the match rule, which 
generalises beta reduction. 

A typed version of the pattern calculus able to support the five forms 
of polymorphism identified will be available shortly. It will use fairly 
conventional types (System F plus type applications and some constants) 
but novel type derivation rules for handling the extension of a function 
with a new case.  Further work would be required to integrate this into 
a version suitable for handling dependent types etc. along the lines 
suggested by Yong Luo.

Yours,
Barry Jay



Yong Luo wrote:

>[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>Since many have come to discuss partially defined functions and pattern
>matching after I gave the talk in TYPES2006 last week.
>
>There is a new version you can download from my home page if you are
>interested. Comments and suggestions are welcome.
>
>http://www.cs.kent.ac.uk/people/staff/yl41/TPF.ps
>
>Yong
>==============================
>Dr. Yong Luo
>Computing Laboratory
>University of Kent
>
>  
>


From gerwin.klein at nicta.com.au  Tue Apr 25 17:51:25 2006
From: gerwin.klein at nicta.com.au (Gerwin Klein)
Date: Wed, 26 Apr 2006 07:51:25 +1000
Subject: [TYPES] completeness of subtype judgments
In-Reply-To: <444E84B0.3070107@doc.ic.ac.uk>
References: <444E84B0.3070107@doc.ic.ac.uk>
Message-ID: <200604260751.25955.gerwin.klein@nicta.com.au>

Dear Sophia,

if I remember correctly, Alessandro Coglio had something like this for his JVM 
subroutine type system in 

A. Coglio, "Simple Verification Technique for Complex Java Bytecode 
Subroutines", Concurrency and Computation: Practice and Experience, 16
(7):647-670, 2004

Cheers,
Gerwin

On Wednesday 26 April 2006 06:21, Sophia Drossopoulou wrote:
>       1) Define a judgment \Gamma |- T <: T? with the obvious meaning
>
>       2) Define the denotation of a type T for a given stack S
>          and heap H, as
>                              [[T]]_{S,H}
>          as the set of all values with type T in S and H.
>         (We need to consider the stack S because we have path-dependent
>          types, i.e.  T may mention entities from S.)
>
>       3) Define a judgment \Gamma |- S, H to express when a
>          stack S and heap H agree with an environment \Gamma.
>
>       4)  The subtyping system is complete, iff
>           \forall \Gamma, T and T?
>               (\forall S, H:
>                \Gamma |- S,H => [[T]]_{S,H} \subset [[T?]]_{S,H} )
>               =>
>               ( \Gamma |- T <: T? )
>
> Our question is whether there are alternative formulations of
> completeness, and, more importantly, whether there is work proving
> such completeness.

From Giuseppe.Castagna at ens.fr  Wed Apr 26 05:56:59 2006
From: Giuseppe.Castagna at ens.fr (Giuseppe Castagna)
Date: Wed, 26 Apr 2006 11:56:59 +0200
Subject: [TYPES] completeness of subtype judgments
In-Reply-To: <444E84B0.3070107@doc.ic.ac.uk>
References: <444E84B0.3070107@doc.ic.ac.uk>
Message-ID: <444F43EB.40207@ens.fr>

Sophia Drossopoulou wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Dave Clarke and I have been wondering whether there is any work
> on the completeness of type systems, in the presence of subtyping
> and rather intricate types.
> 

Yes definitively there is one!

In our paper at LICS 2005, Rocco De Nicola, Daniele Varacca, and I 
defined a subtyping relation for the following types for the pi-calculus

    t ::= ch+(t)  | ch-(t)  |  t\/t  |   t/\t  |  not(t) | Top

which is complete with respect to the following interpretation of types

[[t]] = { v | v:t }

more precisely, [[ ch+(t) ]] is the set of all channels [1] on which you 
can receive message of type t, [[ ch+(t) ]] is the set of all channels 
[1] on which you can safely write message of type t, while the 
combinator have set theoretic interpretation, that is [[s \/ t ]] is the 
union of [[s]] and [[ t ]], [[s /\ t ]] is the intersection of [[s]] and 
[[ t ]], and [[not(t)]] is the complement of [[t]] with respect to the 
set of all (well-typed) values.

I guess this is exactly what you were asking for.

The paper is available on line at

http://www.cduce.org/papers/semantic_pi.pdf

it is a little bit technical. If you want to have a much less technical 
introduction you can consult my invited paper at ICTCS "Semantic 
subtyping: challenges, perspectives, and open problems" (LNCS available 
on line at

ftp://ftp.di.ens.fr/pub/users/castagna/ictcs05a.pdf

Also, Mariangiola Dezani, Daniele Varacca and I studied the "local" 
variant (you cannot read on an input channel, that is you do not have 
the ch+(t) type) of the above calculus and proved how it can 
type-faithfully encode a lambda-calculus with union intersection 
negation arrow products and recursive types. The local variant is quite 
interesting because the subtyping relation is *far* simpler and more 
tractable that the full case (though the latter is decidable). The paper 
is currently under submission but it is accessible (though not 
publicized) at the following URL:

ftp://ftp.di.ens.fr/pub/users/castagna/cpi-encode.pdf

Comments and suggestions are very welcome.

---Beppe---


[1] Channels here are intended as channel /names/, which must thus be 
differentiated from channel /variables/, since values must be closed. In 
practice for channel names we use the standard definition given by 
Barendregt for for lambda-calculus names, that is channels which cannot 
be substituted.


From Giuseppe.Castagna at ens.fr  Wed Apr 26 07:43:08 2006
From: Giuseppe.Castagna at ens.fr (Giuseppe Castagna)
Date: Wed, 26 Apr 2006 13:43:08 +0200
Subject: [TYPES] CORRIGENDA: completeness of subtype judgments
In-Reply-To: <444F43EB.40207@ens.fr>
References: <444E84B0.3070107@doc.ic.ac.uk> <444F43EB.40207@ens.fr>
Message-ID: <444F5CCC.8050308@ens.fr>

Giuseppe Castagna wrote:
>> Dave Clarke and I have been wondering whether there is any work
>> on the completeness of type systems, in the presence of subtyping
>> and rather intricate types.
>>
> 
> Yes definitively there is one!
> 
> In our paper at LICS 2005, Rocco De Nicola, Daniele Varacca, and I 
> defined a subtyping relation for the following types for the pi-calculus
> 
>    t ::= ch+(t)  | ch-(t)  |  t\/t  |   t/\t  |  not(t) | Top
> 


I am sorry Sophia, I have done a slight confusion, since I thought you 
were speaking of pi-calculus (because of the proximity of a mail in by 
mailbox asking references on it). What I said in my previous mail does 
apply to your question, but if you were thinking of lambda-calculus 
rather than pi-calculus, then there is much a better reference, that is 
"Semantic subtyping", another LICS paper (LICS 2002) by Alain Frisch, 
Veronique Benzaken and myself. It is available at

    ftp://ftp.di.ens.fr/pub/users/castagna/lics02.pdf

Here we consider a lambda calculus with the following (possibly 
recursive) types:

t ::=  t -> t  |  t x t  |  t\/t  |   t/\t  |  not(t) | Top


and which is complete with respect to the interpretation of types you asked

  [[t]] = { v | v:t }

where v ranges over values.
So arrow types are interpreted as set of (closed) lambda-expressions of 
that type, and combinators are once more interpreted as the 
corresponding set-theoretic operations.

This paper is very technical too, in particular there is a circularity 
between the definition of [[t]] = { v | v:t } and the subtyping relation 
which cannot be dealt in a straightforward way. More generally, this 
relates to the difficulty of giving a set-theoretic interpretation of 
arrow types (this is *not* a term model).
Therefore if you want to have an idea about the general technique, I 
*strongly* suggest first to consult my joint keynote talk at ICALP 2006 
and PPDP 2006 "A gentle introduction to semantic subtyping" available at

   http://www.di.ens.fr/users/castagna/papers/icalp-ppdp05.pdf

Further insight is given by the ICTCS paper I cited in my previous mail, 
mail that is of course valid for what concerns your topic for concurrent 
languages. A journal version of the cited work in LICS 2002 should be 
ready in few days and I will be happy to send it to all persons interested

---Beppe---

From Alain.Frisch at inria.fr  Wed Apr 26 08:42:14 2006
From: Alain.Frisch at inria.fr (Alain Frisch)
Date: Wed, 26 Apr 2006 14:42:14 +0200
Subject: [TYPES] completeness of subtype judgments
In-Reply-To: <444E84B0.3070107@doc.ic.ac.uk>
References: <444E84B0.3070107@doc.ic.ac.uk>
Message-ID: <444F6AA6.20409@inria.fr>

Sophia Drossopoulou wrote:
> Dave Clarke and I have been wondering whether there is any work
> on the completeness of type systems, in the presence of subtyping
> and rather intricate types.

You might be interested in our paper at LICS 2002 (_Semantic subtyping_,
A. Frisch, G. Castagna, and V. Benzaken). An informal introduction
can be found in _A Gentle Introduction to Semantic Subtyping_ and the
full development is in my PhD thesis (in French); a journal version is
in preparation. ---> http://www.cduce.org/papers.html

The system in these papers includes type constructors (products,
records, arrows), Boolean connectives (finite union and intersection,
negation) and recursive types. Types are interpreted as sets of values
and Boolean connectives are interpreted purely set-theoretically,
so e.g. the negation of a type t contains all the (well-typed) values
which don't have type t. The calculus is a CBV lambda-calculus,
with overloaded first-class functions (whose explicit signature
can mention several arrow types) and dynamic type-dispatch.

The subtyping relation is defined such that it corresponds exactly
to set inclusion. If we write [[t]] for the set of values of type t
[[t]] = { v | |- v : t }, then:

(*) t <: t'  iff  [[t]] \subset [[t']]

Clearly, because of the subsumption rule in the type system
and because values are expressions, we also have:

t <: t'  iff \forall \Gamma, e.  \Gamma |- e : t  ==>  \Gamma |- e : t'

where e stands for expressions. We have another completeness result
which relates the subtyping of arrow types and the dynamic semantics.

The trick to obtain (*) was to actually start from (*)
as a definition for <:, and then derive an axiomatic formulation and an
algorithm (we did this work for a concrete programming language).  In
order to avoid the circularity between the subtyping relation, the type
system and the type-directed semantics, we developed a bootstrapping
approach.


Cheers,

 Alain Frisch

From ostermann at informatik.tu-darmstadt.de  Tue Jul  4 06:13:35 2006
From: ostermann at informatik.tu-darmstadt.de (Klaus Ostermann)
Date: Tue, 04 Jul 2006 12:13:35 +0200
Subject: [TYPES] Systematically testing type systems
Message-ID: <44AA3F4F.1090906@informatik.tu-darmstadt.de>

Hi all,

I hope this is not a stupid question, but I wonder whether it is feasible to 
test the soundness of a type checker by enumerating all programs in the 
language, reducing each program one step (assuming we have a small-step 
interpreter and a language where the full execution state is in the program 
itself) and checking whether subject reduction holds. If the enumeration of all 
programs would be smart enough (i.e., produce only syntactically correct 
programs; no two programs in the enumeration are alpha-equivalent) I could 
imagine that it would be feasible to test a type checker for all programs less 
than X bytes in size, where X is a reasonable number (e.g., 1KB) - at least for 
minimalistic languages as they are common in type research.

Has this ever been tried, or is it obvious that it would not work in practice?

Klaus Ostermann

From james.cheney at gmail.com  Wed Jul  5 10:57:13 2006
From: james.cheney at gmail.com (James Cheney)
Date: Wed, 5 Jul 2006 15:57:13 +0100
Subject: [TYPES] Systematically testing type systems
In-Reply-To: <44AA3F4F.1090906@informatik.tu-darmstadt.de>
References: <44AA3F4F.1090906@informatik.tu-darmstadt.de>
Message-ID: <814253dd0607050757y2221760bg642cd15525b39465@mail.gmail.com>

This is not difficult to do in a logic programming language that supports
higher-order or nominal abstract syntax, such as lambdaProlog, Twelf, or
alphaProlog, using "generate-and-test"; the tricky part is getting the tests
right and setting up the search in such a way that you don't miss obvious
short counterexamples yet still terminate in a small amount of time (my
boredom threshold is five seconds).  Automated assertion checking has also
been investigated in a general (constraint) logic programming and in Haskell
(QuickCheck).  I'm not aware of any prior research on applying this idea
specifically to type systems.

Coincidentally, I wrote a short (and very very preliminary) paper on doing
this in alphaProlog for the upcoming Workshop on Mechanizing Metatheory;
this seems like as good a time as any to mention it.  It is not clear to me
how far an exhaustive search approach can be pushed, since the number of
well-typed programs of size n is still exponential in n; something like
QuickCheck's random checking, but guided by the type system and operational
semantics, might be a better way.  However, even doing an exhaustive search
for "small" counterexamples seems likely to be helpful, at least as a sanity
check for trivial bugs.

If you want to have a look at the paper draft, it's online at

http://homepages.inf.ed.ac.uk/jcheney/publications/wmm06-draft.pdf

Big caveat: alphaProlog is not that well supported right now and the code
for automatic checking is not in a public release yet.

Questions, comments, and fisticuffs welcome.

--James

On 7/4/06, Klaus Ostermann <ostermann at informatik.tu-darmstadt.de> wrote:
>
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
> Hi all,
>
> I hope this is not a stupid question, but I wonder whether it is feasible
> to
> test the soundness of a type checker by enumerating all programs in the
> language, reducing each program one step (assuming we have a small-step
> interpreter and a language where the full execution state is in the
> program
> itself) and checking whether subject reduction holds. If the enumeration
> of all
> programs would be smart enough (i.e., produce only syntactically correct
> programs; no two programs in the enumeration are alpha-equivalent) I could
> imagine that it would be feasible to test a type checker for all programs
> less
> than X bytes in size, where X is a reasonable number (e.g., 1KB) - at
> least for
> minimalistic languages as they are common in type research.
>
> Has this ever been tried, or is it obvious that it would not work in
> practice?
>
> Klaus Ostermann
>

From matthias at ccs.neu.edu  Wed Jul  5 11:12:53 2006
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Wed, 5 Jul 2006 11:12:53 -0400
Subject: [TYPES] Systematically testing type systems
In-Reply-To: <44AA3F4F.1090906@informatik.tu-darmstadt.de>
References: <44AA3F4F.1090906@informatik.tu-darmstadt.de>
Message-ID: <C80975BF-DD52-4F29-9671-D8F00BAA5064@ccs.neu.edu>


On Jul 4, 2006, at 6:13 AM, Klaus Ostermann wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Hi all,
>
> I hope this is not a stupid question, but I wonder whether it is  
> feasible to
> test the soundness of a type checker by enumerating all programs in  
> the
> language, reducing each program one step (assuming we have a small- 
> step
> interpreter and a language where the full execution state is in the  
> program
> itself) and checking whether subject reduction holds. If the  
> enumeration of all
> programs would be smart enough (i.e., produce only syntactically  
> correct
> programs; no two programs in the enumeration are alpha-equivalent)  
> I could
> imagine that it would be feasible to test a type checker for all  
> programs less
> than X bytes in size, where X is a reasonable number (e.g., 1KB) -  
> at least for
> minimalistic languages as they are common in type research.
>
> Has this ever been tried, or is it obvious that it would not work  
> in practice?

That was one of the goals behind our PLT Redex tool (see RTA 2004,  
Aachen): test then verify.

It's not quite there yet. I can imagine that the performance of a  
well-tuned logic-based system, such as the early INRIA efforts, could  
be better.

-- Matthias


From david.nospam.hopwood at blueyonder.co.uk  Wed Jul  5 12:31:56 2006
From: david.nospam.hopwood at blueyonder.co.uk (David Hopwood)
Date: Wed, 05 Jul 2006 17:31:56 +0100
Subject: [TYPES] Systematically testing type systems
In-Reply-To: <44AA3F4F.1090906@informatik.tu-darmstadt.de>
References: <44AA3F4F.1090906@informatik.tu-darmstadt.de>
Message-ID: <44ABE97C.3060802@blueyonder.co.uk>

Klaus Ostermann wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hi all,
> 
> I hope this is not a stupid question, but I wonder whether it is feasible to 
> test the soundness of a type checker by enumerating all programs in the 
> language, reducing each program one step (assuming we have a small-step 
> interpreter and a language where the full execution state is in the program 
> itself) and checking whether subject reduction holds. If the enumeration of all 
> programs would be smart enough (i.e., produce only syntactically correct 
> programs; no two programs in the enumeration are alpha-equivalent) I could 
> imagine that it would be feasible to test a type checker for all programs less 
> than X bytes in size, where X is a reasonable number (e.g., 1KB) - at least for 
> minimalistic languages as they are common in type research.
> 
> Has this ever been tried, or is it obvious that it would not work in practice?

It is obvious that it would not work in practice for programs up to 1 Kbyte.
It could only work for programs up to a few tokens in length.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>



From streicher at mathematik.tu-darmstadt.de  Fri Jul 14 08:11:53 2006
From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher)
Date: Fri, 14 Jul 2006 14:11:53 +0200 (CEST)
Subject: [TYPES] semantics of `quote'
Message-ID: <200607141211.k6ECBruo027638@fb04209.mathematik.tu-darmstadt.de>

Does anyone know of a reference to work on (denotational) semantics of
`quote' constructs in functional languages like LISP?

Probably there is nothing like that since the operational evaluation rule

     quote M -> "M"   (where "M" is e.g. a Goedel number for M)

induces an onservational equivalence coinciding with syntactic equality.
Well, there should be variants if quote is call-by-value where the meaning
of quote M is a Goedel number of the weak head normal form of M.

More generally, one might ask for quote constructs  \libqu  where
\libqu M -> "N" such that M and N have the same denotation (whatever this is).

The reason why I am asking this on TYPES is that languages with (a kind of)
quote seem to be necessary for constructing realizabilty models of Martin-Loef
type theory validating Church's Thesis

    (\Pi f : N \to N) (\Sigma e : N) (\Pi n:N) {e}(n) = f(n)

a question brought up recently by M.Maietti and G. Sambin.

My impression is that a quote construct seems to be incompatible with
the \xi-rule
                    M = N
                 -------------
                  \x.M = \x.N

Best regards, Thomas

From Tim.Sweeney at epicgames.com  Fri Jul 14 14:35:27 2006
From: Tim.Sweeney at epicgames.com (Tim Sweeney)
Date: Fri, 14 Jul 2006 14:35:27 -0400
Subject: [TYPES] semantics of `quote'
In-Reply-To: <200607141211.k6ECBruo027638@fb04209.mathematik.tu-darmstadt.de>
Message-ID: <8A4FE0C7AD1E894EA308C998C0A2648901B8FA0E@ZEUS.epicgames.net>

I looked into this a while ago and found two ways of approaching a
"quote" operation.

The first is to allow one to dynamically convert any value to its Godel
number or something similar (e.g. an AST representation).  Such an
operation has a sweeping impact on the language's properties.

For example, adding "quote" to a language with extensional equality
would make its equality inconsistent with observable equivalence:
quote(f) and quote(g) would reveal that f=lambda(x:int)=x+1 and
g=lambda(x:int)=1+x are distinct.

Adding "quote" to a language respecting the parametricity property would
break parametricity:  You would write a function like forall(t:type)
lambda(x:t) quote(x) which converts a value of any type to an integer
and thus distinguish values of universal type.

The second, and less devastating, approach would be to expose "quote" as
a purely syntactic feature, where you could write code like:

f=quote {lambda(x:int) x+1}

And then, from f, you could extract both the semantic value and the
syntactic value.  For example, f.value would return the function
lambda(x:int) x+1, and f.quote would return a Godel representation,
textual representation, abstract syntax tree representation, or some
other representation that does not obey the parametricity and
extensionality properties you would expect the value itself to obey.

The extent of the "quote" operation here is just the syntactic span of
code inside the quote.  For example, in forall(t:type) lambda(x:t) quote
{x}, the quote {x} would just return some syntactic indicator of a
reference to a bound variable (a local property), rather than
introspecting the actual value of x and returning some syntactic
representation of it (a global property violating extensionality and
parametricity).

This issue is important to many languages, because programmers have a
general desire for both "nice properties" (parametricity,
extensionality, etc) and for the ability to extract metadata from their
program in order to enable automation of certain operations (graphical
user interface creation, implementing persistence, etc).  An explicit
syntactic quote operation like this enables both capabilities to be
mixed and matched explicitly, without violating nice global properties
of programs.

-Tim

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu
[mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Thomas
Streicher
Sent: Friday, July 14, 2006 8:12 AM
To: types-list at lists.seas.upenn.edu
Subject: [TYPES] semantics of `quote'

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

Does anyone know of a reference to work on (denotational) semantics of
`quote' constructs in functional languages like LISP?

Probably there is nothing like that since the operational evaluation
rule

     quote M -> "M"   (where "M" is e.g. a Goedel number for M)

induces an onservational equivalence coinciding with syntactic equality.
Well, there should be variants if quote is call-by-value where the
meaning
of quote M is a Goedel number of the weak head normal form of M.

More generally, one might ask for quote constructs  \libqu  where
\libqu M -> "N" such that M and N have the same denotation (whatever
this is).

The reason why I am asking this on TYPES is that languages with (a kind
of)
quote seem to be necessary for constructing realizabilty models of
Martin-Loef
type theory validating Church's Thesis

    (\Pi f : N \to N) (\Sigma e : N) (\Pi n:N) {e}(n) = f(n)

a question brought up recently by M.Maietti and G. Sambin.

My impression is that a quote construct seems to be incompatible with
the \xi-rule
                    M = N
                 -------------
                  \x.M = \x.N

Best regards, Thomas

From U.S.Reddy at cs.bham.ac.uk  Sat Jul 15 02:50:05 2006
From: U.S.Reddy at cs.bham.ac.uk (Uday Reddy)
Date: Sat, 15 Jul 2006 07:50:05 +0100
Subject: [TYPES] semantics of `quote'
In-Reply-To: <200607141211.k6ECBruo027638@fb04209.mathematik.tu-darmstadt.de>
References: <200607141211.k6ECBruo027638@fb04209.mathematik.tu-darmstadt.de>
Message-ID: <17592.36893.178511.419639@preston.cs.bham.ac.uk>

Dear Thomas,

The standard approach to dealing with quotation is to think of the
language as operating at two levels: one inside the quotation brackets
and one outside.  An "unquote" operation can take you from the upper
level (quotation level) to the lower level (denotation level).  This
idea can also be generalised to multiple levels.

A search on Google Scholar for "two-level languages" or "multi-stage
languages" will take you to the work of Fleming Nielson, Eugenio Moggi
and others.

Cheers,
Uday

Thomas Streicher writes:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Does anyone know of a reference to work on (denotational) semantics of
> `quote' constructs in functional languages like LISP?
> 
> Probably there is nothing like that since the operational evaluation rule
> 
>      quote M -> "M"   (where "M" is e.g. a Goedel number for M)
> 
> induces an onservational equivalence coinciding with syntactic equality.
> Well, there should be variants if quote is call-by-value where the meaning
> of quote M is a Goedel number of the weak head normal form of M.
> 
> More generally, one might ask for quote constructs  \libqu  where
> \libqu M -> "N" such that M and N have the same denotation (whatever this is).
> 
> The reason why I am asking this on TYPES is that languages with (a kind of)
> quote seem to be necessary for constructing realizabilty models of Martin-Loef
> type theory validating Church's Thesis
> 
>     (\Pi f : N \to N) (\Sigma e : N) (\Pi n:N) {e}(n) = f(n)
> 
> a question brought up recently by M.Maietti and G. Sambin.
> 
> My impression is that a quote construct seems to be incompatible with
> the \xi-rule
>                     M = N
>                  -------------
>                   \x.M = \x.N
> 
> Best regards, Thomas
> 
> 


From streicher at mathematik.tu-darmstadt.de  Tue Jul 18 09:33:23 2006
From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher)
Date: Tue, 18 Jul 2006 15:33:23 +0200 (CEST)
Subject: [TYPES] a summary of the responses to my question on `quote'
Message-ID: <200607181333.k6IDXNUN016071@fb04209.mathematik.tu-darmstadt.de>

First of all thanks a lot for the various replies on my question about
semantics of `quote'. 
As one of those people who have replied asked me to give a digest 
of the answers which I do here (with answers compiled for convenience).

(1) The most helpful reply was a pointer to a paper by M.Wand showing that
quote makes the usual laws of \lambda-calculus incompatible with observationa
equivalence (since by quote one may separate terms otherwise having the
same denotational meaning).

(2) There is the work on 2-level languages and more generally multi-level 
languages by Nielsen&Nielsen, Danvy&Malmkjaer, Moggi etc.

(3) Related to this is the work on propositions-as-types for modal logic
by the Goubault brothers and later by Pfenning at al. Here the idea is
that \box A is the type of terms of type A. Typically eval : \box A -> A
and quote is the constructor for \box introduction as in

    x_1 : \box A_1, ..., x_n \box A_n |- t : B
  ---------------------------------------------------------
    x_1 : \box A_1, ..., x_n \box A_n |- quote t : \box B

For this I know a nice categorical semantics. Let \C be the free ccc 
modelling \lambda-calculus and let \E = Psh(\C) = \Set^{\C^\op}. Then there
is an adjunction \Delta -| \Gamma : \E -> Set inducing a (non-enriched) 
comonad \box = \Delta o \Gamma on \E. The lack of enrichment is responsible 
for the split contexts.

Both (2) and (3) are characterized by a careful hierarchization 
(in (3) this is done by \box). In approach (3) (which I, personally, 
understand better than (2)) this leads to the consequence that we don't
have a map quote_A : A -> \box A (which would be ridiculous from a modal
logic point of view!). Instead we just have a "meta-operation"

          |- t : A
    ---------------------
     |- quote t : \box A 

I think there is related work by S.Artemov and his collaborators. 
For a survey see

    "Explicit Provability and Constructive Semantics" 
    Bull. Symbolic Logic  7  (2001),  no. 1, 1--36.

Both (2) and (3) fall short of dealing with the "real quote" which is of
type quote_A : A -> \box A. As they don't have this the laws of lambda-calculus
remain undamaged.

(4) There are 2 papers by G.Meredith and M.Radestock which study a variant
of \pi-calculus with quote with the intention of replacing names of processes
by their code.  Seems to be though stuff which would take me more time 
to study.

(5) Though not mentioned in the replies there is some work by J.-L.~Krivine  

    Dependent choice, `quote' and the clock.
    Theoret. Comput. Sci. 308 (2003), no. 1-3, 259--276.

where he uses \lambda-calculus with quote to realize dependent choice.
It is well known that dependent choice is validated by Kleene's number
realizability where quote is given by identity. Introducing quote into
\lambda-calculus has a similar effect as explained in section 5.2 of
J.Longley's "Matching typed and untyped realizability" pp.74-100 of
ENTCS 23(1) 1999).


In any case the responses have confirmed my impression that for realizing
Church's Thesis in Martin-Loef type theory there has to be `quote' operator
in the underlying untyped model of computation and that this `quote' operator
destroys the usual equalities of \lambda-calculus.

Thomas Streicher

=============================================================================

Vincent DANOS :

Hi Thomas

This may be not what you need, but i remember a paper by Jean and  
Eric Goubault
setting Curry-Howard correspondence for some modal logic where quote
is used to handle the modal part.

Best,
Vincent.

=============================================================================
Nick BENTON :

That eval and quote trivialize contextual equivalence is (apparently) in

Albert Meyer. 13 puzzles in programming logic. Workshop on Formal
Software Development. 1984

which is referenced in this nice paper

Mitch Wand. The theory of fexprs is trivial. Lisp and Symbolic
Computation. 1998

which treats an untyped lambda calculus with a reification operator that
yields quoted values represented as lambda terms in a Churchy style. In
this case contextual equivalence is alpha equivalence.

At the other end of the scale, languages like MetaML give you quoting
without any real ability to introspect on the quoted value - all you can
do with a code<T> is turn it back into a T at a later stage. So that's
not going to drastically mess up contextual equivalence (and there are
various interesting models in the literature).

But I don't know what lies between those two extremes (except, of
course, for the trivial observation that adding something like call/cc
gives you extra discriminatory power without collapsing everything -
that's kind of a limited form of reflection).

  Nick 


===========================================================================

Tim SWEENEY :

I looked into this a while ago and found two ways of approaching a
"quote" operation.

The first is to allow one to dynamically convert any value to its Godel
number or something similar (e.g. an AST representation).  Such an
operation has a sweeping impact on the language's properties.

For example, adding "quote" to a language with extensional equality
would make its equality inconsistent with observable equivalence:
quote(f) and quote(g) would reveal that f=lambda(x:int)=x+1 and
g=lambda(x:int)=1+x are distinct.

Adding "quote" to a language respecting the parametricity property would
break parametricity:  You would write a function like forall(t:type)
lambda(x:t) quote(x) which converts a value of any type to an integer
and thus distinguish values of universal type.

The second, and less devastating, approach would be to expose "quote" as
a purely syntactic feature, where you could write code like:

f=quote {lambda(x:int) x+1}

And then, from f, you could extract both the semantic value and the
syntactic value.  For example, f.value would return the function
lambda(x:int) x+1, and f.quote would return a Godel representation,
textual representation, abstract syntax tree representation, or some
other representation that does not obey the parametricity and
extensionality properties you would expect the value itself to obey.

The extent of the "quote" operation here is just the syntactic span of
code inside the quote.  For example, in forall(t:type) lambda(x:t) quote
{x}, the quote {x} would just return some syntactic indicator of a
reference to a bound variable (a local property), rather than
introspecting the actual value of x and returning some syntactic
representation of it (a global property violating extensionality and
parametricity).

This issue is important to many languages, because programmers have a
general desire for both "nice properties" (parametricity,
extensionality, etc) and for the ability to extract metadata from their
program in order to enable automation of certain operations (graphical
user interface creation, implementing persistence, etc).  An explicit
syntactic quote operation like this enables both capabilities to be
mixed and matched explicitly, without violating nice global properties
of programs.

-Tim

==========================================================================
Greg MEREDITH

Thomas,

i worked out a semantics of this sort of operation in a concurrency setting.
See

L. Gregory Meredith<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/m/Meredith:L=_Gregory.html>,
Matthias Radestock: A Reflective Higher-order Calculus. Electr. Notes Theor.
Comput. Sci. 141<http://www.informatik.uni-trier.de/%7Eley/db/journals/entcs/entcs141.html#MeredithR05>(5):
49-67 (2005)

L. Gregory Meredith<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/m/Meredith:L=_Gregory.html>,
Matthias Radestock: Namespace Logic: A Logic for a Reflective Higher-Order
Calculus. TGC 2005<http://www.informatik.uni-trier.de/%7Eley/db/conf/tgc/tgc2005.html#MeredithR05>:
353-369

Best wishes,

--greg

=============================================================================
Udday REDDY

Dear Thomas,

The standard approach to dealing with quotation is to think of the
language as operating at two levels: one inside the quotation brackets
and one outside.  An "unquote" operation can take you from the upper
level (quotation level) to the lower level (denotation level).  This
idea can also be generalised to multiple levels.

A search on Google Scholar for "two-level languages" or "multi-stage
languages" will take you to the work of Fleming Nielson, Eugenio Moggi
and others.

Cheers,
Uday

===========================================================================

Frank PFENNING

Hi Thomas,

  it may not directly answer your question, but you might find

Aleksandar Nanevski and Frank Pfenning.  Staged computation with names
and necessity.  Journal of Functional Programming, 15(6):837-891,
November 2005.
http://www.cs.cmu.edu/~fp/papers/jfp05.pdf

  somewhat relevant.  This follows work

Rowan Davies and Frank Pfenning.  A modal analysis of staged
computation.  Journal of the ACM, 48(3):555-604, May 2001.
http://www.cs.cmu.edu/~fp/papers/jacm00.pdf

The most recent (and now purely type-theoretic) approach to this can
be found in

Contextual Modal Type Theory 
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 
Submitted, September 2005. 
http://www.cs.cmu.edu/~fp/papers/cmtt05.pdf

which has recently been accepted to ToCL.

  Best,
  Frank


From emakarov at cs.indiana.edu  Sun Jul 23 23:05:10 2006
From: emakarov at cs.indiana.edu (emakarov)
Date: Sun, 23 Jul 2006 23:05:10 -0400
Subject: [TYPES] Lambda calculus with callcc and Moggi's monadic metalanguage
Message-ID: <000b01c6aecd$fda697c0$1a89389c@ads.iu.edu>

I am studying simply-typed call-by-value (CBV) lambda calculus with 
Felleisen's control operator C, or with Scheme's call/cc. For my goal 
(removing useless subterms of singleton type) I need beta reductions which 
are more general than CBV ones, namely, which allow a function's argument to 
be any "pure" term and not necessarily a value. Here "pure" means that the 
term does not invoke control operators, i.e., does not cause side effects.

I think that it would be convenient to translate this lambda calculus into 
Moggi's monadic metalanguage (MML) which explicitly separates terms with 
side effects from pure terms. Terms with side effects have type (M sigma) 
where M is a new type constructor, and they have to be evaluated using a 
special construct do x <- t1; t2 (computational reductions). Pure terms, on 
the other hand, admit arbitrary beta reductions.

However, I believe that just defining the translation does not solve 
anything. One has to actually prove that beta reductions on pure term do not 
change the program's answer. So one has to prove something like bisimulation 
between computational and beta reductions.

I am wondering if somebody has defined this translation from lambda calculus 
with control operators into MML and proved the corresponding properties. 
More precisely, I'd like to know if

(1) there is a translation which inserts the least number of M's (for 
example, it should *not* change every function type sigma1 -> sigma2 into 
sigma1 -> M sigma2). Ideally, only terms with side effects should have type 
starting with M.

(2) it is proved that arbitrary beta reductions do not change the program's 
answer.

Thank you for your help.

Yevgeniy


From dimitriv at cis.upenn.edu  Mon Aug 21 18:19:55 2006
From: dimitriv at cis.upenn.edu (Dimitrios Vytiniotis)
Date: Mon, 21 Aug 2006 18:19:55 -0400
Subject: [TYPES] logical relations and ctx equivalence
Message-ID: <44EA318B.9090809@cis.upenn.edu>

Dear TYPES readers,

    Consider the simplest syntactic relational interpretation of
System-F types as sets of pairs of closed values.  Quantification is
over arbitrary value relations. The semantics is call by value and
terminating. [Definitions can be found at the end of this message]

First, I think it is an easy corollary of the fundamental theorem that
the logical relation is contained in ctx equivalence (I am using
ground equivalence, actually), i.e. that:

Proposition: If (e1,e2) in (interp[t] nil nil)
              then forall contexts C : t -> Int,
              C[e1] and C[e2] evaluate to the same literal.

What I am asking is whether we know that it is complete:

Question: If forall C : t -> Int,
              C[e1] and C[e2] evaluate to the same literal
           then (e1,e2) in (interp[t] nil nil).

It seems that an important step towards completeness is showing that
the logical relation is an equivalence-respecting one. Then, for
example, Pitts' work [ATTAPL clapter] uses TT-closures, and Harper &
Birkedal's paper [Relational interpetation for recursive types in an
Operational Setting] builds the logical relation between equivalence
classes of expressions alltogether (and does not handle polymorphism,
but this probably does not matter). Are all these constructions
necessary? Is there a negative result or an easy counterexample that
the plain-old definition does not give a big enough relation, or do we
not have a direct proof method, or do we not know? Any pointers to
related work would be very useful.

Thank you,
--Dimitrios Vytiniotis


Informal Definitions
=====================

Types:   t ::= a | t -> t | Int | forall a.t
Terms:   e ::= x | \(x:t).e | e e | e [t] | int_literal

Type envs:  m : TyVar -> (Value,Value)
             d : TyVar -> (Type,Type)
	    d1(a) = fst (d(a))
             d2(a) = snd (d(a))

VRel(t1,t2) = set of relations between pairs of
               closed values of types t1 and t2

interp[a] m d  = m(a)
interp[Int] m d = identity on integer literals
interp[t1->t2] m d =
    { (v1,v2) | v1 : d1(t1->t2) and
                v2 : d2(t1->t2) and
      forall x1 x2. (x1,x2) in (interp[t1] m d) =>
       (v1 x1, v2 x2) evaluate to (w1,w2) in (interp[t2] m d) }
interp[forall a.t] m d =
    { (v1,v2) | v1: d1(forall a.t) and
                v2: d2(forall a.t) and
      forall t1 t2 r. r in VRel(t1,t2) =>
       (v1 [t1], v2 [t2]) evaluate to (w1,w2)
                            in (interp[t] (m,a->r) (d,a->(t1,t2)))}



From eijiro.sumii at gmail.com  Sat Sep 30 21:18:45 2006
From: eijiro.sumii at gmail.com (Eijiro Sumii)
Date: Sun, 1 Oct 2006 10:18:45 +0900
Subject: [TYPES] Java generics unsoundness?
Message-ID: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>

Dear all,

Hiromasa Kido, an undergraduate student in the University of Tokyo,
has found the problem below in the implementation of generics in Java.
 Another student, Kouta Mizushima, in Tsukuba University, reported
that it also reproduces in Eclipse (which has its own compiler).

----------------------------------------------------------------------
C:\WINDOWS\Temp>c:\progra~1\java\jdk1.6.0\bin\java -version
java version "1.6.0-rc"
Java(TM) SE Runtime Environment (build 1.6.0-rc-b100)
Java HotSpot(TM) Client VM (build 1.6.0-rc-b100, mixed mode, sharing)

C:\WINDOWS\Temp>type B.java
class A{
       public int compareTo(Object o){
               return 0;
       }
}

class B extends A implements Comparable<B>{
       public int compareTo(B b){
               return 0;
       }

       public static void main(String[] argv){
               System.out.println(new B().compareTo(new Object()));
       }
}

C:\WINDOWS\Temp>c:\progra~1\java\jdk1.6.0\bin\javac -Xlint B.java

C:\WINDOWS\Temp>c:\progra~1\java\jdk1.6.0\bin\java B
Exception in thread "main" java.lang.ClassCastException: java.lang.Object cannot
 be cast to B
        at B.compareTo(B.java:7)
        at B.main(B.java:13)

C:\WINDOWS\Temp>
----------------------------------------------------------------------

Here is my understanding (confirmed by Atsushi Igarashi) of the
problem: after erasure (i.e., replacing every type variable with the
Object class), an auxiliary method (called bridged method) like

  public int compareTo(Object x){
    return compareTo((B)x);
  }

is created by the compiler in class B.  However, this additional
method happens to override A.compareTo and raises an unexpected
ClassCastException.

We have already submitted a bug report to Sun.  My question is: Is
this a bug in the compiler, or in the design of the language?  On one
hand, it is a compiler bug because the bridge method, inserted by the
compiler, is doing the harm.  On the other hand, it would be hard for
any compilers to implement generic interfaces without bridge methods
(unless we modify the present JVM).  In my understading, such
overriding as above is not forbidden in the current language
specification (page 227 and page 478 perhaps).

Does any expert in this list have a word on this matter...?

Thanks in advance,

Eijiro Sumii
http://www.kb.ecei.tohoku.ac.jp/~sumii/

From eijiro.sumii at gmail.com  Sun Oct  1 02:12:57 2006
From: eijiro.sumii at gmail.com (Eijiro Sumii)
Date: Sun, 1 Oct 2006 15:12:57 +0900
Subject: [TYPES] Java generics unsoundness?
In-Reply-To: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
References: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
Message-ID: <a4d0794e0609302312m271f5356s51779670611cbd3@mail.gmail.com>

P.S.

On 10/1/06, Eijiro Sumii <eijiro.sumii at gmail.com> wrote:
> (unless we modify the present JVM).  In my understading, such
> overriding as above is not forbidden in the current language
  ^^^^^^^^^^
I meant "overloading."  Sorry.

> specification (page 227 and page 478 perhaps).

From eernst at daimi.au.dk  Sun Oct  1 17:08:09 2006
From: eernst at daimi.au.dk (Erik Ernst)
Date: Sun, 1 Oct 2006 23:08:09 +0200
Subject: [TYPES] Java generics unsoundness?
In-Reply-To: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
References: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
Message-ID: <200610012308.09407.eernst@daimi.au.dk>

Dear Eijiro Sumii and all others,

not pretending to be the world authority on this issue, the following 
does seem to apply:

  - JLS mentions type erasure (4.6) so this would be part of the 
language, but it is not an inherent property of type erasure that 
these method name clashes arise.

  - JLS does not mention bridge methods as far as I know, so 
presumably it should be possible to implement them in a different way 
without violating the language def.  To avoid the method clash we 
could use name mangling, i.e., including the types of the type-erased 
arguments in the name of the method (as well as $ or similar, to 
avoid clashes with user-defined names).  Call sites would be compiled 
in a context where the argument types are known, so they could easily 
use the correct (mangled) name.

All in all, this seems to be a bug in the implementation.

Of course it is not that easy in practice, e.g., because 
existing .class files would then break en masse...

On Sunday 01 October 2006 03:18, Eijiro Sumii wrote:
> [..]
> 
> Dear all,
> 
> Hiromasa Kido, an undergraduate student in the University of Tokyo,
> has found the problem below in the implementation of generics in 
> Java. [..]
>----------------------------------------------------------------------
> [..]
> C:\WINDOWS\Temp>type B.java
> class A{
>        public int compareTo(Object o){
>                return 0;
>        }
> }
> 
> class B extends A implements Comparable<B>{
>        public int compareTo(B b){
>                return 0;
>        }
> 
>        public static void main(String[] argv){
>                System.out.println(new B().compareTo(new Object()));
>        }
> }
> [..]
>----------------------------------------------------------------------
> 
> Here is my understanding (confirmed by Atsushi Igarashi) of the
> problem: after erasure (i.e., replacing every type variable with the
> Object class), an auxiliary method (called bridged method) like
> 
>   public int compareTo(Object x){
>     return compareTo((B)x);
>   }
> 
> is created by the compiler in class B.  However, this additional
> method happens to override A.compareTo and raises an unexpected
> ClassCastException.
> 
> We have already submitted a bug report to Sun.  My question is: Is
> this a bug in the compiler, or in the design of the language?  On 
> one 
> hand, it is a compiler bug because the bridge method, inserted by 
> the 
> compiler, is doing the harm.  On the other hand, it would be hard 
> for 
> any compilers to implement generic interfaces without bridge methods
> (unless we modify the present JVM).  In my understading, such
> overriding as above is not forbidden in the current language
> specification (page 227 and page 478 perhaps).
> 
> Does any expert in this list have a word on this matter...?
> 
> Thanks in advance,
> 
> Eijiro Sumii
> http://www.kb.ecei.tohoku.ac.jp/~sumii/
> 

  best regards,

-- 
Erik Ernst                        eernst at daimi.au.dk
Department of Computer Science, University of Aarhus
IT-parken,  Aabogade 34,  DK-8200 Aarhus N,  Denmark

From mach.elf at gmail.com  Mon Oct  2 15:39:58 2006
From: mach.elf at gmail.com (Pete Kirkham)
Date: Mon, 2 Oct 2006 20:39:58 +0100
Subject: [TYPES] Java generics unsoundness?
In-Reply-To: <200610012308.09407.eernst@daimi.au.dk>
References: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
	<200610012308.09407.eernst@daimi.au.dk>
Message-ID: <f9d9d39b0610021239j73e58ab5o8c57ac84773c5e00@mail.gmail.com>

The section on override-equivalent signatures,
<http://java.sun.com/docs/books/jls/third_edition/html/classes.html#8.4.2>,
indicates the effect is intentional - the erasure of B#compareTo(B)
overrides A#compareTo(Object) as well as Comparable<T>#compareTo(T)
since B#compareTo(B)  is override equivalent to A#compareTo(Object) by
erasure.

Since B's method does override A's method, but takes a takes a B, the
object undergoes assignment conversion
<http://java.sun.com/docs/books/jls/third_edition/html/conversions.html#5.2
>, and being incompatible, a ClassCastException is thrown. This is
achieved via the bridging method.

So I don't believe it's a bug in the compilers, but rather one of
several design features of a Java generics that are intended to help
backwards compatibility. In this case the non-generic version of B
would have been:

class B extends A implements Comparable {
      public int compareTo(Object o){
              B b = (B)o;
              // it's part of the contract of Comparable to throw CCE
if presented
              // with the wrong type
              return 0;
      }
}

Though actually it was common practice prior to 1.5 to add a bridge
method manually so the type-specific method was called when the type
of the argument was know.


Pete

From eernst at daimi.au.dk  Mon Oct  2 18:13:07 2006
From: eernst at daimi.au.dk (Erik Ernst)
Date: Tue, 3 Oct 2006 00:13:07 +0200
Subject: [TYPES] Java generics unsoundness?
In-Reply-To: <f9d9d39b0610021239j73e58ab5o8c57ac84773c5e00@mail.gmail.com>
References: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
	<200610012308.09407.eernst@daimi.au.dk>
	<f9d9d39b0610021239j73e58ab5o8c57ac84773c5e00@mail.gmail.com>
Message-ID: <200610030013.08074.eernst@daimi.au.dk>

On Monday 02 October 2006 21:39, Pete Kirkham wrote:
> [..]
> The section on override-equivalent signatures,
><http://java.sun.com/docs/books/jls/third_edition/html/classes.html#8.4.2>,
> indicates the effect is intentional - the erasure of B#compareTo(B)
> overrides A#compareTo(Object) as well as Comparable<T>#compareTo(T)
> since B#compareTo(B)  is override equivalent to A#compareTo(Object) 
> by 
> erasure.

True, it is intentional that a generified version of a method should 
be able to be overriden by an erased version, such that people can 
continue to use old code with new, generified libraries.  So dispatch 
does at times select the most specific method implementation from a 
set of methods with different (though override-equivalent) 
signatures:  In 8.4.2 the set is '<T> toList(Collection<T>)' in 
CollectionConverter and 'toList(Collection)' in Overrider, and the 
latter overrides the former.

But 'compareTo(Object)' in A and 'compareTo(B)' in B are not 
override-equivalent (B is a class, not a type variable), so 
override-equivalence does not allow these methods to override each 
other, only overloading may occur.

So far it looks like a bug in the implementation that they end up 
overriding each other, caused by the use of bridge methods.

Now the interesting point is that the crucial bridge method is 
introduced because some clients might access an instance of B under 
the type Comparable<B>.  This interface declares a method with 
signature 'compareTo(B)' where B is a type variable---so it erases to 
'compareTo(Object)' which is of course override-equivalent with 
'compareTo(Object)' in A.

Hence, the two methods 'compareTo(Object)' in A and 'compareTo(B)' in 
B are brought together in overriding _via_ the interface 
Comparable<B> and its method 'compareTo(B)'.  The problem arises 
because B is considered as a class in one context (in the class B) 
and as a type variable in the other context (when accessing an 
instance of B under the type Comparable<B>).  The bridge method is 
generated under the assumption that it will _only_ receive 
invocations based on the type Comparable<B> (and the argument will 
then be of type B), but it may in fact also receive invocations based 
on the type A (with arguments of type Object), which causes the 
ClassCastException.

In other words, the assumptions used when generating bridge methods 
(with the same name) do not always hold.  To me it still seems like 
the problem would disappear if the bridge method were generated with 
a signature along the lines of 'compareTo$B(Object)' and invocations 
based on the type Comparable<B> would call that method.

> Since B's method does override A's method, but takes a takes a B, 
> the 
> object undergoes assignment conversion
><http://java.sun.com/docs/books/jls/third_edition/html/conversions.html#5.2>,
> and being incompatible, a ClassCastException is thrown. This is
> achieved via the bridging method.

I have made an attempt to argue above that B's method does not 
override A's method.

> So I don't believe it's a bug in the compilers, but rather one of
> several design features of a Java generics that are intended to help
> backwards compatibility. 

I agree that the whole idea about override-equivalence was introduced 
in order to improve flexibility in a gradual 'generification' of 
large bodies of software, but I think that the problem is the 
assumptions behind bridge method generation, rather than the notion 
of override-equivalence.

  best regards,

-- 
Erik Ernst                        eernst at daimi.au.dk
Department of Computer Science, University of Aarhus
IT-parken,  Aabogade 34,  DK-8200 Aarhus N,  Denmark

From eijiro.sumii at gmail.com  Tue Oct  3 08:03:42 2006
From: eijiro.sumii at gmail.com (Eijiro Sumii)
Date: Tue, 3 Oct 2006 21:03:42 +0900
Subject: [TYPES] Java generics unsoundness?
In-Reply-To: <45223AB9.4060609@epfl.ch>
References: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
	<45223AB9.4060609@epfl.ch>
Message-ID: <a4d0794e0610030503i33994fc3v7cbcb2a5ecf801ea@mail.gmail.com>

Dear all,

Thank you for all the replies!  Let me try to address one source of
confusion: as far as I understand according to

  http://java.sun.com/docs/books/jls/third_edition/html/typesValues.html#4.6

the erasure of "int compareTo(B)" is itself, not "int
compareTo(Object)", because B is a class, not a type variable - is
this correct?  (Sorry if my terminology is not accurate - I have never
read the Java Language Specification before this.)

Thanks again,

        Eijiro

From ven at jetbrains.com  Tue Oct  3 11:01:45 2006
From: ven at jetbrains.com (Eugene Vigdorchik)
Date: Tue, 3 Oct 2006 19:01:45 +0400
Subject: [TYPES] Java generics unsoundness?
In-Reply-To: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
Message-ID: <003401c6e6fc$d7b3f500$1d01a8c0@Labs.IntelliJ.Net>

 Hello, Ejiro,

As far as I can tell (I'm working on IntelliJ IDEA, and we have our own type system implementation) the compiler is wrong here.
Though bridge methods are not mentioned explicitly in JLS, certain restrictions are imposed by language specification due to their
existance. The code you provide should be rejected because of JLS section 8.4.8.3 stating it is an error to have two inherited
methods (A.compareTo and Comparable.compareTo)  with same erasure that do not override each other.

Hope this helps,
Eugene.

> -----Original Message-----
> From: types-list-bounces at lists.seas.upenn.edu 
> [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of 
> Eijiro Sumii
> Sent: Sunday, October 01, 2006 5:19 AM
> To: types at cis.upenn.edu
> Cc: Eijiro Sumii
> Subject: [TYPES] Java generics unsoundness?
> 
> [ The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Dear all,
> 
> Hiromasa Kido, an undergraduate student in the University of 
> Tokyo, has found the problem below in the implementation of 
> generics in Java.
>  Another student, Kouta Mizushima, in Tsukuba University, 
> reported that it also reproduces in Eclipse (which has its 
> own compiler).
> 
> ----------------------------------------------------------------------
> C:\WINDOWS\Temp>c:\progra~1\java\jdk1.6.0\bin\java -version 
> java version "1.6.0-rc"
> Java(TM) SE Runtime Environment (build 1.6.0-rc-b100) Java 
> HotSpot(TM) Client VM (build 1.6.0-rc-b100, mixed mode, sharing)
> 
> C:\WINDOWS\Temp>type B.java
> class A{
>        public int compareTo(Object o){
>                return 0;
>        }
> }
> 
> class B extends A implements Comparable<B>{
>        public int compareTo(B b){
>                return 0;
>        }
> 
>        public static void main(String[] argv){
>                System.out.println(new B().compareTo(new Object()));
>        }
> }
> 
> C:\WINDOWS\Temp>c:\progra~1\java\jdk1.6.0\bin\javac -Xlint B.java
> 
> C:\WINDOWS\Temp>c:\progra~1\java\jdk1.6.0\bin\java B 
> Exception in thread "main" java.lang.ClassCastException: 
> java.lang.Object cannot  be cast to B
>         at B.compareTo(B.java:7)
>         at B.main(B.java:13)
> 
> C:\WINDOWS\Temp>
> ----------------------------------------------------------------------
> 
> Here is my understanding (confirmed by Atsushi Igarashi) of the
> problem: after erasure (i.e., replacing every type variable 
> with the Object class), an auxiliary method (called bridged 
> method) like
> 
>   public int compareTo(Object x){
>     return compareTo((B)x);
>   }
> 
> is created by the compiler in class B.  However, this 
> additional method happens to override A.compareTo and raises 
> an unexpected ClassCastException.
> 
> We have already submitted a bug report to Sun.  My question 
> is: Is this a bug in the compiler, or in the design of the 
> language?  On one hand, it is a compiler bug because the 
> bridge method, inserted by the compiler, is doing the harm.  
> On the other hand, it would be hard for any compilers to 
> implement generic interfaces without bridge methods (unless 
> we modify the present JVM).  In my understading, such 
> overriding as above is not forbidden in the current language 
> specification (page 227 and page 478 perhaps).
> 
> Does any expert in this list have a word on this matter...?
> 
> Thanks in advance,
> 
> Eijiro Sumii
> http://www.kb.ecei.tohoku.ac.jp/~sumii/
> 
> 
> 


From igarashi at kuis.kyoto-u.ac.jp  Tue Oct  3 11:11:01 2006
From: igarashi at kuis.kyoto-u.ac.jp (Atsushi Igarashi)
Date: Wed, 04 Oct 2006 00:11:01 +0900
Subject: [TYPES] Java generics unsoundness?
In-Reply-To: <200610012308.09407.eernst@daimi.au.dk>
References: <a4d0794e0609301818j1a236233kbc1f6ce5ceb54265@mail.gmail.com>
	<200610012308.09407.eernst@daimi.au.dk>
Message-ID: <874pulqvsq.wl@triangle.sato.kuis.kyoto-u.ac.jp>

Dear all,

I'm not 100% sure but, as far as I understand, compilers should reject
this program according to JLS.

Here is my understanding:

On p.227, there is a description saying:

  It is a compile time error if a type declaration T has a member
  method m1 and there exists a method m2 declared in T or a supertype
  of T such that all of the following conditions hold:

  - m1 and m2 have the same name.
  - m2 is accessible from T.
  - The signature of m1 is not a subsignature (?8.4.2) of the
    signature of m2.
  - m1 or some method m1 overrides (directly or indirectly) has the
    same erasure as m2 or some method m2 overrides (directly or
    indirectly).

In this case, T is B,
 m1 is public int compareTo(B b) {...} (declared in B), and
 m2 is public int compareTo(Object o) {...} (declared in A).

Then,

1. a type declaration T (=B) has a member method m1.

2. it holds that there exists a method m2 declared in T or a supertype
of T, as A is a supertype of B.

Conditions after "such that" also hold:

- Do m1 and m2 have the same name?  Yes.
- Is m2 accessible from T? Yes.
- Is the signature of m1 not a subsignature (?8.4.2) of the signature
of m2?  No, because the signatures of m1 and m2 are different and
also the signature of m1 and the _erased_ signature of m2 are
different.

- Does m1 or some method m1 overrides (directly or indirectly) have the same erasure
as m2 or some method m2 overrides (directly or indirectly)?

  Yes, m1 overrides Comparable's compareTo(), whose erased signature is
  int(Object) and m2's erasure is also int(Object).

Now, all the premises hold, so this should be a compile-time error.

It seems to me that the last condition is checking conflicts among
user-defined methods and bridge methods.

One question remains, though.  Is it correct to say that a concrete
method in a class "overrides" (rather than implements) an abstract
method in an interface?  My interpretation above use "overrides"
for such a relation.

I've found that the definition of "a method in a class overrides
another in a super _class_" (p.224) and "a method in an _interface_
overrides another in a super _interface_" (p.267) but not "a method in
a class overrides another in an interface that the class implements".

Cheers,
--
Atsushi Igarashi
Graduate School of Informatics
Kyoto University
Yoshida-Honmachi, Sakyo-ku
Kyoto 606-8501,Japan
e-mail: igarashi at kuis.kyoto-u.ac.jp
TEL: +81-75-753-4953
FAX: +81-75-753-4954



At Sun, 1 Oct 2006 23:08:09 +0200,
Erik Ernst wrote:
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Dear Eijiro Sumii and all others,
> 
> not pretending to be the world authority on this issue, the following 
> does seem to apply:
> 
>   - JLS mentions type erasure (4.6) so this would be part of the 
> language, but it is not an inherent property of type erasure that 
> these method name clashes arise.
> 
>   - JLS does not mention bridge methods as far as I know, so 
> presumably it should be possible to implement them in a different way 
> without violating the language def.  To avoid the method clash we 
> could use name mangling, i.e., including the types of the type-erased 
> arguments in the name of the method (as well as $ or similar, to 
> avoid clashes with user-defined names).  Call sites would be compiled 
> in a context where the argument types are known, so they could easily 
> use the correct (mangled) name.
> 
> All in all, this seems to be a bug in the implementation.
> 
> Of course it is not that easy in practice, e.g., because 
> existing .class files would then break en masse...
> 
> On Sunday 01 October 2006 03:18, Eijiro Sumii wrote:
> > [..]
> > 
> > Dear all,
> > 
> > Hiromasa Kido, an undergraduate student in the University of Tokyo,
> > has found the problem below in the implementation of generics in 
> > Java. [..]
> >----------------------------------------------------------------------
> > [..]
> > C:\WINDOWS\Temp>type B.java
> > class A{
> >        public int compareTo(Object o){
> >                return 0;
> >        }
> > }
> > 
> > class B extends A implements Comparable<B>{
> >        public int compareTo(B b){
> >                return 0;
> >        }
> > 
> >        public static void main(String[] argv){
> >                System.out.println(new B().compareTo(new Object()));
> >        }
> > }
> > [..]
> >----------------------------------------------------------------------
> > 
> > Here is my understanding (confirmed by Atsushi Igarashi) of the
> > problem: after erasure (i.e., replacing every type variable with the
> > Object class), an auxiliary method (called bridged method) like
> > 
> >   public int compareTo(Object x){
> >     return compareTo((B)x);
> >   }
> > 
> > is created by the compiler in class B.  However, this additional
> > method happens to override A.compareTo and raises an unexpected
> > ClassCastException.
> > 
> > We have already submitted a bug report to Sun.  My question is: Is
> > this a bug in the compiler, or in the design of the language?  On 
> > one 
> > hand, it is a compiler bug because the bridge method, inserted by 
> > the 
> > compiler, is doing the harm.  On the other hand, it would be hard 
> > for 
> > any compilers to implement generic interfaces without bridge methods
> > (unless we modify the present JVM).  In my understading, such
> > overriding as above is not forbidden in the current language
> > specification (page 227 and page 478 perhaps).
> > 
> > Does any expert in this list have a word on this matter...?
> > 
> > Thanks in advance,
> > 
> > Eijiro Sumii
> > http://www.kb.ecei.tohoku.ac.jp/~sumii/
> > 
> 
>   best regards,
> 
> -- 
> Erik Ernst                        eernst at daimi.au.dk
> Department of Computer Science, University of Aarhus
> IT-parken,  Aabogade 34,  DK-8200 Aarhus N,  Denmark

From gmh at Cs.Nott.AC.UK  Mon Oct  9 05:40:59 2006
From: gmh at Cs.Nott.AC.UK (Graham Hutton)
Date: Mon, 09 Oct 2006 10:40:59 +0100
Subject: [TYPES] ICFP 2007 Call for Workshop Proposals
Message-ID: <1598.1160386859@cs.nott.ac.uk>

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

		     CALL FOR WORKSHOP PROPOSALS

	    ICFP 2007, the 12th ACM SIGPLAN International
		 Conference on Functional Programming

		 1-3 October 2007, Freiburg, Germany


The   12th  ACM   SIGPLAN  International   Conference   on  Functional
Programming (ICFP 2007) will be  held in Freiburg, Germany from 1st to
3rd  October  2007.   ICFP   provides  a  forum  for  researchers  and
developers   to  hear   about   the  latest   work   on  the   design,
implementations, principles, and uses of functional programming.

Proposals are  invited for workshops  to be affiliated with  ICFP 2007
and sponsored by SIGPLAN.  These workshops should be more informal and
focused  than ICFP  itself, include  sessions that  enable interaction
among the workshop attendees, and  be fairly low cost.  The preference
is for one-day workshops, but  other schedules can also be considered.
The workshops themselves will be  held on 30th September, 4th October,
and 5th October 2007.

SUBMISSION DETAILS

   Deadline for submission:     17th November 2006 
   Notification of acceptance:  15th December 2006  

Prospective  workshop organisers  are  invited to  submit a  completed
workshop proposal form in plain  text format to the ICFP 2007 workshop
co-chairs   (Graham  Hutton   and  Matthias   Blume),  via   email  to
icfp07-workshops at cs.nott.ac.uk by  17th November 2006.  Please note
that this  is a firm deadline.   Organisers will be  notified if their
proposal  is accepted  by 15th  December 2006,  and if  successful are
required to produce a final  report after the workshop has taken place
that is suitable for publication in SIGPLAN Notices.

SELECTION COMMITTEE

The workshop proposals will be evaluated by a committee comprising the
following members of the ICFP 2007 organising committee, together with
the members of the SIGPLAN executive committee.

   Graham Hutton    University of Nottingham   Workshops co-chair  
   Matthias Blume   TTI at Chicago             Workshops co-chair  
   Ralf Hinze       Universitat Bonn           General chair  
   Norman Ramsey    Harvard University         Program chair  

FURTHER INFORMATION

Any queries regarding ICFP 2007 workshop proposals should be addressed
to  the workshops co-chairs  (Graham Hutton  and Matthias  Blume), via
email to icfp07-workshops at cs.nott.ac.uk.

USEFUL LINKS

   Call for workshop proposals
      http://www.cs.nott.ac.uk/~gmh/icfp07-workshops.html

   Workshop proposal form
      http://www.cs.nott.ac.uk/~gmh/icfp07-workshops-form.txt

   ICFP 2007 home page
      http://www.informatik.uni-bonn.de/~ralf/icfp07.html

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

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.


From Burak.Emir at epfl.ch  Wed Oct 25 12:25:09 2006
From: Burak.Emir at epfl.ch (Burak Emir)
Date: Wed, 25 Oct 2006 18:25:09 +0200
Subject: [TYPES] trace back pattern matching, typecase
Message-ID: <453F8FE5.1020908@epfl.ch>

Dear TYPES readers,

I am looking for historic references on typecase, pattern matching.

1) For pattern matching, I have come to think the earliest publication is:
Burstall (1969) Proving properties of programs by structural induction. 
Computer Journal,  12 (1) pp. 41-48

Although ML was developed later, one can often read ML-style pattern 
matching in the literature.

2) For typecase, it is much less clear to me what one could reference as 
first emergence. Modula-3 comes to my mind. It is probably helpful to 
narrow my query to statically typed languages at this point.

Finally I am tempted to think that elimination of sum types also 
qualifies as a simple form of typecase/basic pattern matching. But I 
cannot imagine a precise point where this particular "feature" made it 
into programming practice (other than the forms described above). I'd be 
glad to hear about such a thing.

Thanks for shedding some light on these issues.

Burak Emir

-- 
Burak Emir

http://lamp.epfl.ch/~emir


From carette at mcmaster.ca  Wed Oct 25 14:04:19 2006
From: carette at mcmaster.ca (Jacques Carette)
Date: Wed, 25 Oct 2006 14:04:19 -0400
Subject: [TYPES] trace back pattern matching, typecase
In-Reply-To: <453F8FE5.1020908@epfl.ch>
References: <453F8FE5.1020908@epfl.ch>
Message-ID: <453FA723.2020001@mcmaster.ca>

Burak Emir wrote:
> 2) For typecase, it is much less clear to me what one could reference as 
> first emergence. Modula-3 comes to my mind. It is probably helpful to 
> narrow my query to statically typed languages at this point.
>   
As far as programming language idioms go, this was already used in 
FORMAC (1962).
http://hopl.murdoch.edu.au/showlanguage.prx?exp=158&language=FORMAC

Certainly it was in heavy use in Macsyma (1967/68 - today).  Which 
probably implies that it was an idiom known to LISP programmers before that.

But perhaps you meant 'typecase' in a (mostly) statically typed 
language?  Then Scratchpad (now Axiom) probably had that from early on 
in its life (definitely by the early 80s, more likely before that).

Jacques


From Malcolm.Tyrrell at computing.dcu.ie  Thu Oct 26 09:21:09 2006
From: Malcolm.Tyrrell at computing.dcu.ie (Malcolm Tyrrell)
Date: Thu, 26 Oct 2006 14:21:09 +0100
Subject: [TYPES] CPO semantics of recursive types
Message-ID: <4540B645.9060205@computing.dcu.ie>


Hello,

I have a question concerning the denotational semantics of
recursive types using complete partial orders.

For a programming language, the domain for a function type T->U is
defined as the space of all continuous functions from the domain of T
to the domain of U. I understand that recursively defined domains
have solutions in this semantics.

I am working with a specification language, and the domains I'm using
for function types T->U is the space of all *monotonic* functions from
the domain of T to the domain of U. Can anyone tell me (or even better,
point me to a reference) whether this has any ramifications for the
existence of recursively defined domains?

Thanks for any help,

Malcolm.

From A.Jung at cs.bham.ac.uk  Thu Oct 26 10:05:51 2006
From: A.Jung at cs.bham.ac.uk (Achim Jung)
Date: Thu, 26 Oct 2006 15:05:51 +0100 (BST)
Subject: [TYPES] CPO semantics of recursive types
In-Reply-To: <4540B645.9060205@computing.dcu.ie>
References: <4540B645.9060205@computing.dcu.ie>
Message-ID: <Pine.LNX.4.64.0610261500350.14860@gromit.cs.bham.ac.uk>

Malcolm, for cpos and continuous functions we have solutions to all 
recursive domain equations, for example, D =  [D -> D].

If [D -> D] is interpreted as the (pointwise ordered) cpo of monotone 
functions then D = [D -> D] has only the one-point cpo as a solution. This 
was first shown in the paper

@Article{davies71,
   author = 	{R. O. Davies and A. Hayes and G. Rousseau},
   title = 	{Complete Lattices and the Generalized {Cantor}
 		  Theorem},
   journal = 	{Proceedings of the AMS},
   year = 	1971,
   volume = 	27,
   pages = 	{253--258}
}

Best regards,

Achim.

-------------------------------------------------------------------------
  Prof Achim Jung			Tel.: (+44) 121 41 44776
  School of Computer Science		Sec.: (+44) 121 41 43711
  The University of Birmingham		Fax.: (+44) 121 41 44281
  Edgbaston				Email: A.Jung at cs.bham.ac.uk
  BIRMINGHAM, B15 2TT			Web: http://www.cs.bham.ac.uk
  England
-------------------------------------------------------------------------



On Thu, 26 Oct 2006, Malcolm Tyrrell wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
> Hello,
>
> I have a question concerning the denotational semantics of
> recursive types using complete partial orders.
>
> For a programming language, the domain for a function type T->U is
> defined as the space of all continuous functions from the domain of T
> to the domain of U. I understand that recursively defined domains
> have solutions in this semantics.
>
> I am working with a specification language, and the domains I'm using
> for function types T->U is the space of all *monotonic* functions from
> the domain of T to the domain of U. Can anyone tell me (or even better,
> point me to a reference) whether this has any ramifications for the
> existence of recursively defined domains?
>
> Thanks for any help,
>
> Malcolm.
>

From Xavier.Leroy at inria.fr  Thu Oct 26 12:48:11 2006
From: Xavier.Leroy at inria.fr (Xavier Leroy)
Date: Thu, 26 Oct 2006 18:48:11 +0200
Subject: [TYPES] trace back pattern matching, typecase
In-Reply-To: <453F8FE5.1020908@epfl.ch>
References: <453F8FE5.1020908@epfl.ch>
Message-ID: <4540E6CB.20208@inria.fr>

Burak Emir wrote:

> I am looking for historic references on typecase, pattern matching.

I suspect a great deal of early work on pattern matching was done in
the Lisp community.  Steele and Gabriel's paper "The Evolution of
Lisp" gives some pointers.

> 2) For typecase, it is much less clear to me what one could reference as
> first emergence. Modula-3 comes to my mind. It is probably helpful to
> narrow my query to statically typed languages at this point.

The paper "Dynamic Typing in a Statically Typed Language" by Abadi,
Cardelli, Pierce and Plotkin lists SIMULA-67 and CLU as early examples
of typecase.  There is also Cardelli's Amber language, which predates
(and probably inspired) Modula-3's typecase.

Hope this helps,

- Xavier Leroy

From Malcolm.Tyrrell at computing.dcu.ie  Fri Oct 27 08:42:27 2006
From: Malcolm.Tyrrell at computing.dcu.ie (Malcolm Tyrrell)
Date: Fri, 27 Oct 2006 13:42:27 +0100
Subject: [TYPES] CPO semantics of recursive types
In-Reply-To: <4540B645.9060205@computing.dcu.ie>
References: <4540B645.9060205@computing.dcu.ie>
Message-ID: <4541FEB3.3080609@computing.dcu.ie>


Thanks to all those who replied (on and off list). As I feared,
recursive domain equations do not, in general, have solutions in the
monotonic case.  I'm working with a typed functional language in
which the domain D = D->D is unlikely to arise. However, losing
recursive types altogether would be very annoying.

One very interesting suggestion (thanks!) was to use a smaller space
for [T->U], such as the space of kappa-continuous functions. I will
investigate this in due course.

Can anyone suggest how other specification languages, which support
recursive types, overcome this problem?

For the moment, I will adopt a defensive position and disallow
recursive types where the recursion parameter occurs in either
argument of a function type constructor. I expect that this
restriction is stronger than necessary (at least, I hope it is). I
also expect (hope!) that the significant majority of types used in
practice will satisfy the condition.  Certainly, standard types such
as lists, trees, etc. would be OK.

Unfortunately, I can think of an important example which the
restriction excludes, namely objects. For example, the following ML
datatype would be disallowed:

(**
  * A type for Point objects.
  *)
datatype Point = Point of {
   getX : int,           (* the x coordinate *)
   getY : int,           (* the y coordinate *)
   setX : int -> Point,  (* set the x coordinate *)
   setY : int -> Point,  (* set the y coordinate *)
   eq   : Point -> bool, (* does this point equal another point? *)
   add  : Point -> Point (* add another point to this point *)
}

(I just hacked up this simple object encoding for this posting, so
it may not be the best representative of the problem.)

Malcolm.

From stone at cs.hmc.edu  Tue Oct 31 02:20:13 2006
From: stone at cs.hmc.edu (Christopher A. Stone)
Date: Mon, 30 Oct 2006 23:20:13 -0800
Subject: [TYPES] Looking for Girard's Dissertation
Message-ID: <F61248E6-F7CF-4983-A12D-29259BFA0BC9@cs.hmc.edu>

Greetings!

I've seen many, many papers referencing Girard's 1972 Ph.D.  
dissertation, but I've never seen the dissertation itself.

Can anyone suggest where I could find a copy?

Thanks,
    Chris Stone

------------------------------------------------------------------------
Christopher A. Stone / Associate Professor              stone at cs.hmc.edu
Computer Science Department, Harvey Mudd College   www.cs.hmc.edu/~stone
301 Platt Boulevard, Claremont, CA 91711                  (909) 607-8975


From Y.Luo at kent.ac.uk  Wed Nov 22 07:28:42 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Wed, 22 Nov 2006 12:28:42 -0000
Subject: [TYPES] An efficient program for the function (mod 3) in type
	theories
Message-ID: <02d001c70e31$bf46e7f0$a0290c81@ad.kent.ac.uk>

Dear all,

I am looking for an efficient program of the following function in the
Martin-Lof's type theory or UTT.

Nat is the type of natural numbers with constructors zero and succ.

f :: Nat -> Nat

f (zero) = zero
f (succ(zero)) = succ(zero)
f (succ(succ(zero))) =  succ(succ(zero))
f (succ(succ(succ(x)))) = f (x)

If a type theory has pattern matching such as
http://www.cs.kent.ac.uk/people/staff/yl41/TPF.htm

then this function can be easily programmed with a very good efficiency, for
example f (100) only takes 34 reduction steps.

In the Martin-Lof's type theory or UTT, every function is defined by
eliminators of inductive data types. I would like to know whether it is
possible to have an efficient program for the function f.

Thank you,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent


From ctm at cs.nott.ac.uk  Thu Nov 23 03:42:35 2006
From: ctm at cs.nott.ac.uk (Conor McBride)
Date: Thu, 23 Nov 2006 08:42:35 +0000
Subject: [TYPES] An efficient program for the function (mod 3) in type
 theories
In-Reply-To: <02d001c70e31$bf46e7f0$a0290c81@ad.kent.ac.uk>
References: <02d001c70e31$bf46e7f0$a0290c81@ad.kent.ac.uk>
Message-ID: <45655EFB.2070401@cs.nott.ac.uk>

Hi Yong

Yong Luo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I am looking for an efficient program of the following function in the
> Martin-Lof's type theory or UTT.
>   

As well you know, I wrote a program which will spit out the program you 
want, given (more or less) the program you've written.

> f :: Nat -> Nat
>
> f (zero) = zero
> f (succ(zero)) = succ(zero)
> f (succ(succ(zero))) =  succ(succ(zero))
> f (succ(succ(succ(x)))) = f (x)
>   

> In the Martin-Lof's type theory or UTT, every function is defined by
> eliminators of inductive data types. I would like to know whether it is
> possible to have an efficient program for the function f.
>   

Yes it is. The pattern matching equations hold computationally for the 
UTT programs which the translation spits out. Given a suitable reduction 
strategy (ie, one designed to exploit this property of the translation), 
you get a constant factor blowup in the number of steps, ie a larger 
number of smaller steps.

Hope this helps

Conor


From ctm at Cs.Nott.AC.UK  Mon Nov 27 08:48:34 2006
From: ctm at Cs.Nott.AC.UK (Conor McBride)
Date: Mon, 27 Nov 2006 13:48:34 +0000
Subject: [TYPES] An efficient program for the function (mod 3) in type
 theories
In-Reply-To: <05d301c71223$4bf23bb0$a0290c81@ad.kent.ac.uk>
References: <02d001c70e31$bf46e7f0$a0290c81@ad.kent.ac.uk>
	<45655EFB.2070401@cs.nott.ac.uk>
	<05d301c71223$4bf23bb0$a0290c81@ad.kent.ac.uk>
Message-ID: <456AECB2.1070307@cs.nott.ac.uk>

Yong Luo wrote:
> I wrote:
>
>   
>> Yes it is. The pattern matching equations hold computationally for the
>> UTT programs which the translation spits out. Given a suitable reduction
>> strategy (ie, one designed to exploit this property of the translation),
>> you get a constant factor blowup in the number of steps, ie a larger
>> number of smaller steps.
>>
>> Hope this helps
>>     
>
> There is no doult that the function "mod 3" can be defined in the UTT, for
> example, by using pairs or similar things. My question is: what is the most
> efficient program in the UTT for this function?  I would also like to know
> how many reduction steps for f(100), roughly?
>   

Are you saying that the constant factor is important? Maybe it is, and 
maybe not. One might also question whether comparing numbers of 
reduction steps makes any sense when UTT reductions are very simple and 
pattern matching requires a more complex combination of constructor 
comparison and tuple unpacking operations. As it happens, the UTT code 
is quite similar to the Augustsson-style efficient compilation of 
pattern matching.

If the constant factor is important to you, I'm sure you can calculate 
it yourself.

All the best

Conor


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.


From Y.Luo at kent.ac.uk  Mon Nov 27 07:55:20 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Mon, 27 Nov 2006 12:55:20 -0000
Subject: [TYPES] An efficient program for the function (mod 3) in type
	theories
References: <02d001c70e31$bf46e7f0$a0290c81@ad.kent.ac.uk>
	<45655EFB.2070401@cs.nott.ac.uk>
Message-ID: <05d301c71223$4bf23bb0$a0290c81@ad.kent.ac.uk>

Hi Conor,

Thank you.

Sent: Thursday, November 23, 2006 8:42 AM
Subject: Re: [TYPES] An efficient program for the function (mod 3) in type
theories


> Hi Yong
>
> Yong Luo wrote:
> > [ The Types Forum,
http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >
> > Dear all,
> >
> > I am looking for an efficient program of the following function in the
> > Martin-Lof's type theory or UTT.
> >
>
> As well you know, I wrote a program which will spit out the program you
> want, given (more or less) the program you've written.
>
> > f :: Nat -> Nat
> >
> > f (zero) = zero
> > f (succ(zero)) = succ(zero)
> > f (succ(succ(zero))) =  succ(succ(zero))
> > f (succ(succ(succ(x)))) = f (x)
> >
>
> > In the Martin-Lof's type theory or UTT, every function is defined by
> > eliminators of inductive data types. I would like to know whether it is
> > possible to have an efficient program for the function f.
> >
>
> Yes it is. The pattern matching equations hold computationally for the
> UTT programs which the translation spits out. Given a suitable reduction
> strategy (ie, one designed to exploit this property of the translation),
> you get a constant factor blowup in the number of steps, ie a larger
> number of smaller steps.
>
> Hope this helps

There is no doult that the function "mod 3" can be defined in the UTT, for
example, by using pairs or similar things. My question is: what is the most
efficient program in the UTT for this function?  I would also like to know
how many reduction steps for f(100), roughly?

Thank you,

Yong


From Y.Luo at kent.ac.uk  Fri Dec  1 07:45:57 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Fri, 1 Dec 2006 12:45:57 -0000
Subject: [TYPES] How fast is the fastest sorting program in type theories?
Message-ID: <0c4c01c71546$a5f661b0$a0290c81@ad.kent.ac.uk>

Dear all,

I would like to know the complexity of Quicksort in type theories.

According to private conversation, the complexity of Quicksort in type
theories is: Cubic. But I am not sure whether it is a correct analysis.

I have implemented a type theory with pattern matching. The complexity of
Quicksort is O(n log n) in the best case (see the following link for
details).
 http://www.cs.kent.ac.uk/people/staff/yl41/TPF.htm

The complexity of Quicksort might be different for different
implementations. I would like to collect all the results and make a
comparison.

Thank you,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent




From Y.Luo at kent.ac.uk  Tue Dec  5 09:05:24 2006
From: Y.Luo at kent.ac.uk (Yong Luo)
Date: Tue, 5 Dec 2006 14:05:24 -0000
Subject: [TYPES] Is Quick Sort slower than Insertion Sort in type theories?
Message-ID: <059c01c71876$68fa9a50$a0290c81@ad.kent.ac.uk>

Dear all,

I posted an email about Quick Sort few days ago. Thank you for your reply.

Insertion Sort is primitive recursion, so it is easy to program it in type
theories and the average complexity is O(n^2).

Quick Sort is not primitive recursion, so there are proofs in the program
when it is programmed in type theories. I am told that the average
complexity "might" be O(n^3), or might be worse. Please let me know if you
know of any work on this.

Regards,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent