From jeremy.siek at gmail.com Wed Jan 16 19:14:12 2008 From: jeremy.siek at gmail.com (Jeremy Siek) Date: Wed, 16 Jan 2008 17:14:12 -0700 Subject: [TYPES] paper on gradual typing with inference Message-ID: Dear Colleagues, We are pleased to share with you a new paper about integrating gradual typing and unification-based type inference (which underlies the Hindley-Milner type system). This was one of those systems where the algorithm was easy to come up with, but the type system was somewhat tricky. http://ece.colorado.edu/~siek/pldi08gradual.pdf Any comments or suggests are most welcome. The paper is under review for PLDI 2008**. Best regards, Jeremy Siek & Manish Vachharajani **The review was double blind, but the reviews have already been submitted and the identities of the authors revealed. ____________________________________ Jeremy Siek http://ece.colorado.edu/~siek/ Assistant Professor Dept. of Electrical and Computer Engineering University of Colorado at Boulder From Tim.Sweeney at epicgames.com Thu Jan 17 17:40:21 2008 From: Tim.Sweeney at epicgames.com (Tim Sweeney) Date: Thu, 17 Jan 2008 17:40:21 -0500 Subject: [TYPES] paper on gradual typing with inference In-Reply-To: References: Message-ID: Hello, This is a welcome work on gradual typing. Now, please pardon me for using this thread to note something relevant to dynamic and gradual typing, which I haven't seen said elsewhere: Any language with a dynamic or gradual type system is necessarily either partial (potentially non-terminating), or aparametric (admitting programs that violate the parametricity property, described in http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html). This is the case because a dynamically typed fragment of a program may coerce a value of unknown type to a specific type required in a context, such as coercing x to a numeric type in x+1. A coercion which fails may provide a means such as exception-handling or returning an appropriately typed indicator value (such as the integer value 0) which the program can observe and act upon. In this case, the language is aparametric, as it allows extracting information from a value of universal type. But parametricity is a valuable security property in languages: a pure function with a parameter of universally quantified type guarantees that it cannot inspect that parameter, but can only place it somewhere in its result value. If failed coercions always cause an unrecoverable program abort, then it's observably equivalent to any other divergent outcome. Hence the language doesn't necessarily violate parametricity, but it is certainly partial. Because gradual typing, total programming, and parametricity are all desirable features in a language, I wanted to note that a type system can soundly support all three in the following way: Start with a total language, and extend it using e.g. Haskell style monads, or effects-typing, to support aparametricity and partiality as effects. At the top level of a program, both would be allowed. Once a function is invoked with requires parametricity or totality, the type system guarantees that it cannot perform operations which are either partial or aparametricity. This approach could be extended further, to the extent of treating every axiom underlying a type system as an independent effect, enabling portions of code to be verified within restrictive fragments of the type system guaranteeing other properties such as linearity, non-commutativity, etc. This provides an interesting means for soundly layering future proofs-of-programs features requiring parametricity and totality on top of existing languages and runtime frameworks which are more lax. Tim Sweeney -----Original Message----- From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Jeremy Siek Sent: Wednesday, January 16, 2008 7:14 PM To: type-list Subject: [TYPES] paper on gradual typing with inference [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear Colleagues, We are pleased to share with you a new paper about integrating gradual typing and unification-based type inference (which underlies the Hindley-Milner type system). This was one of those systems where the algorithm was easy to come up with, but the type system was somewhat tricky. http://ece.colorado.edu/~siek/pldi08gradual.pdf Any comments or suggests are most welcome. The paper is under review for PLDI 2008**. Best regards, Jeremy Siek & Manish Vachharajani **The review was double blind, but the reviews have already been submitted and the identities of the authors revealed. ____________________________________ Jeremy Siek http://ece.colorado.edu/~siek/ Assistant Professor Dept. of Electrical and Computer Engineering University of Colorado at Boulder From wadler at inf.ed.ac.uk Fri Jan 18 10:39:00 2008 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Fri, 18 Jan 2008 15:39:00 +0000 Subject: [TYPES] paper on gradual typing with inference In-Reply-To: References: Message-ID: <4790C814.1070304@inf.ed.ac.uk> Tim, If you set it up carefully, it is possible to mix polymorphic functions with gradual typing and maintain parametricity. Here is a paper that discusses the key idea in the context of contracts: Relationally-parametric polymorphic contracts A Guha, J Matthews, RB Findler, S Krishnamurthi - Proceedings of the 2007 symposium on Dynamic languages, 2007 - portal.acm.org Also look out for forthcoming papers on this topic by Jacob Matthews, Amal Ahmed, Robby Finder, and Philip Wadler (all together and in various combinations). Cheers, -- P Tim Sweeney wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello, > > This is a welcome work on gradual typing. > > Now, please pardon me for using this thread to note something relevant to dynamic and gradual typing, which I haven't seen said elsewhere: > > Any language with a dynamic or gradual type system is necessarily either partial (potentially non-terminating), or aparametric (admitting programs that violate the parametricity property, described in http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html). > > This is the case because a dynamically typed fragment of a program may coerce a value of unknown type to a specific type required in a context, such as coercing x to a numeric type in x+1. > > A coercion which fails may provide a means such as exception-handling or returning an appropriately typed indicator value (such as the integer value 0) which the program can observe and act upon. In this case, the language is aparametric, as it allows extracting information from a value of universal type. But parametricity is a valuable security property in languages: a pure function with a parameter of universally quantified type guarantees that it cannot inspect that parameter, but can only place it somewhere in its result value. > > If failed coercions always cause an unrecoverable program abort, then it's observably equivalent to any other divergent outcome. Hence the language doesn't necessarily violate parametricity, but it is certainly partial. > > Because gradual typing, total programming, and parametricity are all desirable features in a language, I wanted to note that a type system can soundly support all three in the following way: > > Start with a total language, and extend it using e.g. Haskell style monads, or effects-typing, to support aparametricity and partiality as effects. At the top level of a program, both would be allowed. Once a function is invoked with requires parametricity or totality, the type system guarantees that it cannot perform operations which are either partial or aparametricity. > > This approach could be extended further, to the extent of treating every axiom underlying a type system as an independent effect, enabling portions of code to be verified within restrictive fragments of the type system guaranteeing other properties such as linearity, non-commutativity, etc. > > This provides an interesting means for soundly layering future proofs-of-programs features requiring parametricity and totality on top of existing languages and runtime frameworks which are more lax. > > Tim Sweeney > > -----Original Message----- > From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Jeremy Siek > Sent: Wednesday, January 16, 2008 7:14 PM > To: type-list > Subject: [TYPES] paper on gradual typing with inference > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Colleagues, > > We are pleased to share with you a new paper about integrating > gradual typing and unification-based type inference (which > underlies the Hindley-Milner type system). This was one of > those systems where the algorithm was easy to come up > with, but the type system was somewhat tricky. > > http://ece.colorado.edu/~siek/pldi08gradual.pdf > > Any comments or suggests are most welcome. > > The paper is under review for PLDI 2008**. > > Best regards, > Jeremy Siek & Manish Vachharajani > > **The review was double blind, but the reviews have already been > submitted and the identities of the authors revealed. > > ____________________________________ > Jeremy Siek > http://ece.colorado.edu/~siek/ > Assistant Professor > Dept. of Electrical and Computer Engineering > University of Colorado at Boulder > > > > -- \ Philip Wadler, Professor of Theoretical Computer Science /\ School of Informatics, University of Edinburgh / \ http://homepages.inf.ed.ac.uk/wadler/ From matthias at ccs.neu.edu Fri Jan 18 09:54:18 2008 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Fri, 18 Jan 2008 09:54:18 -0500 Subject: [TYPES] paper on gradual typing with inference In-Reply-To: References: Message-ID: Parametricity has indeed been a stumbling block for our work on Typed Scheme -- a full-fledged practical and sound implementation of gradual static typing for a production programming language (see POPL 2008 for the paper, with Sam Tobin-Hochstadt). We are working with the rest of PLT though, and Jacob Matthews @ UChicago (with Amal) plus others have made good progress on this: ESOP 2008: Parametric polymorphism through run-time sealing, or Theorems for low, low prices! (Jacob Matthews and Amal Ahmed) is probably the best citation for your purposes. We intend to build on this for the integration of parametric polymorphism at module boundaries. -- Matthias On Jan 17, 2008, at 5:40 PM, Tim Sweeney wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > Hello, > > This is a welcome work on gradual typing. > > Now, please pardon me for using this thread to note something > relevant to dynamic and gradual typing, which I haven't seen said > elsewhere: > > Any language with a dynamic or gradual type system is necessarily > either partial (potentially non-terminating), or aparametric > (admitting programs that violate the parametricity property, > described in http://homepages.inf.ed.ac.uk/wadler/topics/ > parametricity.html). > > This is the case because a dynamically typed fragment of a program > may coerce a value of unknown type to a specific type required in a > context, such as coercing x to a numeric type in x+1. > > A coercion which fails may provide a means such as exception- > handling or returning an appropriately typed indicator value (such > as the integer value 0) which the program can observe and act > upon. In this case, the language is aparametric, as it allows > extracting information from a value of universal type. But > parametricity is a valuable security property in languages: a pure > function with a parameter of universally quantified type guarantees > that it cannot inspect that parameter, but can only place it > somewhere in its result value. > > If failed coercions always cause an unrecoverable program abort, > then it's observably equivalent to any other divergent outcome. > Hence the language doesn't necessarily violate parametricity, but > it is certainly partial. > > Because gradual typing, total programming, and parametricity are > all desirable features in a language, I wanted to note that a type > system can soundly support all three in the following way: > > Start with a total language, and extend it using e.g. Haskell style > monads, or effects-typing, to support aparametricity and partiality > as effects. At the top level of a program, both would be allowed. > Once a function is invoked with requires parametricity or totality, > the type system guarantees that it cannot perform operations which > are either partial or aparametricity. > > This approach could be extended further, to the extent of treating > every axiom underlying a type system as an independent effect, > enabling portions of code to be verified within restrictive > fragments of the type system guaranteeing other properties such as > linearity, non-commutativity, etc. > > This provides an interesting means for soundly layering future > proofs-of-programs features requiring parametricity and totality on > top of existing languages and runtime frameworks which are more lax. > > Tim Sweeney > > -----Original Message----- > From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list- > bounces at lists.seas.upenn.edu] On Behalf Of Jeremy Siek > Sent: Wednesday, January 16, 2008 7:14 PM > To: type-list > Subject: [TYPES] paper on gradual typing with inference > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > Dear Colleagues, > > We are pleased to share with you a new paper about integrating > gradual typing and unification-based type inference (which > underlies the Hindley-Milner type system). This was one of > those systems where the algorithm was easy to come up > with, but the type system was somewhat tricky. > > http://ece.colorado.edu/~siek/pldi08gradual.pdf > > Any comments or suggests are most welcome. > > The paper is under review for PLDI 2008**. > > Best regards, > Jeremy Siek & Manish Vachharajani > > **The review was double blind, but the reviews have already been > submitted and the identities of the authors revealed. > > ____________________________________ > Jeremy Siek > http://ece.colorado.edu/~siek/ > Assistant Professor > Dept. of Electrical and Computer Engineering > University of Colorado at Boulder > > > > From jeremy.siek at gmail.com Fri Jan 18 14:02:13 2008 From: jeremy.siek at gmail.com (Jeremy Siek) Date: Fri, 18 Jan 2008 12:02:13 -0700 Subject: [TYPES] paper on gradual typing with inference In-Reply-To: References: Message-ID: Hi Tim, Matthias, Phil, On Jan 18, 2008, at 7:54 AM, Matthias Felleisen wrote: > > Parametricity has indeed been a stumbling block for our work on > Typed Scheme -- a full-fledged practical and sound implementation > of gradual static typing for a production programming language (see > POPL 2008 for the paper, with Sam Tobin-Hochstadt). We are working > with the rest of PLT though, and Jacob Matthews @ UChicago (with > Amal) plus others have made good progress on this: > > ESOP 2008: Parametric polymorphism through run-time sealing, > or Theorems for low, low prices! (Jacob Matthews and Amal Ahmed) > is probably the best citation for your purposes. > > We intend to build on this for the integration of parametric > polymorphism at module boundaries. -- Matthias Yes, I'd recommend both the above paper and the DSL 2007 paper Phil mentioned in the following email. Also, I'd like to point out a closely related issue (perhaps a different view on the same issue). Casts could allow programmers to introspect on a type, thereby breaking parametricity. For example, if one were allowed to write (using the notation of System F) f = /\ a. fun x:a. ((fun y:?. y + 1) a) then f is not really parametric because the program is checking whether 'a' is 'int'. In the design of our inference algorithm, there is a little bit of foreshadowing of this problem and one way to solve it. During inference, if a type variable is constrained by a ? and nothing more specific, then the type variable resolves to ? (so it does not stay a type variable). Extending this to a Hindley-Milner setting, this means we would not generalize that type variable. For example, in let f = fun x. ((fun y:?. y +1) a) in ... we have f : ? -> int and not f : forall a. a -> int Thus, with this approach we consider casts as yet another kind of operation that rules out polymorphism. Cheers, Jeremy > > > On Jan 17, 2008, at 5:40 PM, Tim Sweeney wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ >> types-list ] >> >> Hello, >> >> This is a welcome work on gradual typing. >> >> Now, please pardon me for using this thread to note something >> relevant to dynamic and gradual typing, which I haven't seen said >> elsewhere: >> >> Any language with a dynamic or gradual type system is necessarily >> either partial (potentially non-terminating), or aparametric >> (admitting programs that violate the parametricity property, >> described in http://homepages.inf.ed.ac.uk/wadler/topics/ >> parametricity.html). >> >> This is the case because a dynamically typed fragment of a program >> may coerce a value of unknown type to a specific type required in >> a context, such as coercing x to a numeric type in x+1. >> >> A coercion which fails may provide a means such as exception- >> handling or returning an appropriately typed indicator value (such >> as the integer value 0) which the program can observe and act >> upon. In this case, the language is aparametric, as it allows >> extracting information from a value of universal type. But >> parametricity is a valuable security property in languages: a pure >> function with a parameter of universally quantified type >> guarantees that it cannot inspect that parameter, but can only >> place it somewhere in its result value. >> >> If failed coercions always cause an unrecoverable program abort, >> then it's observably equivalent to any other divergent outcome. >> Hence the language doesn't necessarily violate parametricity, but >> it is certainly partial. >> >> Because gradual typing, total programming, and parametricity are >> all desirable features in a language, I wanted to note that a type >> system can soundly support all three in the following way: >> >> Start with a total language, and extend it using e.g. Haskell >> style monads, or effects-typing, to support aparametricity and >> partiality as effects. At the top level of a program, both would >> be allowed. Once a function is invoked with requires >> parametricity or totality, the type system guarantees that it >> cannot perform operations which are either partial or aparametricity. >> >> This approach could be extended further, to the extent of treating >> every axiom underlying a type system as an independent effect, >> enabling portions of code to be verified within restrictive >> fragments of the type system guaranteeing other properties such as >> linearity, non-commutativity, etc. >> >> This provides an interesting means for soundly layering future >> proofs-of-programs features requiring parametricity and totality >> on top of existing languages and runtime frameworks which are more >> lax. >> >> Tim Sweeney >> >> -----Original Message----- >> From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list- >> bounces at lists.seas.upenn.edu] On Behalf Of Jeremy Siek >> Sent: Wednesday, January 16, 2008 7:14 PM >> To: type-list >> Subject: [TYPES] paper on gradual typing with inference >> >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ >> types-list ] >> >> Dear Colleagues, >> >> We are pleased to share with you a new paper about integrating >> gradual typing and unification-based type inference (which >> underlies the Hindley-Milner type system). This was one of >> those systems where the algorithm was easy to come up >> with, but the type system was somewhat tricky. >> >> http://ece.colorado.edu/~siek/pldi08gradual.pdf >> >> Any comments or suggests are most welcome. >> >> The paper is under review for PLDI 2008**. >> >> Best regards, >> Jeremy Siek & Manish Vachharajani >> >> **The review was double blind, but the reviews have already been >> submitted and the identities of the authors revealed. >> >> ____________________________________ >> Jeremy Siek >> http://ece.colorado.edu/~siek/ >> Assistant Professor >> Dept. of Electrical and Computer Engineering >> University of Colorado at Boulder >> >> >> >> > From david.hopwood at industrial-designers.co.uk Sat Jan 19 17:00:51 2008 From: david.hopwood at industrial-designers.co.uk (David Hopwood) Date: Sat, 19 Jan 2008 22:00:51 +0000 Subject: [TYPES] paper on gradual typing with inference In-Reply-To: References: Message-ID: <47927313.6060103@industrial-designers.co.uk> Tim Sweeney wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello, > > This is a welcome work on gradual typing. > > Now, please pardon me for using this thread to note something relevant to dynamic > and gradual typing, which I haven't seen said elsewhere: > > Any language with a dynamic or gradual type system is necessarily either partial > (potentially non-terminating), or aparametric (admitting programs that violate > the parametricity property, described in > http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html). > > This is the case because a dynamically typed fragment of a program may coerce a > value of unknown type to a specific type required in a context, such as coercing > x to a numeric type in x+1. > > A coercion which fails may provide a means such as exception-handling or returning an > appropriately typed indicator value (such as the integer value 0) which the program > can observe and act upon. In this case, the language is aparametric, as it allows > extracting information from a value of universal type. But parametricity is a valuable > security property in languages: a pure function with a parameter of universally > quantified type guarantees that it cannot inspect that parameter, but can only place > it somewhere in its result value. Parametricity is one way to achieve this security property, but it can also be achieved in other ways that do not involve parametricity (and are simpler than the approach you suggest using monads or effects-typing, I think). For example, class-based object-oriented programming languages typically support private instance variables. So an instance of a "box" class with a private field holding some value (possibly of a parameterized type) can be passed to a pure function with the same practical effect as passing a parameter of universally quantified type in a language with parametricity: the function can only return the box. (If the function is impure, it can also place a reference to the box elsewhere, but still cannot obtain the encapulated value.) Obtaining the value from the box can either require use of a token/capability value, or can be restricted to a certain lexical region of the program. Class-based object-orientation can be simulated easily just using lexically scoped closures, so this technique can be used in a wide range of languages, including languages that are both total and gradually typed. -- David Hopwood From geoffrey.washburn at epfl.ch Mon Jan 21 09:22:01 2008 From: geoffrey.washburn at epfl.ch (Geoffrey Alan Washburn) Date: Mon, 21 Jan 2008 15:22:01 +0100 Subject: [TYPES] paper on gradual typing with inference In-Reply-To: <4790C814.1070304@inf.ed.ac.uk> References: <4790C814.1070304@inf.ed.ac.uk> Message-ID: <4794AA89.3090502@epfl.ch> Philip Wadler wrote: > If you set it up carefully, it is possible to mix polymorphic functions > with gradual typing and maintain parametricity. It is also worth noting that it is possible to develop a generalization of the parametricity theorem that holds in languages with runtime type analysis, and should be applicable to languages with adhoc polymorphism and other sorts of dynamic type tests. In the polymorphic lambda-calculus, no expression is allowed to depend upon how an abstract type may be instantiated. The first key insight is that this property is merely one end of a spectrum. At the other end of the spectrum, any expression in a term may depend on the instantiation of any possible abstract type. In between, some expressions may be depend on the instantiation of some abstract types. I expect most programs using runtime type analysis, etc. fall somewhere in this part of the spectrum. The second key insight is that in the polymorphic lambda-calculus this dependency relationship (or rather the lack of dependency) is implicit. Therefore, if we augment the type system to make it possible to express the dependencies between abstract types and expressions explicitly, it is possible to reason about these other points in the spectrum. Information-flow type systems are an example of a class of type systems that makes dependencies between expressions explicit by labeling types. Therefore, one way that the dependencies could be made explicit is to augment the type system of the polymorphic lambda-calculus with information-flow labels on both types and kinds. For example, assuming that the labels are drawn from a lattice with both top (Top) and bottom (Bot) elements. The type of the identity function in the polymorphic lambda-calculus, forall a:*. a -> a, where * is the base kind, could then be expressed in this augmented language as forall a:(* @ Top). a @ Bot -> a @ Bot. Here "* @ Top" is used to denote "a type with the information content Top", and "a @ Bot" is used to denote "a value of type 'a' with an information content of Bot". Therefore, for any given instantiation of the universal, the function takes values of that type, with no information content, to values of that type, again with no information content. Assuming that there is no general recursion, we know that this function must be the identity function because the information content of the of the value produced is less than the information content of the abstract type (Bot <: Top). This fact means that it is not possible for the value returned by the function to depend upon the type used to instantiate the universal. Therefore, the function must return its argument, because there is no other means of producing a value of the correct type. Alternately, if we have a function with the type forall a:(* @ Top). a @ Bot -> a @ Top it is possible that this function is not the identity because the value returned has a maximal information content. Therefore, the value returned might depend upon the chosen instantiation of the universal. For example, it could be the function that returns its argument, unless the argument is an integer, in which case, the function returns 0. For more information on this idea, you can read my LICS 2005 paper, written with Stephanie Weirich, "Generalizing Parametricity Using Information Flow". Even more information on this idea can be found in my dissertation. From P.B.Levy at cs.bham.ac.uk Wed Jan 23 14:09:43 2008 From: P.B.Levy at cs.bham.ac.uk (Paul B Levy) Date: Wed, 23 Jan 2008 19:09:43 +0000 (GMT) Subject: [TYPES] polymorphic isomorphisms Message-ID: Dear all, Do the following System F isomorphisms appear in the literature, and are they validated by the standard models? (1) Prod X. ((X -> B) -> A) cong A [ nu X. B / X ] where X is negative in A and positive in B (2) Prod X. ((B -> X) -> A) cong A [ mu X. B / X ] where X is positive in A and B Also, are any other isomorphisms (beyond the obvious beta-eta ones) known? (By "isomorphism" I mean definable both ways by terms that are inverse up to observational equivalence.) The following isomorphisms are similar, but they're already derivable from (1)-(2). (3) Sum X. ((X -> B) x A) cong A [ nu X. B / X ] where X is positive in A and B (4) Sum X. ((B -> X) x A) cong A [ mu X. B / X ] where X is negative in A and positive in B regards, Paul -- Paul Blain Levy email: pbl at cs.bham.ac.uk School of Computer Science, University of Birmingham Birmingham B15 2TT, U.K. tel: +44 121-414-4792 http://www.cs.bham.ac.uk/~pbl From P.B.Levy at cs.bham.ac.uk Wed Jan 23 14:51:25 2008 From: P.B.Levy at cs.bham.ac.uk (Paul B Levy) Date: Wed, 23 Jan 2008 19:51:25 +0000 (GMT) Subject: [TYPES] polymorphic isomorphisms In-Reply-To: References: Message-ID: On Wed, 23 Jan 2008, Paul B Levy wrote: > Also, are any other isomorphisms (beyond the obvious beta-eta ones) known? Having just looked at Fiore, di Cosmo and Balat's "Remarks on isomorphisms in typed lambda calculi with empty and sum types", please scratch the word "obvious" from before "beta-eta"! Paul From txa at Cs.Nott.AC.UK Thu Jan 24 09:24:40 2008 From: txa at Cs.Nott.AC.UK (Thorsten Altenkirch) Date: Thu, 24 Jan 2008 14:24:40 +0000 Subject: [TYPES] polymorphic isomorphisms In-Reply-To: References: Message-ID: <7CBA63BD-79A5-4AF1-9092-AC2B4FDD365A@cs.nott.ac.uk> Hi Paul, we know that parametricity implies that mu X.B(X) ~ Pi X.(B(X) -> X) -> X where X is positive in B. Your question (2) seems to boil down to A(Pi X.(B(X) -> X) -> X) ~ Pi X.(B(X) -> X) -> A(X) which I think is also implied by parametricity (but I haven't checked it). As far as standard models are concerned: as far as I know it isn't so easy to construct a parametric model, this was done by Bainbridge et al and is called the "Parametric PER model". The standard PER models are in general not parametric, i.e. there is a counterexample by Ivar Rummelhof where he constructs a particular PCA so that the type polynat = Pi X.X -> (X->X) -> X contains non-standard numerals. I'd think that in this model also your isomorphisms should fail. Cheers, Thorsten On 23 Jan 2008, at 19:09, Paul B Levy wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > > > Dear all, > > Do the following System F isomorphisms appear in the literature, and > are they validated by the standard models? > > (1) > > Prod X. ((X -> B) -> A) cong A [ nu X. B / X ] > where X is negative in A and positive in B > > (2) > > Prod X. ((B -> X) -> A) cong A [ mu X. B / X ] > where X is positive in A and B > > Also, are any other isomorphisms (beyond the obvious beta-eta ones) > known? > (By "isomorphism" I mean definable both ways by terms that are > inverse up > to observational equivalence.) > > The following isomorphisms are similar, but they're already > derivable from > (1)-(2). > > (3) > > Sum X. ((X -> B) x A) cong A [ nu X. B / X ] > where X is positive in A and B > > (4) > > Sum X. ((B -> X) x A) cong A [ mu X. B / X ] > where X is negative in A and positive in B > > regards, > Paul > > > > -- > Paul Blain Levy email: pbl at cs.bham.ac.uk > School of Computer Science, University of Birmingham > Birmingham B15 2TT, U.K. tel: +44 121-414-4792 > http://www.cs.bham.ac.uk/~pbl 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 intrwbrwsar at netzero.net Thu Jan 24 10:44:13 2008 From: intrwbrwsar at netzero.net (intrwbrwsar@netzero.net) Date: Thu, 24 Jan 2008 15:44:13 GMT Subject: [TYPES] polymorphic isomorphisms Message-ID: <20080124.074413.17193.1@webmail07.dca.untd.com> There are papers on embedding morphisms and models that might apply. For example, you can glance at an application areas that might appear a distraction at everyday glance from what you consider as types and polymorphisms I had written on: visualization and a hard straddle amongst practical objects, Gentzen systems, on and on. Cyrus http://projektakdmkrd.tripod.com -- Thorsten Altenkirch wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hi Paul, we know that parametricity implies that mu X.B(X) ~ Pi X.(B(X) -> X) -> X where X is positive in B. Your question (2) seems to boil down to A(Pi X.(B(X) -> X) -> X) ~ Pi X.(B(X) -> X) -> A(X) which I think is also implied by parametricity (but I haven't checked it). As far as standard models are concerned: as far as I know it isn't so easy to construct a parametric model, this was done by Bainbridge et al and is called the "Parametric PER model". The standard PER models are in general not parametric, i.e. there is a counterexample by Ivar Rummelhof where he constructs a particular PCA so that the type polynat = Pi X.X -> (X->X) -> X contains non-standard numerals. I'd think that in this model also your isomorphisms should fail. Cheers, Thorsten On 23 Jan 2008, at 19:09, Paul B Levy wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > > > Dear all, > > Do the following System F isomorphisms appear in the literature, and > are they validated by the standard models? > > (1) > > Prod X. ((X -> B) -> A) cong A [ nu X. B / X ] > where X is negative in A and positive in B > > (2) > > Prod X. ((B -> X) -> A) cong A [ mu X. B / X ] > where X is positive in A and B > > Also, are any other isomorphisms (beyond the obvious beta-eta ones) > known? > (By "isomorphism" I mean definable both ways by terms that are > inverse up > to observational equivalence.) > > The following isomorphisms are similar, but they're already > derivable from > (1)-(2). > > (3) > > Sum X. ((X -> B) x A) cong A [ nu X. B / X ] > where X is positive in A and B > > (4) > > Sum X. ((B -> X) x A) cong A [ mu X. B / X ] > where X is negative in A and positive in B > > regards, > Paul > > > > -- > Paul Blain Levy email: pbl at cs.bham.ac.uk > School of Computer Science, University of Birmingham > Birmingham B15 2TT, U.K. tel: +44 121-414-4792 > http://www.cs.bham.ac.uk/~pbl 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. _____________________________________________________________ Click to get 100% digital commercial-free music. http://thirdpartyoffers.netzero.net/TGL2211/fc/Ioyw6ijmlTh9QnERS52ntJNdT0jyI6evJcA04UDFKQsTmvhkfw4iEJ/ From devriese at cs.tcd.ie Thu Jan 24 11:38:26 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Thu, 24 Jan 2008 16:38:26 +0000 Subject: [TYPES] Isorecursive types and type abstraction Message-ID: <20080124163825.GF28553@netsoc.tcd.ie> (Originally sent to haskell-cafe; someone suggested posting it here) Hi, Most descriptions of recursive types state that iso-recursive types (with explicit 'fold' and 'unfold' operators) are easy to typecheck, and that equi-recursive types are much more difficult. My question regards using iso-recursive types (explicitly, not implicitly using algebraic data types) together with type abstraction and application. The usual typing rules for fold and unfold are e :: Fix X. t ----------------------------- Unfold unfold e :: [X := Fix X. t] t e :: [X := Fix X. t] t ----------------------------- Fold fold e : Fix X. t This works ok for the following type: ListInt = Fix L. 1 + Int * L (where "1" is the unit type). If x :: ListInt then unfold x :: 1 + Int * ListInt using the Unfold typing rule. However, this breaks when using type abstraction and application. Consider the polymorphic version of list: List = Fix L. /\A. 1 + A * L A Now if we have x :: List Int we can no longer type unfold x because x does not have type (Fix ..), but ((Fix ..) Int) instead. Of course, we can unroll List Int by first unrolling List, and then re-applying the unrolled type to Int to get (/\A. 1 + A * (Fix L. /\A. 1 * L A) A) Int which can be simplified to 1 + Int * List Int but this is not usually mentioned (that I could find; in particular, TAPL does not mention it) and I'm worried that there are subtleties here that I'm missing--nor do I have an exact definition of what this 'extended' unrolling rule should do. Any hints or pointers to relevant literature would be appreciated! Edsko PS. One way to simplify the problem is to redefine List as List = /\A. Fix L. 1 + A * L so that List Int can easily be simplified to the right form (Fix ..); but that can only be done for regular datatypes. For example, the nested type Perfect = Fix L. /\A. A + Perfect (A, A) cannot be so rewritten because the argument to Perfect in the recursive call is different. From sweirich at cis.upenn.edu Thu Jan 24 11:56:11 2008 From: sweirich at cis.upenn.edu (Stephanie Weirich) Date: Thu, 24 Jan 2008 11:56:11 -0500 Subject: [TYPES] Types-list post from devriese@cs.tcd.ie requires approval In-Reply-To: References: Message-ID: <119972E8-FECE-4C9C-8059-75216E828729@cis.upenn.edu> Hi Edsko, What you need is a higher-kinded version of Fix (parameterized recursive type), with the associated fold and unfold rules. You can find these rules in the paper: Flexible Type Analysis, Karl Crary and Stephanie Weirich, ICFP 99 http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf --Stephanie > > From: Edsko de Vries > Date: January 24, 2008 11:38:26 AM EST > To: types-list at lists.seas.upenn.edu > Subject: Isorecursive types and type abstraction > > > (Originally sent to haskell-cafe; someone suggested posting it here) > > Hi, > > Most descriptions of recursive types state that iso-recursive types > (with explicit 'fold' and 'unfold' operators) are easy to typecheck, > and that equi-recursive types are much more difficult. My question > regards using iso-recursive types (explicitly, not implicitly using > algebraic data types) together with type abstraction and application. > > The usual typing rules for fold and unfold are > > e :: Fix X. t > ----------------------------- Unfold > unfold e :: [X := Fix X. t] t > > e :: [X := Fix X. t] t > ----------------------------- Fold > fold e : Fix X. t > > This works ok for the following type: > > ListInt = Fix L. 1 + Int * L > > (where "1" is the unit type). If > > x :: ListInt > > then > > unfold x :: 1 + Int * ListInt > > using the Unfold typing rule. However, this breaks when using type > abstraction and application. Consider the polymorphic version of list: > > List = Fix L. /\A. 1 + A * L A > > Now if we have > > x :: List Int > > we can no longer type > > unfold x > > because x does not have type (Fix ..), but ((Fix ..) Int) instead. Of > course, we can unroll List Int by first unrolling List, and then > re-applying the unrolled type to Int to get > > (/\A. 1 + A * (Fix L. /\A. 1 * L A) A) Int > > which can be simplified to > > 1 + Int * List Int > > but this is not usually mentioned (that I could find; in > particular, TAPL does not mention it) and I'm worried that there > are subtleties here that I'm missing--nor do I have an exact > definition of what this 'extended' unrolling rule should do. > > Any hints or pointers to relevant literature would be appreciated! > > Edsko > > PS. One way to simplify the problem is to redefine List as > > List = /\A. Fix L. 1 + A * L > > so that List Int can easily be simplified to the right form (Fix ..); > but that can only be done for regular datatypes. For example, the > nested > type > > Perfect = Fix L. /\A. A + Perfect (A, A) > > cannot be so rewritten because the argument to Perfect in the > recursive > call is different. > > From devriese at cs.tcd.ie Thu Jan 24 13:05:43 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Thu, 24 Jan 2008 18:05:43 +0000 Subject: [TYPES] Isorecursive types and type abstraction In-Reply-To: <119972E8-FECE-4C9C-8059-75216E828729@cis.upenn.edu> References: <119972E8-FECE-4C9C-8059-75216E828729@cis.upenn.edu> Message-ID: <20080124180543.GD29018@netsoc.tcd.ie> Hi Stephanie, > What you need is a higher-kinded version of Fix (parameterized > recursive type), with the associated fold and unfold rules. You can > find these rules in the paper: > > Flexible Type Analysis, Karl Crary and Stephanie Weirich, ICFP 99 > > http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf Thank you for your answer. The paper looks interesting and I will study it. Do I understand correctly that it will give me a fix operator that allows me to rewrite Perfect and lift the /\A over the Fix operator, just like for List? In a way though that circumvents the problem I'm having rather than solving it. That is ok, but it does mean having to introduce a more complicated Fix operator, and it seems to me that there should be simpler solution. But perhaps there isn't. Either, I appreciate the pointer. Thanks! Edsko From sweirich at cis.upenn.edu Thu Jan 24 13:28:12 2008 From: sweirich at cis.upenn.edu (Stephanie Weirich) Date: Thu, 24 Jan 2008 13:28:12 -0500 Subject: [TYPES] Isorecursive types and type abstraction In-Reply-To: <20080124180543.GD29018@netsoc.tcd.ie> References: <119972E8-FECE-4C9C-8059-75216E828729@cis.upenn.edu> <20080124180543.GD29018@netsoc.tcd.ie> Message-ID: Hi Edsko, Yes, you can write perfect as /\A:*. rec (/\P. a + P (A, A), A) (and your original version of list as: List = /\A:*. rec (/\L. 1 + (A, L A), A) ) The reason that it is complicated is that the rec operator is creating a recursive type with a higher kind (i.e. a type constructor of kind *->*) but fold and unfold need to work with expressions that are classified by types (with kind *). Therefore, the second argument to rec is a parameter to the type constructor that turns it into a type. We can simplify the rules in the paper a bit by uncurrying the arguments to rec: G |- c1 : (k -> *) -> k -> * G |- c2 : k --------------------------------------------- G |- rec c1 c2 : * with the typing rule for fold (unfold is the reverse): G |- e : c1 (rec c1) c2 -------------------------------- G |- fold x : rec c1 c2 And if you specialize the above rule to List Int (i.e. c1 = List above, c2 = Int), you get: G |- x : 1 + (Int, List Int) ----------------------------- G |- fold x : List Int ---Stephanie On Jan 24, 2008, at 1:05 PM, Edsko de Vries wrote: > Hi Stephanie, > >> What you need is a higher-kinded version of Fix (parameterized >> recursive type), with the associated fold and unfold rules. You can >> find these rules in the paper: >> >> Flexible Type Analysis, Karl Crary and Stephanie Weirich, ICFP 99 >> >> http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf > > Thank you for your answer. The paper looks interesting and I will > study > it. Do I understand correctly that it will give me a fix operator that > allows me to rewrite Perfect and lift the /\A over the Fix operator, > just like for List? > > In a way though that circumvents the problem I'm having rather than > solving it. That is ok, but it does mean having to introduce a more > complicated Fix operator, and it seems to me that there should be > simpler solution. But perhaps there isn't. > > Either, I appreciate the pointer. Thanks! > > Edsko From crary at cs.cmu.edu Thu Jan 24 13:51:31 2008 From: crary at cs.cmu.edu (Karl Crary) Date: Thu, 24 Jan 2008 13:51:31 -0500 Subject: [TYPES] Types-list post from devriese@cs.tcd.ie requires approval In-Reply-To: <119972E8-FECE-4C9C-8059-75216E828729@cis.upenn.edu> References: <119972E8-FECE-4C9C-8059-75216E828729@cis.upenn.edu> Message-ID: <4798DE33.6030702@cs.cmu.edu> I would add our formulation of recursive types in that paper came from Mendler (and can be found in the Nuprl book of Constable et al.). I'm not sure to whom it is originally due. This is the simple formulation of higher-order isorecursive types, in that it only forms types. Higher-kinded recursive types are then encoded using it. Others have looked at formulations in which higher-kinded recursive type constructors are introduced directly, at the cost of more complicated roll/unroll operations. The basic idea is that roll/unroll operate on types taking the form of a recursive constructor within a context (usually an elimnation context). I've seen this done fairly often. I don't know the canonical reference, but I think that Rossberg's Alice ML does something like that. -- Karl Crary Stephanie Weirich wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi Edsko, > > What you need is a higher-kinded version of Fix (parameterized > recursive type), with the associated fold and unfold rules. You can > find these rules in the paper: > > Flexible Type Analysis, Karl Crary and Stephanie Weirich, ICFP 99 > > http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf > > --Stephanie > > >> From: Edsko de Vries >> Date: January 24, 2008 11:38:26 AM EST >> To: types-list at lists.seas.upenn.edu >> Subject: Isorecursive types and type abstraction >> >> >> (Originally sent to haskell-cafe; someone suggested posting it here) >> >> Hi, >> >> Most descriptions of recursive types state that iso-recursive types >> (with explicit 'fold' and 'unfold' operators) are easy to typecheck, >> and that equi-recursive types are much more difficult. My question >> regards using iso-recursive types (explicitly, not implicitly using >> algebraic data types) together with type abstraction and application. >> >> The usual typing rules for fold and unfold are >> >> e :: Fix X. t >> ----------------------------- Unfold >> unfold e :: [X := Fix X. t] t >> >> e :: [X := Fix X. t] t >> ----------------------------- Fold >> fold e : Fix X. t >> >> This works ok for the following type: >> >> ListInt = Fix L. 1 + Int * L >> >> (where "1" is the unit type). If >> >> x :: ListInt >> >> then >> >> unfold x :: 1 + Int * ListInt >> >> using the Unfold typing rule. However, this breaks when using type >> abstraction and application. Consider the polymorphic version of list: >> >> List = Fix L. /\A. 1 + A * L A >> >> Now if we have >> >> x :: List Int >> >> we can no longer type >> >> unfold x >> >> because x does not have type (Fix ..), but ((Fix ..) Int) instead. Of >> course, we can unroll List Int by first unrolling List, and then >> re-applying the unrolled type to Int to get >> >> (/\A. 1 + A * (Fix L. /\A. 1 * L A) A) Int >> >> which can be simplified to >> >> 1 + Int * List Int >> >> but this is not usually mentioned (that I could find; in >> particular, TAPL does not mention it) and I'm worried that there >> are subtleties here that I'm missing--nor do I have an exact >> definition of what this 'extended' unrolling rule should do. >> >> Any hints or pointers to relevant literature would be appreciated! >> >> Edsko >> >> PS. One way to simplify the problem is to redefine List as >> >> List = /\A. Fix L. 1 + A * L >> >> so that List Int can easily be simplified to the right form (Fix ..); >> but that can only be done for regular datatypes. For example, the >> nested >> type >> >> Perfect = Fix L. /\A. A + Perfect (A, A) >> >> cannot be so rewritten because the argument to Perfect in the >> recursive >> call is different. >> >> >> > > > From dreyer at mpi-sws.mpg.de Thu Jan 24 22:28:03 2008 From: dreyer at mpi-sws.mpg.de (Derek Dreyer) Date: Fri, 25 Jan 2008 04:28:03 +0100 Subject: [TYPES] Isorecursive types and type abstraction In-Reply-To: <20080124163825.GF28553@netsoc.tcd.ie> References: <20080124163825.GF28553@netsoc.tcd.ie> Message-ID: <7fa251b70801241928x1d3c0afbk4ef77a58cfb086dd@mail.gmail.com> Edsko, To follow up on what Karl said, if you want to see a formalization of a language with iso-recursive type constructors at higher kind (i.e. of kind K, where K is not restricted to be of the form K' -> Type but may include arbitrary arrows and also product kinds), you could take a look at chapter 6 of my PhD thesis: http://tti-c.org/dreyer/thesis/main.pdf I wouldn't claim that the formalization of iso-recursive higher-kinded constructors here is original, but there is an aspect of the meta-theory studied here that *is* original (see below). In any case, it more or less follows along the lines that Karl suggested. In particular, you have an iso-recursive type constructor Mu alpha:K. A, which has kind K as long as A has kind K under the assumption that alpha does. Equivalence of these mu-constructors is purely structural (no "equi-recursive" unfolding at the type level). Then, a recursive "type" (i.e. of kind Type) just takes the form E{Mu alpha:K.A}, where E is an elimination (a sequence of projections and applications) applied to a Mu-constructor, resulting in a type of kind Type. In the case that K = Type itself, E is the empty path. If K = K' -> K'' -> Type, then E is a sequence of two applications (to constructors of kinds K' and K''), etc. And then the "fold" and "unfold" coercions at this recursive type just coerce between E{Mu alpha:K.A} and E{A[Mu alpha:K.A/alpha]}, which in the chapter are written "Q" and "expand(Q)", respectively. What I've described above is a pretty straightforward extension to F-omega. However, in my thesis, I also considered iso-recursive higher-kinded constructors as an extension to a language with dependent and *singleton* kinds a la Stone and Harper. (This combination arose quite naturally in modeling the type theory of a recursive module system.) Such an extension turns out to be surprisingly tricky, essentially because, when singleton kinds appear to the left of an arrow in the kind of a Mu-constructor, the unfolding of a recursive type rooted at that constructor is not always well-kinded. (See Section 6.2 for an example.) In that chapter, I showed that you could work around this by "monster-barring" such examples (which was not obvious how to do), but I was never totally satisfied with that solution. Derek On 1/24/08, Edsko de Vries wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > (Originally sent to haskell-cafe; someone suggested posting it here) > > Hi, > > Most descriptions of recursive types state that iso-recursive types > (with explicit 'fold' and 'unfold' operators) are easy to typecheck, > and that equi-recursive types are much more difficult. My question > regards using iso-recursive types (explicitly, not implicitly using > algebraic data types) together with type abstraction and application. > > The usual typing rules for fold and unfold are > > e :: Fix X. t > ----------------------------- Unfold > unfold e :: [X := Fix X. t] t > > e :: [X := Fix X. t] t > ----------------------------- Fold > fold e : Fix X. t > > This works ok for the following type: > > ListInt = Fix L. 1 + Int * L > > (where "1" is the unit type). If > > x :: ListInt > > then > > unfold x :: 1 + Int * ListInt > > using the Unfold typing rule. However, this breaks when using type > abstraction and application. Consider the polymorphic version of list: > > List = Fix L. /\A. 1 + A * L A > > Now if we have > > x :: List Int > > we can no longer type > > unfold x > > because x does not have type (Fix ..), but ((Fix ..) Int) instead. Of > course, we can unroll List Int by first unrolling List, and then > re-applying the unrolled type to Int to get > > (/\A. 1 + A * (Fix L. /\A. 1 * L A) A) Int > > which can be simplified to > > 1 + Int * List Int > > but this is not usually mentioned (that I could find; in particular, TAPL does not mention it) and I'm worried that there are subtleties here that I'm missing--nor do I have an exact definition of what this 'extended' unrolling rule should do. > > Any hints or pointers to relevant literature would be appreciated! > > Edsko > > PS. One way to simplify the problem is to redefine List as > > List = /\A. Fix L. 1 + A * L > > so that List Int can easily be simplified to the right form (Fix ..); > but that can only be done for regular datatypes. For example, the nested > type > > Perfect = Fix L. /\A. A + Perfect (A, A) > > cannot be so rewritten because the argument to Perfect in the recursive > call is different. > From devriese at cs.tcd.ie Fri Jan 25 06:47:42 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Fri, 25 Jan 2008 11:47:42 +0000 Subject: [TYPES] Isorecursive types and type abstraction In-Reply-To: <7fa251b70801241928x1d3c0afbk4ef77a58cfb086dd@mail.gmail.com> References: <20080124163825.GF28553@netsoc.tcd.ie> <7fa251b70801241928x1d3c0afbk4ef77a58cfb086dd@mail.gmail.com> Message-ID: <20080125114742.GA6805@netsoc.tcd.ie> Hey, Thanks all for your detailed answers. I will make sure to study all the given references :) Thanks, much appreciated! Edsko From monnier at iro.umontreal.ca Fri Jan 25 10:57:54 2008 From: monnier at iro.umontreal.ca (Stefan Monnier) Date: Fri, 25 Jan 2008 10:57:54 -0500 Subject: [TYPES] Isorecursive types and type abstraction In-Reply-To: <20080125114742.GA6805@netsoc.tcd.ie> (Edsko de Vries's message of "Fri, 25 Jan 2008 11:47:42 +0000") References: <20080124163825.GF28553@netsoc.tcd.ie> <7fa251b70801241928x1d3c0afbk4ef77a58cfb086dd@mail.gmail.com> <20080125114742.GA6805@netsoc.tcd.ie> Message-ID: > Thanks all for your detailed answers. I will make sure to study all the > given references :) You can also take a look at http://flint.cs.yale.edu/flint/publications/inductivemu.html which tried to solve this problem is a slightly different setting. Stefan From P.B.Levy at cs.bham.ac.uk Mon Jan 28 08:23:51 2008 From: P.B.Levy at cs.bham.ac.uk (Paul B Levy) Date: Mon, 28 Jan 2008 13:23:51 +0000 (GMT) Subject: [TYPES] Fwd: polymorphic isomorphisms In-Reply-To: References: <7CBA63BD-79A5-4AF1-9092-AC2B4FDD365A@cs.nott.ac.uk> Message-ID: Thanks Thorsten. Masahito Hasegawa pointed out to me that all the isomorphisms I mentioned are provable in Plotkin-Abadi logic and System R. Paul PS System F is consistent :-) On Mon, 28 Jan 2008, Thorsten Altenkirch wrote: > Hi Paul, > > On 24 Jan 2008, at 14:24, Thorsten Altenkirch wrote: >> we know that parametricity implies that >> >> mu X.B(X) ~ Pi X.(B(X) -> X) -> X >> >> where X is positive in B. Your question (2) seems to boil down to >> >> A(Pi X.(B(X) -> X) -> X) ~ Pi X.(B(X) -> X) -> A(X) >> >> which I think is also implied by parametricity (but I haven't checked >> it). > > I have now, it does indeed follow. The candidate isomorphism > > (phi,phi^-1) : A(mu X.B(X)) ~ Pi X.(B(X) -> X) -> A(X) > > clearly is > > phi a X f = A (fold X f) a > phi^-1 f = f mu in > > where mu X.B(X) = Pi X.(B(X) -> X) -> X , > fold : Pi X.(B(X) -> X) -> mu X.B(X) -> X > fold X f b = b X f > in : B(mu X.B(X)) -> mu X.B(X) > in b X f = f (B(fold f) b) > > To see that phi^-1 o phi = id we only need the functor laws for A and that > fold (mu X.B(X)) in = id which is indeed a part of Wadler's proof that mu > X.B(X) is initial. To show that phi o phi^-1 = id we need to employ > parametricity: given g : Pi X.(B(X) -> X) -> A(X) then for any B-algebra f: > A(C) -> C we have that f is related to in in the relational interpretation of > A(X) -> X applied to the graph of fold f, which I denote as (fold f)^#. > Hence, by parametricity of g we have that g X f and g (mu X. B(X)) in are > related in the raelational interpretation of B(X) applied to (fold f)^#, > which can be spells out as B (fold X f)(g (mu X.B(X) in) = g X f. This > implies the desired result using eta > > phi (phi^- g) = \ X f.B(fold f) (g mu X.B(X) in) > = \ X f .g X f > = g > > Background can be found in Wadler's seminal paper "Theorem's for free" and > his note "Recursive types for free!" available from > http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt > (was this ever published?). I also summarized this in a recent post on our > fp-lunch blog (http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=83). > > Disclaimer: For those who know me better, I'd like to point out that I > consider System F only as a formal game inspired by Type:Type, whose > consistency (i.e. Pi X.X is empty) is irrelevant for the discussion above. > :-) > > Cheers, > Thorsten > > P.S. Why are you actually interested in those isos? > > > > 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. > -- Paul Blain Levy email: pbl at cs.bham.ac.uk School of Computer Science, University of Birmingham Birmingham B15 2TT, U.K. tel: +44 121-414-4792 http://www.cs.bham.ac.uk/~pbl From txa at Cs.Nott.AC.UK Mon Jan 28 06:49:41 2008 From: txa at Cs.Nott.AC.UK (Thorsten Altenkirch) Date: Mon, 28 Jan 2008 11:49:41 +0000 Subject: [TYPES] Fwd: polymorphic isomorphisms References: <7CBA63BD-79A5-4AF1-9092-AC2B4FDD365A@cs.nott.ac.uk> Message-ID: Hi Paul, On 24 Jan 2008, at 14:24, Thorsten Altenkirch wrote: > we know that parametricity implies that > > mu X.B(X) ~ Pi X.(B(X) -> X) -> X > > where X is positive in B. Your question (2) seems to boil down to > > A(Pi X.(B(X) -> X) -> X) ~ Pi X.(B(X) -> X) -> A(X) > > which I think is also implied by parametricity (but I haven't checked > it). I have now, it does indeed follow. The candidate isomorphism (phi,phi^-1) : A(mu X.B(X)) ~ Pi X.(B(X) -> X) -> A(X) clearly is phi a X f = A (fold X f) a phi^-1 f = f mu in where mu X.B(X) = Pi X.(B(X) -> X) -> X , fold : Pi X.(B(X) -> X) -> mu X.B(X) -> X fold X f b = b X f in : B(mu X.B(X)) -> mu X.B(X) in b X f = f (B(fold f) b) To see that phi^-1 o phi = id we only need the functor laws for A and that fold (mu X.B(X)) in = id which is indeed a part of Wadler's proof that mu X.B(X) is initial. To show that phi o phi^-1 = id we need to employ parametricity: given g : Pi X.(B(X) -> X) -> A(X) then for any B-algebra f: A(C) -> C we have that f is related to in in the relational interpretation of A(X) -> X applied to the graph of fold f, which I denote as (fold f)^#. Hence, by parametricity of g we have that g X f and g (mu X. B(X)) in are related in the raelational interpretation of B(X) applied to (fold f)^#, which can be spells out as B (fold X f)(g (mu X.B(X) in) = g X f. This implies the desired result using eta phi (phi^- g) = \ X f.B(fold f) (g mu X.B(X) in) = \ X f .g X f = g Background can be found in Wadler's seminal paper "Theorem's for free" and his note "Recursive types for free!" available from http:// homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt (was this ever published?). I also summarized this in a recent post on our fp-lunch blog (http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=83). Disclaimer: For those who know me better, I'd like to point out that I consider System F only as a formal game inspired by Type:Type, whose consistency (i.e. Pi X.X is empty) is irrelevant for the discussion above. :-) Cheers, Thorsten P.S. Why are you actually interested in those isos? 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 txa at Cs.Nott.AC.UK Mon Jan 28 08:50:05 2008 From: txa at Cs.Nott.AC.UK (Thorsten Altenkirch) Date: Mon, 28 Jan 2008 13:50:05 +0000 Subject: [TYPES] polymorphic isomorphisms In-Reply-To: References: <7CBA63BD-79A5-4AF1-9092-AC2B4FDD365A@cs.nott.ac.uk> Message-ID: On 28 Jan 2008, at 13:23, Paul B Levy wrote: > PS System F is consistent :-) I am relieved to hear that. :-) Why? Cheers, Thorsten 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 wadler at inf.ed.ac.uk Mon Jan 28 17:36:38 2008 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Mon, 28 Jan 2008 22:36:38 +0000 Subject: [TYPES] Fwd: polymorphic isomorphisms In-Reply-To: References: <7CBA63BD-79A5-4AF1-9092-AC2B4FDD365A@cs.nott.ac.uk> Message-ID: On 28 Jan 2008, at 11:49, Thorsten Altenkirch wrote: > Background can be found in Wadler's seminal paper "Theorem's for > free" and his note "Recursive types for free!" available from http:// > homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt > (was this ever published?). Thanks for the kind words. I hasten to point out that "Theorems for Free" is strongly influenced by Reynolds' seminal paper, "Types, Abstraction, and Parametric Polymorphism". "Recursive types for free" is indeed unpublished. Another related paper is "The Girard-Reynolds Isomorphism"; the second edition is in the Reynolds festschrift: http://dx.doi.org/10.1016/j.tcs.2006.12.042 There I wrote: The basic structure of the proofs in Section 5 was suggested, independently, by Wadler [46] and Hasegawa [16]. Wadler?s proof was not published, but it circulated informally, and influenced the work of Abadi, Cardelli, and Curien [1] and the subsequent work of Plotkin and Abadi [33]. (Reference 46 is "Recursive types for free".) Cheers, -- P From rwh at cs.cmu.edu Mon Feb 18 12:19:42 2008 From: rwh at cs.cmu.edu (Robert Harper) Date: Mon, 18 Feb 2008 12:19:42 -0500 Subject: [TYPES] focusing on binding and computation Message-ID: We are pleased to accounce a technical report on a new approach to integrating higher-order abstract syntax with a functional programming language: Focusing on Binding and Computation Daniel R. Licata, Noam Zeilberger, Robert Harper PDF and companion code: http://www.cs.cmu.edu/~drl/pubs.html Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing and computing with binding. This language is extracted as the Curry- Howard interpretation of a focused sequent calculus with {\em two} kinds of implication, of opposite polarity. The \emph{representational arrow} extends systems of definitional reflection with the notion of a scoped inference rule, which permits the adequate representation of binding via higher-order abstract syntax. On the other hand, the usual \emph{computational arrow} classifies recursive functions over such higher-order data. Unlike many previous approaches, both binding and computation can mix freely. Following Zeilberger [POPL 2008], the computational function space admits a form of open-endedness, in that it is represented by an abstract map from patterns to expressions. As we demonstrate with Coq and Agda implementations, this has the important practical benefit that we can reuse the pattern coverage checking of these tools. Comments welcome! Dan, Noam, and Bob From cardone at disco.unimib.it Tue Feb 19 07:18:20 2008 From: cardone at disco.unimib.it (Felice Cardone) Date: Tue, 19 Feb 2008 13:18:20 +0100 Subject: [TYPES] Paper announcement Message-ID: Dear colleagues, we are pleased to announce that our paper "History of Lambda-Calculus and Combinatory logic" is available at the address http://www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf The paper is scheduled to appear as a chapter in Volume 5 of the Handbook of the History of Logic, edited by Dov M. Gabbay and John Woods and published by Elsevier (http://www.johnwoods.ca/HHL/). Of course, we welcome any comment, suggestion and additional information on the topics of the paper, namely the development of lambda-calculi and combinatory logic from the prehistory (Frege, Peano and Russell) to the end of 20th century. Regards, J. R. Hindley and F. Cardone From daniel.yokomizo at gmail.com Sat Feb 23 00:02:57 2008 From: daniel.yokomizo at gmail.com (Daniel Yokomizo) Date: Sat, 23 Feb 2008 05:02:57 +0000 Subject: [TYPES] Object-oriented calculi Message-ID: Hi, I'm currently defining a minimalist object-oriented calculus and wanted to know if there were other research on this area, besides Cardelli's and Nordhagen's work. I know some work on formalizations of object systems but found few pointers in calculi. In particular I was looking for work calculi that aren't extensions to other calculi (e.g. lambda, pi) to express OO constructs, but calculi that are fundamentally distinct and foundational (in the sense that the calculus defines only the strictly necessary and things like effects, type systems are defined as extensions). Any information will be much appreciated. Best regards, Daniel Yokomizo. From daniel.yokomizo at gmail.com Sun Feb 24 20:55:54 2008 From: daniel.yokomizo at gmail.com (Daniel Yokomizo) Date: Mon, 25 Feb 2008 01:55:54 +0000 Subject: [TYPES] Object-oriented calculi In-Reply-To: <4683d9370802241654o32ceec39p1cc007f55d2fbe@mail.gmail.com> References: <4683d9370802241654o32ceec39p1cc007f55d2fbe@mail.gmail.com> Message-ID: On Mon, Feb 25, 2008 at 12:54 AM, Tim Chevalier wrote: > On 2/22/08, Daniel Yokomizo wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > > Hi, > > > > I'm currently defining a minimalist object-oriented calculus and > > wanted to know if there were other research on this area, besides > > Cardelli's and Nordhagen's work. I know some work on formalizations of > > object systems but found few pointers in calculi. In particular I was > > looking for work calculi that aren't extensions to other calculi (e.g. > > lambda, pi) to express OO constructs, but calculi that are > > fundamentally distinct and foundational (in the sense that the > > calculus defines only the strictly necessary and things like effects, > > type systems are defined as extensions). > > It's so obvious that I hesitated to reply on-list, but I assume you've > looked at Featherweight Java, as detailed in ch. 19 of Pierce's _Types > and Programming Languages_ (and elsewhere). That chapter contains > citations to related work, too. But perhaps I'm misunderstanding your > question... Hi, Yes, I'm familiar with FWJ, but I don't consider it foundational (as it includes a type system, so it isn't the smallest set of building blocks that allows us to build other abstractions upon it, as we can remove the type system and still have a complete calculus). It just didn't occur to me to consider it, thanks for the reminder. Anyway I'm looking for something even more lightweight, probably with a single expression language (FWJ separates the class language and the expression language, we can't mix them arbitrarily). My research resulted in a quite interesting and minimalistic calculus, but it seems so obvious that I'm surprised to be unable to find anything similar in the literature. > Cheers, > Tim > > -- > Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt > "What is this jest in majesty? This ass in passion? How do God and > Devil combine to form a live dog?" -- Vladimir Nabokov Best regards, Daniel Yokomizo. From David.Teller at ens-lyon.org Mon Feb 25 07:39:24 2008 From: David.Teller at ens-lyon.org (David Teller) Date: Mon, 25 Feb 2008 13:39:24 +0100 Subject: [TYPES] Object-oriented calculi In-Reply-To: References: <4683d9370802241654o32ceec39p1cc007f55d2fbe@mail.gmail.com> Message-ID: <1203943164.8769.6.camel@Blefuscu> Have you looked at Abadi & Cardelli's _A calculus of objects_ ? On Mon, 2008-02-25 at 01:55 +0000, Daniel Yokomizo wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] -- David Teller Security of Distributed Systems http://www.univ-orleans.fr/lifo/Members/David.Teller Angry researcher: French Universities need reforms, but the LRU act brings liquidations. From cce at ccs.neu.edu Mon Feb 25 11:44:00 2008 From: cce at ccs.neu.edu (Carl Eastlund) Date: Mon, 25 Feb 2008 11:44:00 -0500 Subject: [TYPES] Object-oriented calculi In-Reply-To: References: Message-ID: <990e0c030802250844x30d00d45p1af4de6bc39df9fc@mail.gmail.com> Daniel, Matthias Felleisen and I published a technical report in 2006 related to this. I'll paste a link to it below this paragraph. Our OO semantics called "sequence traces" formalizes the behavior of objects with fields and methods, and is parameterized over the computation that occurs inside single objects between messages. The tech report shows representations of Abadi and Cardelli's calculus, ClassicJava, and a multiple dispatch language in our system. This may not fit your criteria of minimality, but perhaps it is of interest. We also cite other semantics and calculi, in case that helps broaden your search. Good luck! You can find the tech report at: http://www.ccs.neu.edu/home/cce/publications.html -- Carl Eastlund On Sat, Feb 23, 2008 at 12:02 AM, Daniel Yokomizo wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi, > > I'm currently defining a minimalist object-oriented calculus and > wanted to know if there were other research on this area, besides > Cardelli's and Nordhagen's work. I know some work on formalizations of > object systems but found few pointers in calculi. In particular I was > looking for work calculi that aren't extensions to other calculi (e.g. > lambda, pi) to express OO constructs, but calculi that are > fundamentally distinct and foundational (in the sense that the > calculus defines only the strictly necessary and things like effects, > type systems are defined as extensions). > Any information will be much appreciated. > > Best regards, > Daniel Yokomizo. From streicher at mathematik.tu-darmstadt.de Thu Mar 13 12:55:14 2008 From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher) Date: Thu, 13 Mar 2008 17:55:14 +0100 (CET) Subject: [TYPES] my habilitation thesis available on the net Message-ID: <200803131655.m2DGtE3L009855@fb04209.mathematik.tu-darmstadt.de> Now and then I receive a request for my Habilitation Thesis from 1993 on Semantics of Intensional Type Theory which was never published and is not available in one of the usual electronic formats. But if you really want to look at it you can find a scanned version at www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf BUT it's awfully big (4915468 KB). Thomas Streicher From dlsmith at rice.edu Wed Apr 9 11:15:31 2008 From: dlsmith at rice.edu (Dan Smith) Date: Wed, 9 Apr 2008 10:15:31 -0500 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? Message-ID: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> Benjamin Pierce's PhD work involved a calculus combining System F, intersection types, and bounded quantification (Programming With Intersection Types and Bounded Polymorphism, 1991). His earlier work aspired to including union types in this calculus as well, but that was apparently dropped (Programming with Intersection Types, Union Types, and Polymorphism, 1991). What is the best place to find a similar calculus that includes union types? In particular, I'm looking for a similar formal treatment of subtyping that includes the following rules ("&" is intersection; "|" is union): S->T1 & S->T2 <: S->(T1 & T2) S1->T & S2->T <: (S1 | S2)->T Any help would be appreciated. --Dan From bcpierce at cis.upenn.edu Wed Apr 9 13:40:41 2008 From: bcpierce at cis.upenn.edu (Benjamin Pierce) Date: Wed, 9 Apr 2008 13:40:41 -0400 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> References: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> Message-ID: <42B14531-AFE9-4F73-A967-C9CBC2FC1EBB@cis.upenn.edu> There's been a huge amount of work in this area since the papers you mentioned. Joshua Dunfield's recent (CMU) PhD thesis has a pretty comprehensive bibliography. Also check out the CDuce web page. Best, - Benjamin On Apr 9, 2008, at 11:15 AM, Dan Smith wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > Benjamin Pierce's PhD work involved a calculus combining System F, > intersection types, and bounded quantification (Programming With > Intersection Types and Bounded Polymorphism, 1991). His earlier work > aspired to including union types in this calculus as well, but that > was apparently dropped (Programming with Intersection Types, Union > Types, and Polymorphism, 1991). > > What is the best place to find a similar calculus that includes union > types? In particular, I'm looking for a similar formal treatment of > subtyping that includes the following rules ("&" is intersection; "|" > is union): > > S->T1 & S->T2 <: S->(T1 & T2) > > S1->T & S2->T <: (S1 | S2)->T > > Any help would be appreciated. > > --Dan From gc at pps.jussieu.fr Wed Apr 9 14:58:53 2008 From: gc at pps.jussieu.fr (NOREPLY) Date: Wed, 09 Apr 2008 20:58:53 +0200 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? Message-ID: <47FD11ED.7060608@pps.jussieu.fr> Benjamin Pierce wrote: > > Also check out the CDuce web page. > If you do not want to check all the papers in the CDuce page my advice is that your best bet is the following paper that will appear in The Journal of the ACM: Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types. it can be found in my home page or directly by following this link http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf Section 2 gives an relatively simple introduction of the subject, in Sections 3-4 you have an overview of the main results. Then you can skip Section 6 and jump directly to Section 7 which is a commentary on the more technical results among which you will also find a discussion about the relation with Benjamin's PhD and its follows up. Please do not hesitate to contact me if you have any question or remark. ---Beppe--- (Giuseppe Castagna) From noam+types at cs.cmu.edu Thu Apr 10 12:04:47 2008 From: noam+types at cs.cmu.edu (Noam Zeilberger) Date: Thu, 10 Apr 2008 12:04:47 -0400 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> Message-ID: <20080410160447.GA16573@cs.cmu.edu> You should also be aware that in the presence of effects, this rule: (1) S->T1 & S->T2 <: S->(T1 & T2) is unsound for call-by-value functions, while this rule: (2) S1->T & S2->T <: (S1 | S2)->T is unsound for call-by-name functions. To understand why (1) fails for CBV, you can read the paper "Intersection types and computational effects" by Davies and Pfenning in ICFP 00. (2) is unsound under CBN "by reason of duality"--although the subtyping principle is not mentioned explicitly there, the paper "Tridirectional typechecking" by Dunfield and Pfenning in POPL 04 should give you an intuition for why not to expect (2) in CBN with effects. On the other hand, (1) is valid under CBN, and (2) under CBV. How to derive these valid laws while avoiding the unsound ones is sketched very briefly in Section 4 of my paper "On the unity of duality" in the current issue of APAL -- but I'm hoping to write something more complete about this soon. (If you are *very* curious, you can download my thesis proposal.) Noam From dlsmith at rice.edu Thu Apr 10 17:28:07 2008 From: dlsmith at rice.edu (Dan Smith) Date: Thu, 10 Apr 2008 16:28:07 -0500 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> References: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> Message-ID: Thank you all for your useful pointers. In skimming a number of papers related to these references, I have yet to come upon the ideal presentation I'm looking for. I would love to see a paper that: - Extends lambda-sub (the simply-typed lambda-calculus with subtyping) with intersection and union types. - Defines typing and subtyping in this calculus using simple operational semantics, in the style used by Pierce. - Develops a subtyping algorithm in two stages: first, by defining subtyping "declaratively" -- explicitly including rules like transitivity -- and then redefining it using syntax-directed rules (and proving that the two definitions are equivalent). - Includes in its declarative subtyping definition the two rules I mentioned below for distribution over arrow types. Of course, this is just the lazy route -- given the papers that I *have* seen, I ought to be able with some effort to extract the concepts that would be presented in my ideal paper. And I can accept that. (My apologies if any of the references I've been pointed to meet these criteria, and I just wasn't perceptive enough to catch it.) But I thought I'd be more explicit about what I'm looking for, just in case anyone is aware of something that meets or is close to these criteria. --Dan On Apr 9, 2008, at 10:15 AM, Dan Smith wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Benjamin Pierce's PhD work involved a calculus combining System F, > intersection types, and bounded quantification (Programming With > Intersection Types and Bounded Polymorphism, 1991). His earlier work > aspired to including union types in this calculus as well, but that > was apparently dropped (Programming with Intersection Types, Union > Types, and Polymorphism, 1991). > > What is the best place to find a similar calculus that includes union > types? In particular, I'm looking for a similar formal treatment of > subtyping that includes the following rules ("&" is intersection; "|" > is union): > > S->T1 & S->T2 <: S->(T1 & T2) > > S1->T & S2->T <: (S1 | S2)->T > > Any help would be appreciated. > > --Dan From P.B.Levy at cs.bham.ac.uk Thu Apr 10 18:12:14 2008 From: P.B.Levy at cs.bham.ac.uk (Paul B Levy) Date: Thu, 10 Apr 2008 23:12:14 +0100 (BST) Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <20080410160447.GA16573@cs.cmu.edu> References: <20080410160447.GA16573@cs.cmu.edu> Message-ID: On Thu, 10 Apr 2008, Noam Zeilberger wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > You should also be aware that in the presence of effects, this rule: > > (1) S->T1 & S->T2 <: S->(T1 & T2) > > is unsound for call-by-value functions, while this rule: > > (2) S1->T & S2->T <: (S1 | S2)->T > > is unsound for call-by-name functions. To understand why (1) fails > for CBV, you can read the paper "Intersection types and computational > effects" by Davies and Pfenning in ICFP 00. (2) is unsound under CBN > "by reason of duality"--although the subtyping principle is not > mentioned explicitly there, the paper "Tridirectional typechecking" by > Dunfield and Pfenning in POPL 04 should give you an intuition for why > not to expect (2) in CBN with effects. > > On the other hand, (1) is valid under CBN, and (2) under CBV. Very interesting. And in call-by-push-value, both are valid. What's not valid, if I understand you correctly, is (3) F T1 & F T2 <: F (T1 & T2) which is why (1) fails in CBV (4) U (S1 | S2) <: U S1 | U S2 which is why (2) fails in CBN. I was aware of (3), but (4) is new to me. Paul -- Paul Blain Levy email: pbl at cs.bham.ac.uk School of Computer Science, University of Birmingham Birmingham B15 2TT, U.K. tel: +44 121-414-4792 http://www.cs.bham.ac.uk/~pbl From gc at pps.jussieu.fr Thu Apr 10 20:30:45 2008 From: gc at pps.jussieu.fr (gc@pps.jussieu.fr) Date: Fri, 11 Apr 2008 02:30:45 +0200 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <20080410160447.GA16573@cs.cmu.edu> References: <20080410160447.GA16573@cs.cmu.edu> Message-ID: <47FEB135.5070108@pps.jussieu.fr> Noam Zeilberger wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > You should also be aware that in the presence of effects, this rule: > > (1) S->T1 & S->T2 <: S->(T1 & T2) > > is unsound for call-by-value functions, while this rule: > > (2) S1->T & S2->T <: (S1 | S2)->T > > is unsound for call-by-name functions. Please note that all of this is true only for Curry-style terms. In the JACM paper on Semantic Subtyping I cited in my previous post, http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf which uses call by value Church-style notation (1) [and of course (2)] is sound. This and the difference with Davies and Pfenning 2000 paper are thouroughly explained in Appendix A2 (cf. the "related work" subsection) ... if you survive to read till page 65 :-) ---Beppe--- From gc at pps.jussieu.fr Thu Apr 10 20:53:17 2008 From: gc at pps.jussieu.fr (gc@pps.jussieu.fr) Date: Fri, 11 Apr 2008 02:53:17 +0200 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: References: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> Message-ID: <47FEB67D.1000307@pps.jussieu.fr> Dan Smith wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Thank you all for your useful pointers. > > In skimming a number of papers related to these references, I have yet > to come upon the ideal presentation I'm looking for. I would love to > see a paper that: > You can probably find a good match (the calculus aside) in a paper by Mariangiola Dezani et al "The relevance of semantic subtyping". http://www.di.unito.it/~dezani/papers/itrs02.pdf Look in particular in Section 3. The paper is more logic-oriented than functional programming oriented howver it will also give you an idea on the relation about what you are looking for and a streamlined version of semantic subtyping without negation types. > - Extends lambda-sub (the simply-typed lambda-calculus with subtyping) > with intersection and union types. Church style or Curry style? It is quite likely to make a difference. ---Beppe--- From rowan at csse.uwa.edu.au Fri Apr 11 03:43:08 2008 From: rowan at csse.uwa.edu.au (Rowan Davies) Date: Fri, 11 Apr 2008 15:43:08 +0800 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: References: <20080410160447.GA16573@cs.cmu.edu> Message-ID: On Fri, Apr 11, 2008 at 6:12 AM, Paul B Levy wrote: > > What's not valid, if I understand you correctly, is > > (3) F T1 & F T2 <: F (T1 & T2) which is why (1) fails in CBV > > (4) U (S1 | S2) <: U S1 | U S2 which is why (2) fails in CBN. > > I was aware of (3), but (4) is new to me. > Just a small note that the zero-ary case of the failure of (4) makes particular sense. U bot <: bot does not hold. Intuitively, this is because it's possible to have a thunk that contains a computation that never yields a value. From dlsmith at rice.edu Fri Apr 11 10:09:49 2008 From: dlsmith at rice.edu (Dan Smith) Date: Fri, 11 Apr 2008 09:09:49 -0500 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <47FEB67D.1000307@pps.jussieu.fr> References: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> <47FEB67D.1000307@pps.jussieu.fr> Message-ID: <90AF2AA2-90FC-49EB-9C77-1321F7F74D2C@rice.edu> On Apr 10, 2008, at 7:53 PM, gc at pps.jussieu.fr wrote: > Dan Smith wrote: >> - Extends lambda-sub (the simply-typed lambda-calculus with >> subtyping) >> with intersection and union types. > > Church style or Curry style? It is quite likely to make a difference. Curry-style, but with explicit type annotations. --Dan From dezani at di.unito.it Fri Apr 11 12:47:06 2008 From: dezani at di.unito.it (Mariangiola Dezani) Date: Fri, 11 Apr 2008 18:47:06 +0200 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <90AF2AA2-90FC-49EB-9C77-1321F7F74D2C@rice.edu> References: <82C45207-47D2-42EF-8148-02C7E725F6C0@rice.edu> <47FEB67D.1000307@pps.jussieu.fr> <90AF2AA2-90FC-49EB-9C77-1321F7F74D2C@rice.edu> Message-ID: <1981DB99-7232-4BA9-AE3C-5F54487CD66A@di.unito.it> About losing subject reduction in presence of intersection/union/arrow I suggest also to look at: M. Dezani-Ciancaglini and S. Ronchi Della Rocca. Intersection and Reference Types, http://www.di.unito.it/~dezani/papers/dr.pdf which discusses (1) S->T1 & S->T2 <: S->(T1 & T2) S. van Bakel. Subject Reduction vs Intersection / Union Types for lambda-bar-mu-mu-tilde http://www.doc.ic.ac.uk/~svb/ which shows that subject reduction does not hold without assuming subtyping involving arrows. Best, Mariangiola @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Mariangiola Dezani-Ciancaglini Dipartimento di Informatica Universita' di Torino c.Svizzera 185, 10149 Torino (Italy) e-mail : dezani at di.unito.it phone: 39-011-6706732 fax : 39-011-751603 mobile: 39-320-4359903 (preferred) 39-348-2251592 http://www.di.unito.it/~dezani ********************************************************************** Unless unavoidable, no Word, Excel or PowerPoint attachments, please. See http://www.gnu.org/philosophy/no-word-attachments.html ********************************************************************** "L'ITALIA RIPUDIA LA GUERRA come strumento di offesa alla libert? degli altri popoli e come mezzo di risoluzione delle controversie internazionali." (Art. 11 della Costituzione della Repubblica Italiana) From wadler at inf.ed.ac.uk Tue Apr 15 08:07:06 2008 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Tue, 15 Apr 2008 13:07:06 +0100 Subject: [TYPES] Equational correspondence and equational embedding Message-ID: <48049A6A.8050603@inf.ed.ac.uk> The notion of *equational correspondence* was defined by Sabry and Felleisen in their paper: Amr Sabry and Matthias Felleisen Reasoning about programs in continuation-passing style LISP and Symbolic Computation, 6(3--4):289--360, November 1993. We lay out below the definition, along with a related notion of *equational embedding*. We've seen relatively little about equational correspondence in the literature, and nothing about equational embedding. Given that these seem to be fundamental concepts, we suspect we've been looking in the wrong places. Any pointers to relevant literature would be greatly apprectiated. An *equational theory* T is a set of terms t of T, and a set of equations t =_T t' (where t, t' are terms of T). Let S, T be equational theories. We say that f : S -> T and g : T -> S constitute an *equational correspondence* between S and T if 1. g(f(s)) =_S s, for all terms s in S 2. f(g(t)) =_T t, for all terms t in T 3. s =_S s' implies f(s) =_T f(s'), for all terms s, s' in S 4. t =_T t' implies g(t) =_S g(t'), for all terms t, t' in T Let S, T be equational theories. We say that f : S -> T and g : f(S) -> S (where f(S) is the image of S under f, a subset of T) constitute an *equational embedding* between S and T if 1. g(f(s)) =_S s, for all s in S 2. s =_S s' implies f(s) =_T f(s'), for all s, s' in S It is easy to see that there is an equational embedding of S into T if and only if there is a function from S to T that preserves and reflects equations. Clearly, f and g constitute an equational correspondence between S and T if f and g constitute an equational embedding of S into T and g and f constitute an equational embedding of T into S. We conjecture that whenever there is an equational embedding of S into T and of T into S that there is an equational correspondence between S and T. This is not immediate, because one equational embedding might be given by f and g and the other by h and k, with no obvious relation between the two. As I said, any pointers to relevant literature would be greatly appreciated! Yours, -- Sam Lindley, Philip Wadler, Jeremy Yallop -- \ Philip Wadler, Professor of Theoretical Computer Science /\ School of Informatics, University of Edinburgh / \ http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. From matthias at ccs.neu.edu Tue Apr 15 10:06:57 2008 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Tue, 15 Apr 2008 10:06:57 -0400 Subject: [TYPES] Equational correspondence and equational embedding In-Reply-To: <48049A6A.8050603@inf.ed.ac.uk> References: <48049A6A.8050603@inf.ed.ac.uk> Message-ID: Phil, Amr responded with the bare facts. Here is my path of discovery, with two additional lit ptrs: John Gately was an MS student at IU working in Indiana. I suggested to him that he work out a cbv theory of combinators in the spirit of Gordon Plotkin's CBN/CBV paper in TCS(1974). I also suggested that he read Barendregt (chapter 7, with an overview in chapter 2) because it summarizes the equational correspondence I was after. John dropped out from IU but rejoined me at Rice and published a paper on his CBV CL ~ lambda_v correspondence paper at some workshop (mathematical foundations of programming languages?). Around the same time, I started Eric Crank on a correspondence between cps(\lambda_v) and lambda with the hope that a reduction rule Bruce Duba and I had played with since 1985: (\x.E[x]) M = E[M] for x not in fv(E) [beta_Omega]. While Eric preferred to switch to equational characterizations of imperative parameter passing, Amr came along and solved this puzzle. As Amr said, we tried to stay as close as possible to the source (Curry) with our write-up for LFP 1992. -- Matthias On Apr 15, 2008, at 8:07 AM, Philip Wadler wrote: > The notion of *equational correspondence* was defined by Sabry and > Felleisen in their paper: > > Amr Sabry and Matthias Felleisen > Reasoning about programs in continuation-passing style > LISP and Symbolic Computation, 6(3--4):289--360, November 1993. > > We lay out below the definition, along with a related notion of > *equational embedding*. We've seen relatively little about equational > correspondence in the literature, and nothing about equational > embedding. Given that these seem to be fundamental concepts, we > suspect we've been looking in the wrong places. Any pointers to > relevant literature would be greatly apprectiated. > > An *equational theory* T is a set of terms t of T, and a set of > equations > t =_T t' (where t, t' are terms of T). > > Let S, T be equational theories. We say that f : S -> T and g : T - > > S > constitute an *equational correspondence* between S and T if > > 1. g(f(s)) =_S s, for all terms s in S > 2. f(g(t)) =_T t, for all terms t in T > 3. s =_S s' implies f(s) =_T f(s'), for all terms s, s' in S > 4. t =_T t' implies g(t) =_S g(t'), for all terms t, t' in T > > Let S, T be equational theories. We say that f : S -> T and > g : f(S) -> S (where f(S) is the image of S under f, a subset of T) > constitute an *equational embedding* between S and T if > > 1. g(f(s)) =_S s, for all s in S > 2. s =_S s' implies f(s) =_T f(s'), for all s, s' in S > > It is easy to see that there is an equational embedding of S into T if > and only if there is a function from S to T that preserves and > reflects equations. > > Clearly, f and g constitute an equational correspondence between S and > T if f and g constitute an equational embedding of S into T and g and > f constitute an equational embedding of T into S. > > We conjecture that whenever there is an equational embedding of S into > T and of T into S that there is an equational correspondence between S > and T. This is not immediate, because one equational embedding might > be given by f and g and the other by h and k, with no obvious relation > between the two. > > As I said, any pointers to relevant literature would be greatly > appreciated! > > Yours, -- Sam Lindley, Philip Wadler, Jeremy Yallop > > -- > \ Philip Wadler, Professor of Theoretical Computer Science > /\ School of Informatics, University of Edinburgh > / \ http://homepages.inf.ed.ac.uk/wadler/ > > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > From svb at doc.ic.ac.uk Tue Apr 15 11:31:25 2008 From: svb at doc.ic.ac.uk (Steffen van Bakel) Date: Tue, 15 Apr 2008 16:31:25 +0100 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? Message-ID: <405F904B-7D06-446C-8246-EBBAF30BF13C@doc.ic.ac.uk> Hi Dan, This is to inform you that I have just updated my paper, Subject Reduction vs Intersection / Union Types for lambda-bar-mu-mu- tilde available at http://www.doc.ic.ac.uk/~svb/Research. The previous version was not complete. That said, Mariangiola's statement still holds: subject reduction collapses also in a 'simple' system, where the only subtype relation is the one induced by commutativity and associativity of both union and intersection. Also, it is not just union that creates a problem. Best, Steffen van Bakel Imperial College London From Tim.Sweeney at epicgames.com Tue Apr 15 13:59:03 2008 From: Tim.Sweeney at epicgames.com (Tim Sweeney) Date: Tue, 15 Apr 2008 13:59:03 -0400 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: <47FD11ED.7060608@pps.jussieu.fr> References: <47FD11ED.7060608@pps.jussieu.fr> Message-ID: This paper's treatment of subtyping as a subset relation is extremely insightful. In particular, its definition of function arrows T->U as the complemented product ~(T x ~U) precisely captures the nature of contravariance and overloaded functions in the presence of subtyping. In this sort of representation, is it recognized that universal and existential quantifiers coincide precisely with set-indexed intersection and union? In particular, all(x:t) ux coincides with the intersection, for each element x from set t, of the set ux (which may reference x). And similarly for existential quantifiers. If this system is extended with such quantifiers, with a dependent-typed singleton-set constructor, a powerset constructor, and recursive definitions, then we have [my conjecture] the perfect type system for future programming languages, given its combination of power and expressiveness. The singleton-set construct enables us to use the type-quantifiers over values, so that we types dependent on other types and on values. For example, given a type of n-element arrays of elements with type t, we can use its existential quantifiers to express type of all arrays of type t, with n effectively erased (not bundled up into an existential dependent product). Then we can use its universal quantifiers to express functions over arrays of any length, where we reconstruct the length through quantifier instantiation. The resulting code is very concise, and this allows programming practices similar to C++ templates and Java generics, where the programmer writes simple code using libraries with complex types, and the compiler performs a lot of quantifier instantiation to fill in the implicit details during the typechecking phase. Taking this approach does require a temporary suspension of disbelief. As the author points out, cardinality arguments prevent us from interpreting types precisely as sets within ZF. In this case, I think it's fruitful to explore the type theory first, and look to resolve the seeming contradictions later. The author avoids trouble by referring to the subset relation only to establish subtyping, and not as a literal interpretation of types as sets. But other approaches may be interesting, for example choosing a set theory such as NF which treats infinities differently than ZF, perhaps giving types a valid literal interpretation as sets. Tim Sweeney Epic Games -----Original Message----- From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of NOREPLY Sent: Wednesday, April 09, 2008 2:59 PM To: types-list at lists.seas.upenn.edu Subject: Re: [TYPES] Formal treatment of intersection/union/arrow subtyping? [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Benjamin Pierce wrote: > Also check out the CDuce web page. If you do not want to check all the papers in the CDuce page my advice is that your best bet is the following paper that will appear in The Journal of the ACM: Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types. it can be found in my home page or directly by following this link http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf Section 2 gives an relatively simple introduction of the subject, in Sections 3-4 you have an overview of the main results. Then you can skip Section 6 and jump directly to Section 7 which is a commentary on the more technical results among which you will also find a discussion about the relation with Benjamin's PhD and its follows up. Please do not hesitate to contact me if you have any question or remark. ---Beppe--- (Giuseppe Castagna) From gc at pps.jussieu.fr Wed Apr 16 05:41:07 2008 From: gc at pps.jussieu.fr (gc@pps.jussieu.fr) Date: Wed, 16 Apr 2008 11:41:07 +0200 Subject: [TYPES] Formal treatment of intersection/union/arrow subtyping? In-Reply-To: References: <47FD11ED.7060608@pps.jussieu.fr> Message-ID: <4805C9B3.5080906@pps.jussieu.fr> Tim Sweeney wrote: >> >> This paper's treatment of subtyping as a subset relation is extremely >> insightful. In particular, its definition of function arrows T->U as >> the complemented product ~(T x ~U) precisely captures the nature of >> contravariance and overloaded functions in the presence of subtyping. >> Thank you very much, I am very glad you liked it. >> In this sort of representation, is it recognized that universal and >> existential quantifiers coincide precisely with set-indexed >> intersection and union? In particular, all(x:t) ux coincides with the >> intersection, for each element x from set t, of the set ux (which may >> reference x). And similarly for existential quantifiers. >> >> If this system is extended with such quantifiers, with a >> dependent-typed singleton-set constructor, a powerset constructor, and >> recursive definitions, then we have [my conjecture] the perfect type >> system for future programming languages, given its combination of >> power and expressiveness. >> I cannot give a general answer (I would love to) but just a partial one based on some form of poor-man dependent types. First of all, even though the paper omitted them, CDuce has singleton types. So for instance you can specify, that the successor function ?x.x+1 has type (Int ? Int) ? (2 ? 3) where 2 and 3 are the singleton types containing the values 2 and 3 respectively. Now in their seminal paper A Modest Model of Records, Inheritance and Bounded Quantification. Inf. Comput. 87(1/2):196-239 (1990) Bruce and Longo showed that record types can be interpreted as an indexed product that is as a first order quantification on finite sets of labels. Roughly the record type { a: Int, b: Bool} is the universal quantification ?x:{a,b}.F(x) where F is the mapping { a ? Int, b ? Bool}. Interestingly in CDuce record types are obtained by an intersection. Morally they are an intersection of maps from singleton types to types or, if you prefer, they are overloaded functions whose domains are singleton types of labels. That is { a:Int, b:Bool } corresponds in CDuce to the overloaded function type ( a?Int ) ? (b?Bool) where again here a and b denote the two singleton types containing the respective labels. So in this simple perspective you can see a correspondence between ?x:{a,b}.F(x) and (a?F(a)) ? (b?F(b)) which, if I understood correctly, is what you were asking for. Of course this is a very reductive example and whether this can be extended to general case you point out in your post (and that if remember correctly you also evoked in your POPL talk) I cannot say. But I would be delighted to see more examples of its use to exactly understand what you are looking for. Do you have any pointer to pseudocode you would like to type with such a technique? [Advertisement]In the meanwhile if you want to try to play with the CDuce singleton recursive intersection and union types and you do not want to install it, you can use our online interpreter at http://cduce.org/cgi-bin/cduce [/Advertisement] That said the combination of singleton types and semantic subtyping is a funny beast since stunningly related problems about singleton types naturally pop out from applying semantic subtyping to settings so different as parametric polymorphism (Hosoya et al. POPL'05) and pi-calculus (Castagna et al. LICS '05) For those interested in this and similar problems they can find in LNCS n.3701 a non-technical (well, let me say as less technical as possible) survey titled Semantic subtyping: challenges, perspectives, and open problems. which I gave as invited talk at ICTCS '05 http://www.pps.jussieu.fr/~gc/papers/ictcs05a.pdf There you will see that among the perspectives for semantic subtyping I consider the application to dependent types quite an interesting topic for future investigation. I think it would be a very nice topic for a PhD dissertation (I would love to supervise). >> >> Taking this approach does require a temporary suspension of >> disbelief. As the author points out, cardinality arguments prevent us >> from interpreting types precisely as sets within ZF. In this case, I >> think it's fruitful to explore the type theory first, and look to >> resolve the seeming contradictions later. The author avoids trouble >> by referring to the subset relation only to establish subtyping, and >> not as a literal interpretation of types as sets. But other >> approaches may be interesting, for example choosing a set theory such >> as NF which treats infinities differently than ZF, perhaps giving >> types a valid literal interpretation as sets. >> Personally, I do not consider it a contradiction nor does it makes me feel uneasy. More precisely I do not care whether I cannot precisely associate each type to a set that represents all its programs. All I really care is that I can reason on types as if they were sets, and use this reasoning to deduce their inclusion. In fact all that matters for me is that my programs do not go wrong, and for that what I need to know is whether I can use an expression of some type where one of a different type is expected. Once I can establish it I am happy even if I cannot say what the two types at issues exactly denoted but just how they were related. Actually this is the essence of our approach. ---Beppe--- >> Benjamin Pierce wrote: >>> Also check out the CDuce web page. >> >> If you do not want to check all the papers in the CDuce page my advice >> is that your best bet is the following paper that will appear in >> The Journal of the ACM: >> >> Semantic Subtyping: dealing set-theoretically with function, union, >> intersection, and negation types. >> >> it can be found in my home page or directly by following this link >> http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf >> From jeremy.siek at gmail.com Mon Apr 21 17:59:42 2008 From: jeremy.siek at gmail.com (Jeremy Siek) Date: Mon, 21 Apr 2008 15:59:42 -0600 Subject: [TYPES] analogy between Felleisen's syntactic theories of state and Hindley-Milner constraints Message-ID: Dear Types Readers, I was recently reading Felleisen and Hieb's "The revised report on syntactic theories of sequential control and state" and also Francois Pottier and Didier Remy's "The Essence of ML Type Inference" and was struck by the similarity between the \rho binder in the \Lambda_ \sigma calculus and and the \exists binder in the language of constraints. They both provide a local way to generate fresh variables. Also, the semantics of how these binders "bubble up" through the program is quite similar. I'm curious if they have a shared ancestry or whether there were two independent branches of discovery. It seems like this technique deserves the status of a "design pattern" for dealing with the generation of fresh variables. I'm also curious about other applications of this technique. Cheers, Jeremy From Francois.Pottier at inria.fr Wed Apr 23 08:12:23 2008 From: Francois.Pottier at inria.fr (Francois Pottier) Date: Wed, 23 Apr 2008 14:12:23 +0200 Subject: [TYPES] analogy between Felleisen's syntactic theories of state and Hindley-Milner constraints In-Reply-To: References: Message-ID: <20080423121223.GB27654@yquem.inria.fr> Hi, On Mon, Apr 21, 2008 at 03:59:42PM -0600, Jeremy Siek wrote: > I was recently reading Felleisen and Hieb's "The revised report on syntactic > theories of sequential control and state" and also Francois Pottier and > Didier Remy's "The Essence of ML Type Inference" and was struck by the > similarity between the \rho binder in the \Lambda_ \sigma calculus and and > the \exists binder in the language of constraints. They both provide a local > way to generate fresh variables. That's also the way \nu binders float up in the pi-calculus. It is, by now, a standard way to provide local rewriting rules that explain global generation of fresh names. Didier and I did not invent anything here. I don't know who is the earliest inventor of this idea. Best regards, -- Fran?ois Pottier Francois.Pottier at inria.fr http://cristal.inria.fr/~fpottier/ From matthias at ccs.neu.edu Wed Apr 23 20:58:09 2008 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Wed, 23 Apr 2008 20:58:09 -0400 Subject: [TYPES] analogy between Felleisen's syntactic theories of state and Hindley-Milner constraints In-Reply-To: <20080423121223.GB27654@yquem.inria.fr> References: <20080423121223.GB27654@yquem.inria.fr> Message-ID: On Apr 23, 2008, at 8:12 AM, Francois Pottier wrote: > I don't know who is the earliest inventor of this idea. Bob and I agreed to have co-discovered the concept in the week between Christmas and New Year 1987. (It was buried in my dissertation but it wasn't good enough.) I am also confident that Ian Mason and Carolyn Talcott had figured out a similar idea by 1988, if not earlier. -- I don't know when Milner did his scope stuff. -- Matthias From Gerard.Boudol at sophia.inria.fr Thu Apr 24 04:14:49 2008 From: Gerard.Boudol at sophia.inria.fr (Gerard Boudol) Date: Thu, 24 Apr 2008 10:14:49 +0200 Subject: [TYPES] analogy between Felleisen's syntactic theories of state and Hindley-Milner constraints In-Reply-To: <20080423121223.GB27654@yquem.inria.fr> References: <20080423121223.GB27654@yquem.inria.fr> Message-ID: <48104179.1020706@sophia.inria.fr> Francois Pottier wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > Hi, > > > > That's also the way \nu binders float up in the pi-calculus. It is, by now, a > standard way to provide local rewriting rules that explain global generation > of fresh names. Didier and I did not invent anything here. I don't know who > is the earliest inventor of this idea. Hello, as far as the pi-calculus is concerned, I think the idea of moving binders and having only "local" reductions comes from the paper on the Chemical Abstract Machine I wrote with G?rard Berry, where reduction is "reaction" of "molecules in contact". Then Milner popularized the idea under the name of "structural equivalence" (or, for some people, congruence). Cheers, G?rard From claus.reinke at talk21.com Thu Apr 24 11:07:54 2008 From: claus.reinke at talk21.com (Claus Reinke) Date: Thu, 24 Apr 2008 16:07:54 +0100 Subject: [TYPES] analogy between Felleisen's syntactic theories of state andHindley-Milner constraints References: Message-ID: <016701c8a61c$faa82dc0$cd058351@cr3lt> > both provide a local way to generate fresh variables. Also, the > semantics > of how these binders "bubble up" through the program is quite similar. > I'm curious if they have a shared ancestry or whether there were two > independent branches of discovery. It seems like this technique deserves > the status of a "design pattern" for dealing with the generation of > fresh variables. > I'm also curious about other applications of this technique. it has been a very long time, and i don't have the papers at hand to check my memories, but such things were popular at a time in the functional logic programming field, with the subset of fp-background proponents who were fond of lambda-calculus, explicit scopes, and reduction semantics (as opposed to the lp-background proponents, who were more used to dropping their quantifiers). as i said, i'm not sure about the precise references, but i think the following two touched on this subject: @inproceedings{Berkling86b, author = {Klaus Berkling}, title = {{Epsilon reduction -- another view of unification}}, booktitle = {{Fifth Generation Computer Architectures}}, year = 1986, editor = {J. V. Wood}, pages = {163-176}, organization = {IFIP}, publisher = {Elsevier Science Publishers B.V. (North-Holland)}, topics = {FP - Lambda Calculi,LP - Unification} } @inproceedings{Reddy86b, author = {Uday S.~Reddy}, title = {{Functional Logic Languages: Part I}}, booktitle = {{Graph Reduction, Santa F{\'e}, New Mexico, USA (LNCS 279)}}, year = 1986, editor = {J.~H.~Fasel and R.~M.~Keller}, publisher = {Springer-Verlag}, topics = {FP - General,LP - General} } dropping choice moves from logic to single-assignment variables, which suggested the use of similar quantifiers for handling state. once you let binders "bubble up", you also get another version of the name capture problem, to which Berkling applied the same elegant (and underappreciated) solution as he used for lambda-calculus (see any of the references below). hth, claus @techreport{Berkling76, author = {Berkling, K.J.}, title = {{A Symmetric Complement to the Lambda Calculus}}, institution = GMD, note = {ISF-76-7}, month = {September}, year = 1976, abstract = {"The calculi of Lambda-conversion" introduced by A.Church are complemented by a new operator lambda-bar, which is in some sense the inverse to the lambda-operator. The main advantage of the complemented system is that variables do not have to be renamed. Conversely, any renaming of variables in a formula is possible. Variables may, however, appear with varied numbers of lambda-bars in front of them. Implementations of the lambda calculus representation with the symmetric complement are greatly facilitated. In particular, a renaming of all variables in a formula to the same one is possible. Variables are then distinguished only by the number of preceding lambda-bars. Finally, we give a four symbol representation of the lambda calculus based on the above mentioned freedom in renaming. }, topics = {FP - Lambda Calculi} } @article{BerklingFehr82a, author = {Klaus Berkling and E. Fehr}, title = {{A Consistent Extension of the Lambda Calculus as a Base for Functional Programming Languages}}, journal = {Information and Control}, volume = {55}, number = {1-3}, pages = {89-101}, year = 1982, topics = {FP - Lambda Calculi} } @article{BerklingFehr82b, author = {Klaus Berkling and E. Fehr}, title = {{A modification of the $\lambda$-calculus as a base for functional programming languages}}, journal = {{Lecture Notes in Computer Science}}, volume = {140}, pages = {35-47}, year = 1982, topics = {FP - Lambda Calculi} } From devriese at cs.tcd.ie Fri May 16 04:36:56 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Fri, 16 May 2008 09:36:56 +0100 Subject: [TYPES] Y-combinator in Type:Type? Message-ID: <20080516083656.GA9813@netsoc.tcd.ie> Hi, Assuming that Type:Type (or *:*) in dependently typed languages is said to be inconsistent (Girard's paradox?). Does that mean that it is possible to define a Y combinator in such a language? Thanks, Edsko From crary at cs.cmu.edu Fri May 16 10:11:26 2008 From: crary at cs.cmu.edu (Karl Crary) Date: Fri, 16 May 2008 10:11:26 -0400 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <20080516083656.GA9813@netsoc.tcd.ie> References: <20080516083656.GA9813@netsoc.tcd.ie> Message-ID: <482D960E.6040604@cs.cmu.edu> No. You can define a looping combinator, but not a true fixed point combinator. Doug Howe's paper "The Computational Behaviour of Girard's Paradox" is a good reference. Karl Crary Edsko de Vries wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi, > > Assuming that Type:Type (or *:*) in dependently typed languages is said > to be inconsistent (Girard's paradox?). Does that mean that it is > possible to define a Y combinator in such a language? > > Thanks, > > Edsko > > From pierre.hyvernat at univ-savoie.fr Fri May 16 10:38:29 2008 From: pierre.hyvernat at univ-savoie.fr (Pierre Hyvernat) Date: Fri, 16 May 2008 16:38:29 +0200 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <20080516083656.GA9813@netsoc.tcd.ie> References: <20080516083656.GA9813@netsoc.tcd.ie> Message-ID: <20080516143829.GA18889@d53.lama.univ-savoie.fr> Hello, > Assuming that Type:Type (or *:*) in dependently typed > languages is said to be inconsistent (Girard's > paradox?). Does that mean that it is possible to > define a Y combinator in such a language? > If I am not mistaken, this is still an open question. Thierry Coquand and Hugo Herbelin showed how to get "looping" combinators inside any inconsistent PTS. This is enough for all "programming" purposes: "A-translation and looping combinators in PTS", Journal of Functional Programming , Volume 4, 1994. The paper is available on Hugo Herbelin's web page... The existence of a fixpoint combinator for *:* is said to be open in the conclusion, and last time I asked (about a year ago), it was still the case. Concerning this, you should also have a look at "Remarks on the Equational Theory of non-Normalizing PTS" by Thierry Coquand and Gilles Barthe, Journal of Functional Programming, 14(2), 2004. (Available on Gilles Barthe's page.) I guess more knowledgeable people will have other suggestions (which I'd welcome)... All the best Pierre -- From herman at cs.ru.nl Fri May 16 10:50:33 2008 From: herman at cs.ru.nl (Herman Geuvers) Date: Fri, 16 May 2008 16:50:33 +0200 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <20080516083656.GA9813@netsoc.tcd.ie> References: <20080516083656.GA9813@netsoc.tcd.ie> Message-ID: <482D9F39.9080300@cs.ru.nl> Edsko de Vries wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi, > > Assuming that Type:Type (or *:*) in dependently typed languages is said > to be inconsistent (Girard's paradox?). Does that mean that it is > possible to define a Y combinator in such a language? > > No but you can define a family of looping combinators: Y_0, Y_1, Y_2 ... satisfying the property Y_i F = F(Y_{i+1} F) This is proven in* A-translation and Looping Combinators in Pure Type Systems by Thierry Coquand, Hugo Herbelin, Journal of Functional Programming (1994)*** This is enough to type all partial recursive functions. (For the know proof of representation of recursive functions in lambda calculus, a looping combinator suffices.) Using the short proof of inconsistency by Hurkens, one can actually exhibit such a looping combinator, and if you look at the underlying "Curry variant" of it (which you can exhibit in the system lambda-U), then it is a fixed point combinator indeed. So the looping occurs just because the type information in the term gets bigger and bigger; the underlying untyped term is a fixed-point combinator. See also an old note of mine, where the latter result is just mentioned without proof. Best Regards Herman Geuvers Reference: ||A. J. Hurkens, "A simplification of Girard's paradox", Proceedings of the 2nd international conference Typed Lambda-Calculi and Applications (TLCA'95), 1995. H. Geuvers, Inconsistency of classical logic in type theory, Short Note (Version of November 27, 2001) http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz From Francois.Pottier at inria.fr Fri May 16 10:55:49 2008 From: Francois.Pottier at inria.fr (Francois Pottier) Date: Fri, 16 May 2008 16:55:49 +0200 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <20080516083656.GA9813@netsoc.tcd.ie> References: <20080516083656.GA9813@netsoc.tcd.ie> Message-ID: <20080516145549.GB3357@yquem.inria.fr> Hello, On Fri, May 16, 2008 at 09:36:56AM +0100, Edsko de Vries wrote: > Assuming that Type:Type (or *:*) in dependently typed languages is said > to be inconsistent (Girard's paradox?). Does that mean that it is > possible to define a Y combinator in such a language? There is an interesting 1987 paper by Howe about this question: http://ecommons.library.cornell.edu/handle/1813/6660 Howe did not settle the question. I don't know if it has been settled since? Best regards, -- Fran?ois Pottier Francois.Pottier at inria.fr http://cristal.inria.fr/~fpottier/ From streicher at mathematik.tu-darmstadt.de Fri May 16 11:41:42 2008 From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher) Date: Fri, 16 May 2008 17:41:42 +0200 (CEST) Subject: [TYPES] Y-combinator in Type:Type? Message-ID: <200805161541.m4GFfgZm031240@fb04209.mathematik.tu-darmstadt.de> But if you have Type:Type together with extensional identity types then every type X is equal to X->X and thus provides a model for untyped lambda calculus and thus allows one to write down an Y-combinator of type X. So the problem is open because of intensional identity types, isn't it? Thomas From andreas.abel at ifi.lmu.de Fri May 16 13:35:24 2008 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Fri, 16 May 2008 19:35:24 +0200 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <20080516143829.GA18889@d53.lama.univ-savoie.fr> References: <20080516083656.GA9813@netsoc.tcd.ie> <20080516143829.GA18889@d53.lama.univ-savoie.fr> Message-ID: <482DC5DC.2070500@ifi.lmu.de> Pierre Hyvernat wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello, > >> Assuming that Type:Type (or *:*) in dependently typed >> languages is said to be inconsistent (Girard's >> paradox?). Does that mean that it is possible to >> define a Y combinator in such a language? > > Concerning this, you should also have a look at > > "Remarks on the Equational Theory of non-Normalizing > PTS" by Thierry Coquand and Gilles Barthe, Journal of > Functional Programming, 14(2), 2004. In that very paper a fixed-point combinator is given for domain-free *:*. I.e., there is a fixed-point combinator if you ignore the type-labels in lambda-abstraction. Andreas -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/ From devriese at cs.tcd.ie Fri May 16 17:20:22 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Fri, 16 May 2008 22:20:22 +0100 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <20080516083656.GA9813@netsoc.tcd.ie> References: <20080516083656.GA9813@netsoc.tcd.ie> Message-ID: <20080516212022.GA9705@netsoc.tcd.ie> Thanks for all the responses! Most helpful, as always :) Edsko From andreas.abel at ifi.lmu.de Mon May 19 09:03:55 2008 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Mon, 19 May 2008 15:03:55 +0200 Subject: [TYPES] SN for System F with countable universe of types? Message-ID: <48317ABB.8020801@ifi.lmu.de> When proving strong normalization for System F a la Girard, one uses a complete lattice SAT of saturated sets (reducibility candidates, resp.). SAT is uncountable. However, there are only countably many type expressions. Thinking naively, it should be possible to only use a countable part of SAT to interpret type expressions. Is this possible? Are there any results on this question? Reminder: The interpretation [[A]]rho in SAT of type A in environment rho is defined by induction on A as follows: [[X]]rho = rho(X) [[A -> B]]rho = [[A]]rho => [[B]]rho (function space on SAT) [[forall X A]]rho = intersect_{S in SAT} [[A]](rho,X=S) The intersection is over an uncountable set. Cheers, Andreas -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/ From txa at Cs.Nott.AC.UK Mon May 19 10:16:05 2008 From: txa at Cs.Nott.AC.UK (Thorsten Altenkirch) Date: Mon, 19 May 2008 15:16:05 +0100 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <200805161541.m4GFfgZm031240@fb04209.mathematik.tu-darmstadt.de> References: <200805161541.m4GFfgZm031240@fb04209.mathematik.tu-darmstadt.de> Message-ID: <237D184B-107C-4D4F-B6C8-5CF82D883046@cs.nott.ac.uk> Actually, the initial PTS (Type : Type) has got no identity types but only Pi-types. However, we can encode an equality type using the usual "Leibniz encoding" Eq : (A:Type) -> A -> A -> Type Eq A a b = Pi P:A -> Type.P a -> P b and this behaves like intensional equality actually worse: we cannot even show that equality is a groupoid (actually using eta we can show that it is a category but the laws involving symmetry require parametricity, I think). If you add W-types with the normal elimination principle you get a fixpoint combinator (See Thierry's paper on the paradox of Trees). That's maybe cheaper then extensional equality (depending on your currency). The problem is that the impredicative encodings don't give you primitive recursion but only iteration - I'd say. Cheers, Thorsten On 16 May 2008, at 16:41, Thomas Streicher wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > But if you have Type:Type together with extensional identity types > then > every type X is equal to X->X and thus provides a model for untyped > lambda calculus and thus allows one to write down an Y-combinator of > type X. > > So the problem is open because of intensional identity types, isn't > it? > > Thomas 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 jonathan.seldin at uleth.ca Mon May 19 18:36:35 2008 From: jonathan.seldin at uleth.ca (Jonathan P. Seldin) Date: Mon, 19 May 2008 16:36:35 -0600 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <237D184B-107C-4D4F-B6C8-5CF82D883046@cs.nott.ac.uk> References: <200805161541.m4GFfgZm031240@fb04209.mathematik.tu-darmstadt.de> <237D184B-107C-4D4F-B6C8-5CF82D883046@cs.nott.ac.uk> Message-ID: <938C6B54-2634-4342-A01A-7278ABD1F22D@uleth.ca> I cannot believe the last statement about getting iteration but not primitive recursion. In Combinatory Logic, vol. II, section 3A3, Curry gives several methods for defining the primitive recursion combinator R in terms of an iterator Z, and the compatibility of some of them with simple types is shown in section 13D3, especially Theorem 13D3 for the R he calls R(Kp). (The typing system Curry is using here is $\lambda \rightarrow$, and he is writing Fab instead of a -> b; furthermore, he is taking the type N of natural numbers as an atomic type. But with the Pi types and the impredicative definitions, N can be defined.) On 19-May-08, at 8:16 AM, Thorsten Altenkirch wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > Actually, the initial PTS (Type : Type) has got no identity types but > only Pi-types. However, we can encode an equality type using the usual > "Leibniz encoding" > > Eq : (A:Type) -> A -> A -> Type > Eq A a b = Pi P:A -> Type.P a -> P b > > and this behaves like intensional equality actually worse: we cannot > even show that equality is a groupoid (actually using eta we can show > that it is a category but the laws involving symmetry require > parametricity, I think). > > If you add W-types with the normal elimination principle you get a > fixpoint combinator (See Thierry's paper on the paradox of Trees). > That's maybe cheaper then extensional equality (depending on your > currency). The problem is that the impredicative encodings don't give > you primitive recursion but only iteration - I'd say. > > Cheers, > Thorsten > > On 16 May 2008, at 16:41, Thomas Streicher wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ >> types-list >> ] >> >> But if you have Type:Type together with extensional identity types >> then >> every type X is equal to X->X and thus provides a model for untyped >> lambda calculus and thus allows one to write down an Y-combinator of >> type X. >> >> So the problem is open because of intensional identity types, isn't >> it? >> >> Thomas > > > 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. > 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 txa at Cs.Nott.AC.UK Mon May 19 18:51:15 2008 From: txa at Cs.Nott.AC.UK (Thorsten Altenkirch) Date: Mon, 19 May 2008 23:51:15 +0100 Subject: [TYPES] Y-combinator in Type:Type? In-Reply-To: <938C6B54-2634-4342-A01A-7278ABD1F22D@uleth.ca> References: <200805161541.m4GFfgZm031240@fb04209.mathematik.tu-darmstadt.de> <237D184B-107C-4D4F-B6C8-5CF82D883046@cs.nott.ac.uk> <938C6B54-2634-4342-A01A-7278ABD1F22D@uleth.ca> Message-ID: Dear Jonathan, you are right primitive recursion can be defined from iteration. E.g. in the case of natural numbers, given It : (A:Type) -> A -> (A -> A) -> N -> A satisfying It A z s 0 = z It A z s (succ n) = s (It A z s a) we can define (using products) R : (A:Type) -> A -> (N -> A -> A) -> N -> A R A z s n = fst (It (NxA) (0,z) (\ (n,a) -> (succ n,s n a)) n) but we cannot derive the equation R A a z s (succ n) = s n (R A a z s n) from the equations for the iterator. We can only show by induction that the equation holds for all numerals, i.e. for all definable elements of type N. Cheers, Thorsten On 19 May 2008, at 23:36, Jonathan P. Seldin wrote: > I cannot believe the last statement about getting iteration but not > primitive recursion. In Combinatory Logic, vol. II, section 3A3, > Curry gives several methods for defining the primitive recursion > combinator R in terms of an iterator Z, and the compatibility of > some of them with simple types is shown in section 13D3, especially > Theorem 13D3 for the R he calls R(Kp). (The typing system Curry is > using here is $\lambda \rightarrow$, and he is writing Fab instead > of a -> b; furthermore, he is taking the type N of natural numbers > as an atomic type. But with the Pi types and the impredicative > definitions, N can be defined.) > > On 19-May-08, at 8:16 AM, Thorsten Altenkirch wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> ] >> >> Actually, the initial PTS (Type : Type) has got no identity types but >> only Pi-types. However, we can encode an equality type using the >> usual >> "Leibniz encoding" >> >> Eq : (A:Type) -> A -> A -> Type >> Eq A a b = Pi P:A -> Type.P a -> P b >> >> and this behaves like intensional equality actually worse: we cannot >> even show that equality is a groupoid (actually using eta we can show >> that it is a category but the laws involving symmetry require >> parametricity, I think). >> >> If you add W-types with the normal elimination principle you get a >> fixpoint combinator (See Thierry's paper on the paradox of Trees). >> That's maybe cheaper then extensional equality (depending on your >> currency). The problem is that the impredicative encodings don't give >> you primitive recursion but only iteration - I'd say. >> >> Cheers, >> Thorsten >> >> On 16 May 2008, at 16:41, Thomas Streicher wrote: >> >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >>> ] >>> >>> But if you have Type:Type together with extensional identity types >>> then >>> every type X is equal to X->X and thus provides a model for untyped >>> lambda calculus and thus allows one to write down an Y-combinator of >>> type X. >>> >>> So the problem is open because of intensional identity types, isn't >>> it? >>> >>> Thomas >> >> >> 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. >> > > 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 > > > 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 pierre.hyvernat at univ-savoie.fr Tue May 20 02:56:09 2008 From: pierre.hyvernat at univ-savoie.fr (Pierre Hyvernat) Date: Tue, 20 May 2008 08:56:09 +0200 Subject: [TYPES] SN for System F with countable universe of types? In-Reply-To: <48317ABB.8020801@ifi.lmu.de> References: <48317ABB.8020801@ifi.lmu.de> Message-ID: <20080520065609.GB10594@d53.lama.univ-savoie.fr> > When proving strong normalization for System F a la Girard, one uses a > complete lattice SAT of saturated sets (reducibility candidates, resp.). > SAT is uncountable. However, there are only countably many type > expressions. Thinking naively, it should be possible to only use a > countable part of SAT to interpret type expressions. > > Is this possible? Are there any results on this question? > Well, isn't it the whole point of impredicativity: that we don't really know how to do much better than that? This is not a definite answer to your question, but since one needs a little bit of third order to prove SN of system F; which probably means that you cannot hope to get a nice (say indexed by types) family of candidates to prove SN: this would allow to prove SN in second order arithmetic. Am I just babbling here? Correct me if I'm wrong... There is something by Coquand and Altenkirch for a very restricted subsystem of F in "A Finitary subsystem of the polymorphic lambda-calculus", LNCS 2044. (IIRC, this was simplified in "Completeness theorems and lambda-calculus.", LNCS 3461.) This is supposed to be a readable account of a more general result in Buchholz & Sch?tte, "Proof theory of impredicative subsystems of analysis". Somehow, Pi_1^1 quantification is predicative... Some notes by R. Labib-Sami or K. Nour & S. Farkh ("Un R?sultat de Compl?tude pour les Types positifs du Syst?me F") might might also be relevant here, but I'm not sure how... However, I've never read Labib-Sami's note, and Nour's note is in French. (Summary of Nour's note: there is a weak completeness result for positive types: t in [[A]] iff t -->* t' with |- t':A.) Pierre -- Everything should be made as simple as possible, but not simpler. -- Albert Einstein From devriese at cs.tcd.ie Mon May 26 09:51:32 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Mon, 26 May 2008 14:51:32 +0100 Subject: [TYPES] Historical question: origin of the ":" symbol Message-ID: <20080526135132.GF14143@netsoc.tcd.ie> Hi, Can anyone refer me to a discussion of the history of the symbols used in type theory? In particular, the origin of the ":" symbol? I seem to recall reading somewhere that is derived from \epsilon, which in turn is the first letter of 'esti' (to be), but I cannot remember where I read this -- might have made it up myself :) Thanks, Edsko From u.s.reddy at cs.bham.ac.uk Tue May 27 12:23:09 2008 From: u.s.reddy at cs.bham.ac.uk (Uday S Reddy) Date: Tue, 27 May 2008 17:23:09 +0100 Subject: [TYPES] Historical question: origin of the ":" symbol In-Reply-To: <20080526135132.GF14143@netsoc.tcd.ie> References: <20080526135132.GF14143@netsoc.tcd.ie> Message-ID: <18492.13677.528000.255095@gargle.gargle.HOWL> Edsko de Vries writes: > Can anyone refer me to a discussion of the history of the symbols used > in type theory? In particular, the origin of the ":" symbol? I seem to > recall reading somewhere that is derived from \epsilon, which in turn is > the first letter of 'esti' (to be), but I cannot remember where I read > this -- might have made it up myself :) I always thought the notation of f: A -> B for function types must have been the origin of the ":" symbol. Does that predate set theory? Cheers, Uday From ezra at ezrakilty.net Wed May 28 06:22:25 2008 From: ezra at ezrakilty.net (Ezra Cooper) Date: Wed, 28 May 2008 11:22:25 +0100 Subject: [TYPES] Historical question: origin of the ":" symbol In-Reply-To: <20080526135132.GF14143@netsoc.tcd.ie> References: <20080526135132.GF14143@netsoc.tcd.ie> Message-ID: On May 26, 2008, at 2:51 PM, Edsko de Vries wrote: > Can anyone refer me to a discussion of the history of the symbols used > in type theory? In particular, the origin of the ":" symbol? I seem to > recall reading somewhere that is derived from \epsilon, which in > turn is > the first letter of 'esti' (to be), but I cannot remember where I read > this -- might have made it up myself :) This may not help, but Paul Taylor briefly discusses the history of the subset symbol in "Practical Foundations of Mathematics," page 75. Ezra From devriese at cs.tcd.ie Wed May 28 14:36:55 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Wed, 28 May 2008 19:36:55 +0100 Subject: [TYPES] \lambda 2 a subset of System F? Message-ID: <20080528183655.GA8307@netsoc.tcd.ie> Hi, (Sorry to be asking these basic questions) In his description of the lambda cube, Barendregt mentions that his system "\lambda 2" (with (*,*) and ([], *)) is a subset of System F. In what sense is it a subset? It seems to me that there is a rather direct mapping from the System F typing rules (as described in "System F of variable types: 15 years later", for example) to the specialization of Barendregt's Forall and Abs rules to (*,*) and ([], *). Are there terms that can be typed in System F that cannot be typed in \lambda 2? (I don't have a copy of Girard's original thesis and so have to rely on later definitions, unfortunately.) Thanks, Edsko From moelius at cis.udel.edu Tue Jun 3 06:38:13 2008 From: moelius at cis.udel.edu (Samuel E. Moelius III) Date: Tue, 03 Jun 2008 06:38:13 -0400 Subject: [TYPES] Question about the polymorphic lambda calculus Message-ID: <48451F15.3030302@cis.udel.edu> Suppose that T is a type with exactly one free variable X. Further suppose that for every closed type U, there is some term with type T[U/X]. Then, does there necessarily exist some term with type (forall X. T)? In other words, in the situation described above, can the meta-level ``forall'' be pushed down into the types? If this is a theorem, could someone please point me to a proof of it? Thanks in advance. Sam Moelius From noam+types at cs.cmu.edu Tue Jun 3 11:34:05 2008 From: noam+types at cs.cmu.edu (Noam Zeilberger) Date: Tue, 3 Jun 2008 11:34:05 -0400 Subject: [TYPES] Question about the polymorphic lambda calculus In-Reply-To: <48451F15.3030302@cis.udel.edu> References: <48451F15.3030302@cis.udel.edu> Message-ID: <20080603153403.GA22041@cs.cmu.edu> On Tue, Jun 03, 2008 at 06:38:13AM -0400, Samuel E. Moelius III wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, there is some term with type > T[U/X]. Then, does there necessarily exist some term with type (forall > X. T)? > > In other words, in the situation described above, can the meta-level > ``forall'' be pushed down into the types? I'm not sure these two questions are the same. As stated, I'm reading the first question as: Question 1 Suppose that T is a type with exactly one free variable X. Further suppose that for every closed type U, the type T[U/X] is inhabited. Then is the type (forall X.T) inhabited? But perhaps you mean something like so, which could more naturally be considered "pushing down the meta-level forall": Question 2 Suppose that T is a type with exactly one free variable X. Further suppose that for every closed type U, there is some term t_U with type T[U/X]. Then does there exist some term t with type (forall X. T), such that for all U, the terms t(U) and t_U are observationally equivalent? The answer to Q2 is no, in general. For a counterexample, suppose we have sum types T1+T2. If these aren't primitive, we can Church encode them (T1+T2 = forall Y.(T1->Y)->(T2->Y)->Y). Let T = 1+X, and define the term t_U of type 1+U as follows: inr(t') if there exists some t' : U t_U = inl() if U is uninhabited Now, there is only one inhabitant of the type (forall X.1+X), the term t = [X].inl(). But for inhabited types U, t(U) is not equivalent to t_U. If you drop the restriction that X appears exactly once in T, you can come up with even simpler counterexamples. For example, with T = bool (again, you can Church encode the booleans), take true if U = bool t*_U = false otherwise In fact, the restriction doesn't make a difference, because you can weaken T to X->bool and define t*_U appropriately as \x.true or \x.false. Is Q2 what you meant, or did you really mean Q1? Noam From moelius at cis.udel.edu Tue Jun 3 12:26:15 2008 From: moelius at cis.udel.edu (Samuel E. Moelius III) Date: Tue, 3 Jun 2008 12:26:15 -0400 Subject: [TYPES] Question about the polymorphic lambda calculus In-Reply-To: <20080603153403.GA22041@cs.cmu.edu> Message-ID: Noam, > I'm not sure these two questions are the same. As stated, I'm > reading the first question as: > > Question 1 > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, the type T[U/X] is inhabited. > Then is the type (forall X.T) inhabited? Yes, that's exactly what I meant. But your response to the alternative question was interesting and appreciated, nonetheless. :) Sam From noam+types at cs.cmu.edu Wed Jun 4 12:41:52 2008 From: noam+types at cs.cmu.edu (Noam Zeilberger) Date: Wed, 4 Jun 2008 12:41:52 -0400 Subject: [TYPES] Question about the polymorphic lambda calculus In-Reply-To: References: <20080603153403.GA22041@cs.cmu.edu> Message-ID: <20080604164152.GA23990@cs.cmu.edu> On Tue, Jun 03, 2008 at 12:26:15PM -0400, Samuel E. Moelius III wrote: > >Question 1 > > Suppose that T is a type with exactly one free variable X. Further > > suppose that for every closed type U, the type T[U/X] is inhabited. > > Then is the type (forall X.T) inhabited? > > Yes, that's exactly what I meant. Aha, sorry I assumed otherwise. I think the answer to Q1 is yes. Examine the single occurrence of X in T. Is it positive or negative? (Definition: X occurs positively in X; X occurs positively (neg.) in A->B if it occurs pos. (neg.) in B or neg. (pos.) in A.) Then define an instance T' of T as follows: T[bot/X] X occurs positively T' = T[top/X] X occurs negatively where top = forall Y.Y->Y and bot = forall Y.Y By assumption, T' is inhabited. From this it follows that T (and hence forall X.T) is inhabited, by the following pair of lemmas: Lemmas 1. If X occurs only positively in T, then [bot/X]T |- T, and if negatively then T |- [bot/X]T 2. If X occurs only positively in T, then T |- [top/X]T, and if negatively then [top/X]T |- T Proof: by induction on T. Do you buy that? It seems that the statement can be generalized to when T has multiple occurrences of X, but they are all either positive or negative. I am curious, though, of whether you know of any counterexamples when X occurs both positively and negatively in T? Noam From miles at milessabin.com Wed Jun 4 13:28:27 2008 From: miles at milessabin.com (Miles Sabin) Date: Wed, 4 Jun 2008 18:28:27 +0100 Subject: [TYPES] Question about the polymorphic lambda calculus In-Reply-To: <48451F15.3030302@cis.udel.edu> References: <48451F15.3030302@cis.udel.edu> Message-ID: <30961e500806041028w4573c84dyf5ca2390dc38005a@mail.gmail.com> On Tue, Jun 3, 2008 at 11:38 AM, Samuel E. Moelius III wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, there is some term with type > T[U/X]. Then, does there necessarily exist some term with type (forall > X. T)? > > In other words, in the situation described above, can the meta-level > ``forall'' be pushed down into the types? Maybe I'm missing something, but I would have thought that in general the answer has to be no: it doesn't follow from the fact that universal quantification is expressible in the meta-language that it's expressible in the object-language. Compare the analogous situation with first-order predicate calculus as the meta-language for first-order propositional calculus with countably infinite named constants and a finiteness constraint on proposition and proof length. Cheers, Miles From noam+types at cs.cmu.edu Wed Jun 4 13:37:59 2008 From: noam+types at cs.cmu.edu (Noam Zeilberger) Date: Wed, 4 Jun 2008 13:37:59 -0400 Subject: [TYPES] Question about the polymorphic lambda calculus In-Reply-To: <20080604164152.GA23990@cs.cmu.edu> References: <20080603153403.GA22041@cs.cmu.edu> <20080604164152.GA23990@cs.cmu.edu> Message-ID: <20080604173759.GA24128@cs.cmu.edu> On Wed, Jun 04, 2008 at 12:41:52PM -0400, Noam Zeilberger wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > On Tue, Jun 03, 2008 at 12:26:15PM -0400, Samuel E. Moelius III wrote: > > >Question 1 > > > Suppose that T is a type with exactly one free variable X. Further > > > suppose that for every closed type U, the type T[U/X] is inhabited. > > > Then is the type (forall X.T) inhabited? > > > > Yes, that's exactly what I meant. > > Aha, sorry I assumed otherwise. I think the answer to Q1 is yes. > Examine the single occurrence of X in T. Oops, it seems I read too much into the question again. Samuel did not state that T has a single occurrence of X, just that X is the single free type variable. Noam From moelius at cis.udel.edu Thu Jun 5 08:01:47 2008 From: moelius at cis.udel.edu (Samuel E. Moelius III) Date: Thu, 05 Jun 2008 08:01:47 -0400 Subject: [TYPES] Question about the polymorphic lambda calculus In-Reply-To: <30961e500806041028w4573c84dyf5ca2390dc38005a@mail.gmail.com> References: <48451F15.3030302@cis.udel.edu> <30961e500806041028w4573c84dyf5ca2390dc38005a@mail.gmail.com> Message-ID: <4847D5AB.5020308@cis.udel.edu> Miles, > Maybe I'm missing something, but I would have thought that in general > the answer has to be no: it doesn't follow from the fact that > universal quantification is expressible in the meta-language that it's > expressible in the object-language. I appreciate your point. But this case is special in at least two respects: (1) the quantified statements are all of a certain form (i.e., there exists a term with a certain type), and (2) the object language is the polymorphic lambda calculus, specifically. For this special case, I think there is good reason to suspect that the universal quantifier can be expressed in the object language. Sam From herman at cs.ru.nl Fri Jun 6 08:58:31 2008 From: herman at cs.ru.nl (Herman Geuvers) Date: Fri, 06 Jun 2008 14:58:31 +0200 Subject: [TYPES] Question about the polymorphic lambda calculus In-Reply-To: <48451F15.3030302@cis.udel.edu> References: <48451F15.3030302@cis.udel.edu> Message-ID: <48493477.6090801@cs.ru.nl> Samuel E. Moelius III wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, there is some term with type > T[U/X]. Then, does there necessarily exist some term with type (forall > X. T)? > > In other words, in the situation described above, can the meta-level > ``forall'' be pushed down into the types? > > If this is a theorem, could someone please point me to a proof of it? > > Thanks in advance. > > Sam Moelius > > Dear Sam, If I look at your question in the polymorphic lambda calculus (system F), then it is basically a question about derivability in second order proposition logic PROP2: Does the following hold? If |- Phi(U) for every closed proposition U, then |- forall X Phi(X) PROP2 is constructive proposition logic: only implication -> and a second order quantifier over propositions. Now, in the classical case, your conjecture holds, because then, if |- Phi(U) for every closed proposition U, then |- Phi(top) and |- Phi(bot) and so |- forall X. Phi(X). (In classical PROP2, let's call it CPROP2, we have an axiom forall X.(X \/ ~X); bot is forall X.X and top is forall X. X->X. The definition of the connectives is just the usual one from PROP2.) That |- Phi(top) and |- Phi(bot) imply |- forall X. Phi(X) is because we have a complete truth table semantics for CPROP2. I have spelled that out in detail in my PhD thesis in 1993. Now, can we conclude anything from this for PROP2? Yes, because there is a G"odel not-not translation from CPROP2 to PROP2. One can take the one from Coquand-Herbelin (called "A-translation" in their paper) or the "standard one" in the book of Van Dalen (Logic and Structure): Coquand-Herbelin: X* := X (A->B)* := ~~A* -> ~~B* (forall X.A)* := forall X. ~~A* van Dalen: X* := ~~X (A->B)* := A* -> B* (forall X.A)* := forall X. A* For the first one, we have Gamma |-_{CPROP2} phi <=> ~~(Gamma*) |- _{PROP2} ~~(phi*) For the second one, we have Gamma |-_{CPROP2} phi <=> Gamma* |- _{PROP2} phi* So if we consider the van Dalen translation, we can derive that for formulas of the form Phi(X)*, we have (in PROP2): If |- Phi(U)* for every closed proposition U, then |- forall X. Phi(X)* Proof: If |-_{PROP2} Phi(U)* for every closed proposition U, then |-_{PROP2} Phi(top)* and |-_{PROP2} Phi(bot)*, so |-_{CPROP2} Phi(top) and |-_{CPROP2} Phi(bot), so |-_{CPROP2} forall X. Phi(X), so |-_{PROP2} forall X. Phi(X)*. I have no idea to which extent this extends to the general case. Best Regards Herman Geuvers References: ======== My PhD thesis: J.H. Geuvers, Logics and Type systems , PhD. Thesis, University of Nijmegen, September 1993. http://www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz Thierry Coquand, Hugo Herbelin A-translation and Looping Combinators in Pure Type Systems, 1994, Journal of Functional Programming Dirk van Dalen Logic and Structure (3rd extended ed.). Springer Verlag, Berlin. From matthias at ccs.neu.edu Tue Jun 10 09:34:43 2008 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Tue, 10 Jun 2008 09:34:43 -0400 Subject: [TYPES] Fwd: Revenue-neutral Adjustment for Functional Programming References: <10E6AA40-9F02-4F84-8004-20879B3D1411@ccs.neu.edu> Message-ID: <2AB09C8E-B503-4BD9-98D1-22B2591BD234@ccs.neu.edu> This message is slightly off-topic, and apologies for that. I believe, however, that it is in the spirit of this list. The ACM Curriculum board has re-opened the 2001 design for review. Although ACM is a US-based organization, the curriculum is not only influential at the middle tier of US colleges and universities, it is also taken seriously by many evolving and developing educational institutions overseas. As you may recall, I alerted the readers of this list in the late 90s that the curriculum has relegated the study of PL and type systems to a peripheral status. We may now have an opening to make a small change. The ACM Curriculum board has agreed to consider a proposal on including FP as an equal to OOP (10 "hours" each) in the standard curriculum. See forwarded message below. This was the most concrete outcome of the PLC workshop at Harvard two weeks ago. (Stuart Reges, Shriram Krishnamurthi, and I drafted the proposal; Larry Snyder volunteered to submit it once the workshop expressed its unanimous support. The three of us came to the conclusion that only an inclusion of FP in the general curriculum will prepare students for properly designed though possibly optional PL courses, including a thorough study of type systems.) Please consider contributing comments to the web site. A simple "Yes, I think this is a great idea" will be helpful. A short explanation is even better. Thanks -- Matthias >> Begin forwarded message: >> >>> From: Larry Snyder >>> Date: June 9, 2008 6:58:43 PM EDT >>> To: PL-CURRC-WKSHP-INVITEES at LISTSERV.ACM.ORG >>> Subject: Revenue-neutral Adjustment for Functional Programming >>> Reply-To: Larry Snyder >>> >>> Colleagues: >>> >>> The ACM Education Board accepted our last minute input for adding >>> Functional Programming to the core of the revised CC2001-CS >>> curriculum, has posted our proposed changes on it's Web site >>> >>> http://wiki.acm.org/cs2001/index.php?title=SIGPLAN_Proposal >>> >>> and invited comments. Feel free to endorse our "revenue neutral" >>> workshop motion. (I quickly wrote the text in support of this for >>> use by the Ed Board, not expecting it to be included in the >>> posting; so apologies if I missed points or messed them up.) >>> Accordingly, crisp arguments for this change will doubtless be >>> helpful. -- LS >>> >> > From Luigi.Liquori at sophia.inria.fr Wed Jun 11 06:12:38 2008 From: Luigi.Liquori at sophia.inria.fr (Luigi Liquori INRIA) Date: Wed, 11 Jun 2008 12:12:38 +0200 Subject: [TYPES] =?iso-8859-1?q?Paper_announcement=3A_Intersection_types_?= =?iso-8859-1?q?=E0_la_Church?= Message-ID: <52DF8FBA-7F2A-4BD0-8E77-9464FC131EB1@sophia.inria.fr> I'm pleased to announce the available of a new paper on Intersection Types ? la Church: http://dx.doi.org/10.1016/j.ic.2007.03.005 http://www-sop.inria.fr/members/Luigi.Liquori/PAPERS/ic-07.pdf As always, comments and suggestions are welcome. Luigi Liquori and Simona Ronchi Della Rocca. Intersection-Types ? la Church by Luigi Liquori INRIA Sophia Antipolis, France Simona Ronchi Della Rocca Dipartimento di Informatica, Universit? di Torino, Italy Abstract In this paper, we present ?t?, a fully typed ?-calculus based on the intersection-type system discipline, which is a counterpart ? la Church of the type assignment system as invented by Coppo and Dezani. The relationship between ?t? and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable. Key words: Logics and Intersection-Types, ?-calculus ? la Curry and ? la Church -- Luigi Liquori, H.d.R., Ph.D. INRIA Researcher, Sophia Antipolis M?diterran?e LogNet Research Team Vox : +33 4 92 38 71 93 Fax : +33 4 92 38 79 71 Hom : +33 4 93 67 09 72 MobFr : +33 6 65 39 51 32 MobIt : +39 3 49 16 56 45 1 SIP : luigi_liquori at voip.wengo.fr Url : www-sop.inria.fr/members/Luigi.Liquori Url : www.inria.fr/recherche/equipes/lognet.en.html Email : Let (*,#)=(.,@) in Luigi*Liquori#inria*fr Addr : INRIA, 2004 Route des Lucioles - BP 93 FR-06902 Sophia Antipolis, France ? Pensez ? la plan?te et n'imprimez ce message que si n?cessaire ! Earth will kind ask you to print this message only if really needed! ? From aurelien.pardon at ens-lyon.fr Fri Jun 20 06:12:19 2008 From: aurelien.pardon at ens-lyon.fr (Aurelien Pardon) Date: Fri, 20 Jun 2008 12:12:19 +0200 Subject: [TYPES] connectedness and acyclicity in IMLL proof nets Message-ID: <20080620121219.e5styk3mnqgoko0c@tadorne.ens-lyon.fr> Dear all, Has anyone already noticed that a switching of an intuitionistic multiplicative linear logic (IMLL) proof-structure is acyclic iff it is connected (in the sense of the Danos-Regnier correctness criterion of proof nets) ? A simple corollary is: "An IMLL proof-structure is correct if all its switchings are connected or acyclic." Here is a simple proof: We assume a set of propositional variables V. IMLL formulas are built from the following syntax: F ::= v | I | F -o F | F x F where v is a variable belonging to V, "-o" stands for the linear implication and "x" for the tensor. The leaves of a formula F are the occurrences of variables and I's. Its sets of positive leaves F+ and negative leaves F- are inductively defined by: v+ = {v} v- = \emptyset I+ = {I} I- = \emptyset (A x B)+ = A+ + B+ (A x B)- = A- + B- (A -o B)+ = A- + B+ (A -o B)- = A+ + B-, where + is coproduct. As proof-structures on the IMLL sequent F1,...,Fn |- F are in one-to-one correspondence with proof-structures on the sequent |- (F1 x ... x Fn) -o F, one being correct iff the other is, we don't loose generality by considering only IMLL proof-structures on a single formula. Such an IMLL proof-structure is then an IMLL formula together with a "leaf" function from negative leaves to positive leaves, bijective and label-preserving on variables. The graph G = (V,E) of a proof-structure is the "glueing" of the formula's graph and the leaf function's graph. More precisely, its vertices are the leaves and the connectives of the formula; its edges are the edges of the syntax tree (between connectives or between a connective and a leaf), plus the edges of the leaf function's graph (between leaves). A switching (V,E') of G is obtained by removing one of the two auxiliary edges of each positive "-o" and negative "x" in G. This corresponds to the notion of switching in MLL nets by the translation from IMLL formulas to MLL formulas: A -o B |----> A* par B (where * stands for linear negation). By induction, it is easy to prove that, in an IMLL formula F, there are as many negative leaves as switched connectives (denoted by F_s) and one more positive leaf than there are non-switched connectives (denoted by F_ns). The induction may be summed up in a table (best viewed with a fixed-width font): | |F+| | |F-| | |F_s| | |F_ns| | ------------------------------------------------------------------------------ v | 1 | 0 | 0 | 0 | I | 1 | 0 | 0 | 0 | A x B | |A+| + |B+| | |A-| + |B-| | |A_s| + |B_s| | |A_ns| + |B_ns| +1 | A -o B | |A-| + |B+| | |A+| + |B-| | |A_ns| + |B_s| + 1 | |A_s| + |B_ns| | Thus, by induction, we have: | |F-| - |F_s| | |F+| - |F_ns| | ---------------------------------------- v | 0 | 1 | I | 0 | 1 | A x B | 0 | 1 | A -o B | 0 | 1 | The graph T of the IMLL formula is a tree, thus its number of vertices exceed its number of edges by one. G contains exactly |F-| more edges, arising from the leaf function, than T. Any switching of G contains exactly |F_s| less edges than G (one edge of each switched connective is removed). Thus, any switching (V,E') satisfies that |V| = |E'| + 1. It is a well-known result of graph theory that this implies the equivalence between connectedness and acyclicity. From s-matsuoka at aist.go.jp Sun Jun 22 22:46:52 2008 From: s-matsuoka at aist.go.jp (Satoshi Matsuoka) Date: Mon, 23 Jun 2008 11:46:52 +0900 Subject: [TYPES] connectedness and acyclicity in IMLL proof nets In-Reply-To: <20080620121219.e5styk3mnqgoko0c@tadorne.ens-lyon.fr> References: <20080620121219.e5styk3mnqgoko0c@tadorne.ens-lyon.fr> Message-ID: <20080623114628.C70B.1469792C@aist.go.jp> Dear Aurelien, In MLL, your observation holds if a proof structure satisfies the equation #(ID) = #( x ) + 1, where #(ID) is the number of the ID-links and #( x ) is the number of the tensor-links in the proof structure. The equation is an invariant of MLL proof nets, which you can find in "Le Point Aveugle I" by Girard. Best regards, -- Satoshi Matsuoka National Institute of Advanced Industrial Science and Technology 1-1-1 Umezono,Tsukuba,Ibaraki 305-8563, Japan E-mail : matsuoka at ni.aist.go.jp TEL : +81-29-861-4106 From ko at daimi.au.dk Sun Jun 22 09:05:57 2008 From: ko at daimi.au.dk (Klaus Ostermann) Date: Sun, 22 Jun 2008 15:05:57 +0200 Subject: [TYPES] Universe Polymorphism Message-ID: <485E4E35.3010400@daimi.au.dk> Dear Types Readers, I'd like to learn about languages that support an infinite number of type universes, and in particular the notion of "universe polymorphism", as described in Harper and Pollack's "Type Checking With Universes" paper. In particular I am interested in practical (maybe implemented?) programming languages which support an infinite number of universes, some notion of "type:type", or other interesting features along these lines. All the calculi that I have seen seem to be based on dependent types (such as Generalized Calculus of Constructions). Wouldn't it also be possible to extend, say, F-Omega, with an infinite number of universes, without adding dependent types? Has this already been done? I would assume that in such a language it would be possible to add, say, a fixed point operator (on the term level) to the language without rendering type checking undecidable, because types do not depend on terms. What are the practical implications of having "type:type"? I read that it destroys the consistency of the type system as a logic, but this is not relevant for my purposes. On one hand, I have read that type-checking in systems with "type:type" is not decidable, but on the other hand, the paper "Why dependent types matter" mentions in Sec. 7 that the authors have adopted "type:type" in their Epigram language. How does this fit together? Are there any useful examples in Epigram (or any other language) that use the "type:type" possibility? Regards, Klaus Ostermann From soloviev at irit.fr Mon Jun 23 13:54:22 2008 From: soloviev at irit.fr (soloviev@irit.fr) Date: Mon, 23 Jun 2008 19:54:22 +0200 (CEST) Subject: [TYPES] connectedness and acyclicity in IMLL proof nets In-Reply-To: <20080623114628.C70B.1469792C@aist.go.jp> References: <20080620121219.e5styk3mnqgoko0c@tadorne.ens-lyon.fr> <20080623114628.C70B.1469792C@aist.go.jp> Message-ID: <35861.141.115.8.141.1214243662.squirrel@websecu.irit.fr> Dear all, in fact, the acyclicity and connectedness follows very easily from the fact that a) every IMLL derivation can be obtained by substitution of I, elimination of "redundant" I's (like in A x I and I-o A) and identification of variables from some derivation of a balanced sequent without I (balanced = every variable occurs exactly twice with opposite signs) b) in case of a derivable balanced sequent there is no cycles, for example, because IMLL derivations may be seen also as a subclass of derivations in classical logics, and for balanced sequents there are trivial valuations that show the absence of cycles. I had a lemma A. Babaev, S. Soloviev "A coherence theorem for canonical morphisms in cartesian closed categories", Journal of Soviet Math., v.20 , pp.2263-2282 (1982) (lemma 3) which describes this valuation, and in my ph.d. thesis (1985) similar results and their consequences for a logical system for Symmetric Monoidal Closed Categories (equivalent to IMLL) were obtained. I discussed this also in my lectures in Munich in 1995 (it may be still on the site of LMU). I would like to stress here that these results may be obtained quite easily. Best Sergei Soloviev > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear Aurelien, > > In MLL, your observation holds if a proof structure satisfies > the equation #(ID) = #( x ) + 1, where #(ID) is the number of > the ID-links and #( x ) is the number of the tensor-links in > the proof structure. > > The equation is an invariant of MLL proof nets, which you can find > in "Le Point Aveugle I" by Girard. > > Best regards, > -- > Satoshi Matsuoka > National Institute of > Advanced Industrial Science and Technology > 1-1-1 Umezono,Tsukuba,Ibaraki > 305-8563, Japan > E-mail : matsuoka at ni.aist.go.jp > TEL : +81-29-861-4106 > > > From seha at informatik.uni-kiel.de Tue Jun 24 03:33:16 2008 From: seha at informatik.uni-kiel.de (Sebastian Hanowski) Date: Tue, 24 Jun 2008 09:33:16 +0200 Subject: [TYPES] Universe Polymorphism In-Reply-To: <485E4E35.3010400@daimi.au.dk> References: <485E4E35.3010400@daimi.au.dk> Message-ID: <20080624073315.GA15733@bilbo.informatik.uni-kiel.de> * Am 22.06.08 schrieb Klaus Ostermann: > In particular I am interested in practical (maybe implemented?) > programming languages which support an infinite number of universes, > some notion of "type:type", or other interesting features along these > lines. Have a look at: http://www.cs.nott.ac.uk/~txa/publ/pisigma.pdf http://sneezy.cs.nott.ac.uk/cgi-bin/PiSigma > What are the practical implications of having "type:type"? I read that > it destroys the consistency of the type system as a logic, but this is > not relevant for my purposes. On one hand, I have read that > type-checking in systems with "type:type" is not decidable, but on the > other hand, the paper "Why dependent types matter" mentions in Sec. 7 > that the authors have adopted "type:type" in their Epigram language. > How does this fit together? Are there any useful examples in Epigram > (or any other language) that use the "type:type" possibility? "Type:Type" is not part of the design of the Epigram programming language. Foundational issues with polymorphic stratified universes, postponed design decisions and a prototypical implementation probably all can count in why it is present in the Epigram 1 system. For an outlook into the future see: http://article.gmane.org/gmane.comp.lang.epigram/167 And this an 'idiomatic' Epigram program showing universe polymorphism beeing desirable, which in the meantime is only possible with the *:* shortcut: http://sneezy.cs.nott.ac.uk/epigram/durham/examples/ctm/veczip.epi Cheers, Sebastian From Xavier.Leroy at inria.fr Wed Jun 25 04:35:09 2008 From: Xavier.Leroy at inria.fr (Xavier Leroy) Date: Wed, 25 Jun 2008 10:35:09 +0200 Subject: [TYPES] Universe Polymorphism In-Reply-To: <485E4E35.3010400@daimi.au.dk> References: <485E4E35.3010400@daimi.au.dk> Message-ID: <4862033D.3020003@inria.fr> > What are the practical implications of having "type:type"? I read > that it destroys the consistency of the type system as a logic, but > this is not relevant for my purposes. There is an old technical report by Luca Cardelli that discusses Type:Type from a programming language viewpoint: http://lucacardelli.name/Papers/TypeType.A4.pdf I don't think Cardelli implemented these ideas -- the Quest language that he designed and implemented shortly after was stratified into terms, types and kinds, probably because it was an imperative language (see below). > On one hand, I have read that type-checking in systems with > "type:type" is not decidable Here is my (limited) understanding of the problem, from a programming language viewpoint. Apologies for the inaccuracies. - Even for a restricted language of terms (no fixed-point operator), various paradoxes can be encoded with Type:Type, establishing undecidability of type-checking. However, the programmer has to go to a long way to run into undecidability. In this respect, this is no worse than other programming languages where type-checking is also undecidable "in corner cases", such as full F_sub, the C++ template language, or OCaml's higher-order functors. - If the term language contains general recursive functions, as seems necessary for a fully-fledged programming language, it is much easier to run into undecidability, since arbitrary computations can be performed at compile-time at the type level. Stratification could then become desirable, e.g. have general recursion at the bottom level but only structural recursion at higher levels. - If the term language contains imperative features such as ML's references, I'd be worried that the type system could become unsound. Stratification appears necessary to confine imperative features to a bottom level of computations. For an example of such stratification, see e.g. the work by Zhong Shao and his group: http://flint.cs.yale.edu/flint/publications/tscb-toplas.html Hope this helps, - Xavier Leroy From txa at Cs.Nott.AC.UK Wed Jun 25 11:55:57 2008 From: txa at Cs.Nott.AC.UK (Thorsten Altenkirch) Date: Wed, 25 Jun 2008 16:55:57 +0100 Subject: [TYPES] Universe Polymorphism In-Reply-To: <485E4E35.3010400@daimi.au.dk> References: <485E4E35.3010400@daimi.au.dk> Message-ID: <07C96242-85B8-4A76-A059-8C5B4F2EE190@cs.nott.ac.uk> Hi Klaus, > What are the practical implications of having "type:type"? I read > that it destroys the consistency of the > type system as a logic, but this is not relevant for my purposes. On > one hand, I have read > that type-checking in systems with "type:type" is not decidable, but > on the other hand, the paper > "Why dependent types matter" mentions in Sec. 7 that the authors > have adopted "type:type" in their > Epigram language. How does this fit together? Are there any useful > examples in Epigram (or any other language) that > use the "type:type" possibility? To add to this: recently, I asked for Type:Type (or rather Set:Set) to be added to Agda because since Agda currently doesn't support any sort of universe polymorphism you frequently had to duplicate code. Thanks to Ulf and Nisse this was implemented very quickly - now you only have to set a flag to indicate that you are "lying". One particular example was that the Agda library has a function [_,_] for copairing, i.e. if f : A -> C and g : B -> C then [f,g] : A+B -> C and I wanted to use this on dependent types, i.e. I had f: A -> Set and g : B -> Set and wanted to construct [f.g]: A+B -> Set. Agda complained that Set:Set1 but the function [_,_] required C:Set. This sort of example is covered by currently implemented forms of universe polymorphism (e.g. in Coq) but when you start programming with types more seriously you easily run into examples which are beyond the state of the art, e.g. you may want that the function \ F:Type -> Type. F o F has the Type (Pi i.Type (i) -> Type(i+1)) -> Type (j) -> Type (j+2). Indeed, I think, this was the reason for Conor to avoid this issue altogether when implementing Epigram and use Type:Type as a stop-gap until a reasonable form of universe polymorphism is implemented. It seems to me that Type:Type is an honest form of impredicativity, because at least you know that the system is inconsistent as a logic (as opposed to System F where so far nobody has been able to show this :-). Type:Type includes System F and the calculus of constructions and I think all *reasonable* programs can be reformed into Type(i):Type(i+1) possibly parametric in i. However, sometimes you don't want to think about the levels initially and sort this out later - i.e. use Type:Type. A similar attitude makes sense in Mathematics, in particular Category Theory, where it is convenient to worry about size conditions later... Btw, Andreas Abel and I have recently written a paper which uses Type:Type as an example of a partial type theory. We show that our type checker is sound and "partially complete", it will only fail to accept a welltyped term because there are diverging terms in the type derivation (http://www.cs.nott.ac.uk/~txa/publ/msfp08.pdf). This is only for beta, while there is an algorithm to typecheck Type:Type with beta-eta, I think even soundness is open for this case. Cheers, Thorsten 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 stefan at cs.uu.nl Thu Jun 26 12:32:52 2008 From: stefan at cs.uu.nl (Stefan Holdermans) Date: Thu, 26 Jun 2008 18:32:52 +0200 Subject: [TYPES] Universe Polymorphism In-Reply-To: <07C96242-85B8-4A76-A059-8C5B4F2EE190@cs.nott.ac.uk> References: <485E4E35.3010400@daimi.au.dk> <07C96242-85B8-4A76-A059-8C5B4F2EE190@cs.nott.ac.uk> Message-ID: Thorsten, > It seems to me that Type:Type is an honest form of impredicativity, > because at least you know that the system is inconsistent as a logic > (as opposed to System F where so far nobody has been able to show > this :-). Type:Type includes System F and the calculus of > constructions and I think all *reasonable* programs can be reformed > into Type(i):Type(i+1) possibly parametric in i. However, sometimes > you don't want to think about the levels initially and sort this out > later - i.e. use Type:Type. A similar attitude makes sense in > Mathematics, in particular Category Theory, where it is convenient to > worry about size conditions later... From a programmer's perspective: what can be said about the inferrability of universe polymorphism? I mean: it would be great if the programmer could just proceed as if Type:Type and have the compiler infer the correct indices, universe abstractions, and universe applications. Cheers, Stefan From txa at Cs.Nott.AC.UK Thu Jun 26 16:42:27 2008 From: txa at Cs.Nott.AC.UK (Thorsten Altenkirch) Date: Thu, 26 Jun 2008 21:42:27 +0100 Subject: [TYPES] Universe Polymorphism In-Reply-To: <76BBA19B-9F59-4C5D-A49B-CD69B452465D@cs.uu.nl> References: <485E4E35.3010400@daimi.au.dk> <07C96242-85B8-4A76-A059-8C5B4F2EE190@cs.nott.ac.uk> <76BBA19B-9F59-4C5D-A49B-CD69B452465D@cs.uu.nl> Message-ID: <8D410D07-2B5B-40FE-973E-EE9B72F6FC6C@Cs.Nott.AC.UK> Hi Stefan, > Thorsten, > >> It seems to me that Type:Type is an honest form of impredicativity, >> because at least you know that the system is inconsistent as a logic >> (as opposed to System F where so far nobody has been able to show >> this :-). Type:Type includes System F and the calculus of >> constructions and I think all *reasonable* programs can be reformed >> into Type(i):Type(i+1) possibly parametric in i. However, sometimes >> you don't want to think about the levels initially and sort this out >> later - i.e. use Type:Type. A similar attitude makes sense in >> Mathematics, in particular Category Theory, where it is convenient to >> worry about size conditions later... > > From a programmer's perspective: what can be said about the > inferrability of universe polymorphism? I mean: it would be great if > the programmer could just proceed as if Type:Type and have the > compiler infer the correct indices, universe abstractions, and > universe applications. Maybe a good starting point would be to answer the question what is the language of explicit universe polymorphism. Such a language should include at least abstraction and quantification over universe levels. Should the embedding from one universe into the next be implicit or explicit, i.e. do we want to have the rule A : Type(i) => A : Type(i+1)? While many trivial uses of universe levels may be inferable, I suspect that there may be situations where you want to have a "manual override". However, as far as know to find a good way to integrate explicit and implicit universe polymorphism is an open issue. Maybe somebody else can comment on this. Btw, in the context of Type Theory much larger universes have been investigated, e.g. Palmgren introduced "superuniverses" and Setzer the "Mahlo universe". These constructions may also have interesting applications in programming with dependent types. Cheers, Thorsten 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 uuomul at yahoo.com Wed Jun 25 16:20:30 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Wed, 25 Jun 2008 13:20:30 -0700 (PDT) Subject: [TYPES] the polymorphic lambda calculus - A related question concerning its uniformity Message-ID: <470014.76696.qm@web56104.mail.re3.yahoo.com> Consider a modification of the typing system for System F so that one deals with ground items only.? Namely, contexts are now lists t1 : A1,..., tn : An with the ti's ground terms and the Ai's ground types, and the typing system consists of the following (some of them infinitary) rules, where I use t,s for ground terms, x for term variables, A,B for ground types, p for arbitrary terms, D for arbitrary types, and X for type variables: ????? . ------------------------[t:A in Gamma]?? Gamma |-- t : A Gamma, t : A? |--? p[t/x] : B for all t --------------------------------------------------[FreeVars(p) included in {x}] Gamma? |--? lam x : A. p : A -> B Gamma? |--? p[A/X] : D[A/x] for all A ---------------------------------------------------[FreeVars(p) and FreeVars(D) included in {X}] Gamma |-- lam X. p : All X. D Gamma |-- t : A -> B???? Gamma |-- s : A ---------------------------------------------------------- Gamma |-- t s : B Gamma |-- t : All X. D ------------------------------------[FreeVars(D) included in {X}] Gamma |-- t [A] : D[A/X] It is easy to see that this ground type system is at least as powerful as the original system, in that any ground term typable in the empty context in the original system is also typable in the empty context in the above ground system.? Is the converse true? Thanks in advance, ?? Andrei --- On Wed, 6/11/08, types-list-request at lists.seas.upenn.edu wrote: From: types-list-request at lists.seas.upenn.edu Subject: Types-list Digest, Vol 46, Issue 2 To: types-list at lists.seas.upenn.edu Date: Wednesday, June 11, 2008, 4:49 PM Send Types-list mailing list submissions to types-list at lists.seas.upenn.edu To subscribe or unsubscribe via the World Wide Web, visit http://lists.seas.upenn.edu/mailman/listinfo/types-list or, via email, send a message with subject or body 'help' to types-list-request at lists.seas.upenn.edu You can reach the person managing the list at types-list-owner at lists.seas.upenn.edu When replying, please edit your Subject line so it is more specific than "Re: Contents of Types-list digest..." Today's Topics: 1. Re: Question about the polymorphic lambda calculus (Noam Zeilberger) 2. Re: Question about the polymorphic lambda calculus (Samuel E. Moelius III) 3. Re: Question about the polymorphic lambda calculus (Noam Zeilberger) 4. Re: Question about the polymorphic lambda calculus (Miles Sabin) 5. Re: Question about the polymorphic lambda calculus (Noam Zeilberger) 6. Re: Question about the polymorphic lambda calculus (Samuel E. Moelius III) 7. Re: Question about the polymorphic lambda calculus (Herman Geuvers) 8. Fwd: Revenue-neutral Adjustment for Functional Programming (Matthias Felleisen) 9. Paper announcement: Intersection types ? la Church (Luigi Liquori INRIA) ---------------------------------------------------------------------- Message: 1 Date: Tue, 3 Jun 2008 11:34:05 -0400 From: Noam Zeilberger Subject: Re: [TYPES] Question about the polymorphic lambda calculus To: "Samuel E. Moelius III" Cc: types-list at lists.seas.upenn.edu Message-ID: <20080603153403.GA22041 at cs.cmu.edu> Content-Type: text/plain; charset=us-ascii On Tue, Jun 03, 2008 at 06:38:13AM -0400, Samuel E. Moelius III wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, there is some term with type > T[U/X]. Then, does there necessarily exist some term with type (forall > X. T)? > > In other words, in the situation described above, can the meta-level > ``forall'' be pushed down into the types? I'm not sure these two questions are the same. As stated, I'm reading the first question as: Question 1 Suppose that T is a type with exactly one free variable X. Further suppose that for every closed type U, the type T[U/X] is inhabited. Then is the type (forall X.T) inhabited? But perhaps you mean something like so, which could more naturally be considered "pushing down the meta-level forall": Question 2 Suppose that T is a type with exactly one free variable X. Further suppose that for every closed type U, there is some term t_U with type T[U/X]. Then does there exist some term t with type (forall X. T), such that for all U, the terms t(U) and t_U are observationally equivalent? The answer to Q2 is no, in general. For a counterexample, suppose we have sum types T1+T2. If these aren't primitive, we can Church encode them (T1+T2 = forall Y.(T1->Y)->(T2->Y)->Y). Let T = 1+X, and define the term t_U of type 1+U as follows: inr(t') if there exists some t' : U t_U = inl() if U is uninhabited Now, there is only one inhabitant of the type (forall X.1+X), the term t = [X].inl(). But for inhabited types U, t(U) is not equivalent to t_U. If you drop the restriction that X appears exactly once in T, you can come up with even simpler counterexamples. For example, with T = bool (again, you can Church encode the booleans), take true if U = bool t*_U = false otherwise In fact, the restriction doesn't make a difference, because you can weaken T to X->bool and define t*_U appropriately as \x.true or \x.false. Is Q2 what you meant, or did you really mean Q1? Noam ------------------------------ Message: 2 Date: Tue, 3 Jun 2008 12:26:15 -0400 From: "Samuel E. Moelius III" Subject: Re: [TYPES] Question about the polymorphic lambda calculus To: Noam Zeilberger Cc: types-list at lists.seas.upenn.edu Message-ID: Content-Type: text/plain; charset=US-ASCII; format=flowed Noam, > I'm not sure these two questions are the same. As stated, I'm > reading the first question as: > > Question 1 > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, the type T[U/X] is inhabited. > Then is the type (forall X.T) inhabited? Yes, that's exactly what I meant. But your response to the alternative question was interesting and appreciated, nonetheless. :) Sam ------------------------------ Message: 3 Date: Wed, 4 Jun 2008 12:41:52 -0400 From: Noam Zeilberger Subject: Re: [TYPES] Question about the polymorphic lambda calculus To: "Samuel E. Moelius III" Cc: types-list at lists.seas.upenn.edu Message-ID: <20080604164152.GA23990 at cs.cmu.edu> Content-Type: text/plain; charset=us-ascii On Tue, Jun 03, 2008 at 12:26:15PM -0400, Samuel E. Moelius III wrote: > >Question 1 > > Suppose that T is a type with exactly one free variable X. Further > > suppose that for every closed type U, the type T[U/X] is inhabited. > > Then is the type (forall X.T) inhabited? > > Yes, that's exactly what I meant. Aha, sorry I assumed otherwise. I think the answer to Q1 is yes. Examine the single occurrence of X in T. Is it positive or negative? (Definition: X occurs positively in X; X occurs positively (neg.) in A->B if it occurs pos. (neg.) in B or neg. (pos.) in A.) Then define an instance T' of T as follows: T[bot/X] X occurs positively T' = T[top/X] X occurs negatively where top = forall Y.Y->Y and bot = forall Y.Y By assumption, T' is inhabited. From this it follows that T (and hence forall X.T) is inhabited, by the following pair of lemmas: Lemmas 1. If X occurs only positively in T, then [bot/X]T |- T, and if negatively then T |- [bot/X]T 2. If X occurs only positively in T, then T |- [top/X]T, and if negatively then [top/X]T |- T Proof: by induction on T. Do you buy that? It seems that the statement can be generalized to when T has multiple occurrences of X, but they are all either positive or negative. I am curious, though, of whether you know of any counterexamples when X occurs both positively and negatively in T? Noam ------------------------------ Message: 4 Date: Wed, 4 Jun 2008 18:28:27 +0100 From: "Miles Sabin" Subject: Re: [TYPES] Question about the polymorphic lambda calculus To: "Samuel E. Moelius III" Cc: types-list at lists.seas.upenn.edu Message-ID: <30961e500806041028w4573c84dyf5ca2390dc38005a at mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-1 On Tue, Jun 3, 2008 at 11:38 AM, Samuel E. Moelius III wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, there is some term with type > T[U/X]. Then, does there necessarily exist some term with type (forall > X. T)? > > In other words, in the situation described above, can the meta-level > ``forall'' be pushed down into the types? Maybe I'm missing something, but I would have thought that in general the answer has to be no: it doesn't follow from the fact that universal quantification is expressible in the meta-language that it's expressible in the object-language. Compare the analogous situation with first-order predicate calculus as the meta-language for first-order propositional calculus with countably infinite named constants and a finiteness constraint on proposition and proof length. Cheers, Miles ------------------------------ Message: 5 Date: Wed, 4 Jun 2008 13:37:59 -0400 From: Noam Zeilberger Subject: Re: [TYPES] Question about the polymorphic lambda calculus To: "Samuel E. Moelius III" Cc: types-list at lists.seas.upenn.edu Message-ID: <20080604173759.GA24128 at cs.cmu.edu> Content-Type: text/plain; charset=us-ascii On Wed, Jun 04, 2008 at 12:41:52PM -0400, Noam Zeilberger wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > On Tue, Jun 03, 2008 at 12:26:15PM -0400, Samuel E. Moelius III wrote: > > >Question 1 > > > Suppose that T is a type with exactly one free variable X. Further > > > suppose that for every closed type U, the type T[U/X] is inhabited. > > > Then is the type (forall X.T) inhabited? > > > > Yes, that's exactly what I meant. > > Aha, sorry I assumed otherwise. I think the answer to Q1 is yes. > Examine the single occurrence of X in T. Oops, it seems I read too much into the question again. Samuel did not state that T has a single occurrence of X, just that X is the single free type variable. Noam ------------------------------ Message: 6 Date: Thu, 05 Jun 2008 08:01:47 -0400 From: "Samuel E. Moelius III" Subject: Re: [TYPES] Question about the polymorphic lambda calculus To: Miles Sabin Cc: types-list at lists.seas.upenn.edu Message-ID: <4847D5AB.5020308 at cis.udel.edu> Content-Type: text/plain; charset="ISO-8859-1"; format=flowed Miles, > Maybe I'm missing something, but I would have thought that in general > the answer has to be no: it doesn't follow from the fact that > universal quantification is expressible in the meta-language that it's > expressible in the object-language. I appreciate your point. But this case is special in at least two respects: (1) the quantified statements are all of a certain form (i.e., there exists a term with a certain type), and (2) the object language is the polymorphic lambda calculus, specifically. For this special case, I think there is good reason to suspect that the universal quantifier can be expressed in the object language. Sam ------------------------------ Message: 7 Date: Fri, 06 Jun 2008 14:58:31 +0200 From: Herman Geuvers Subject: Re: [TYPES] Question about the polymorphic lambda calculus To: "Samuel E. Moelius III" , types-list at lists.seas.upenn.edu Message-ID: <48493477.6090801 at cs.ru.nl> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Samuel E. Moelius III wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Suppose that T is a type with exactly one free variable X. Further > suppose that for every closed type U, there is some term with type > T[U/X]. Then, does there necessarily exist some term with type (forall > X. T)? > > In other words, in the situation described above, can the meta-level > ``forall'' be pushed down into the types? > > If this is a theorem, could someone please point me to a proof of it? > > Thanks in advance. > > Sam Moelius > > Dear Sam, If I look at your question in the polymorphic lambda calculus (system F), then it is basically a question about derivability in second order proposition logic PROP2: Does the following hold? If |- Phi(U) for every closed proposition U, then |- forall X Phi(X) PROP2 is constructive proposition logic: only implication -> and a second order quantifier over propositions. Now, in the classical case, your conjecture holds, because then, if |- Phi(U) for every closed proposition U, then |- Phi(top) and |- Phi(bot) and so |- forall X. Phi(X). (In classical PROP2, let's call it CPROP2, we have an axiom forall X.(X \/ ~X); bot is forall X.X and top is forall X. X->X. The definition of the connectives is just the usual one from PROP2.) That |- Phi(top) and |- Phi(bot) imply |- forall X. Phi(X) is because we have a complete truth table semantics for CPROP2. I have spelled that out in detail in my PhD thesis in 1993. Now, can we conclude anything from this for PROP2? Yes, because there is a G"odel not-not translation from CPROP2 to PROP2. One can take the one from Coquand-Herbelin (called "A-translation" in their paper) or the "standard one" in the book of Van Dalen (Logic and Structure): Coquand-Herbelin: X* := X (A->B)* := ~~A* -> ~~B* (forall X.A)* := forall X. ~~A* van Dalen: X* := ~~X (A->B)* := A* -> B* (forall X.A)* := forall X. A* For the first one, we have Gamma |-_{CPROP2} phi <=> ~~(Gamma*) |- _{PROP2} ~~(phi*) For the second one, we have Gamma |-_{CPROP2} phi <=> Gamma* |- _{PROP2} phi* So if we consider the van Dalen translation, we can derive that for formulas of the form Phi(X)*, we have (in PROP2): If |- Phi(U)* for every closed proposition U, then |- forall X. Phi(X)* Proof: If |-_{PROP2} Phi(U)* for every closed proposition U, then |-_{PROP2} Phi(top)* and |-_{PROP2} Phi(bot)*, so |-_{CPROP2} Phi(top) and |-_{CPROP2} Phi(bot), so |-_{CPROP2} forall X. Phi(X), so |-_{PROP2} forall X. Phi(X)*. I have no idea to which extent this extends to the general case. Best Regards Herman Geuvers References: ======== My PhD thesis: J.H. Geuvers, Logics and Type systems , PhD. Thesis, University of Nijmegen, September 1993. http://www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz Thierry Coquand, Hugo Herbelin A-translation and Looping Combinators in Pure Type Systems, 1994, Journal of Functional Programming Dirk van Dalen Logic and Structure (3rd extended ed.). Springer Verlag, Berlin. ------------------------------ Message: 8 Date: Tue, 10 Jun 2008 09:34:43 -0400 From: Matthias Felleisen Subject: [TYPES] Fwd: Revenue-neutral Adjustment for Functional Programming To: types Message-ID: <2AB09C8E-B503-4BD9-98D1-22B2591BD234 at ccs.neu.edu> Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed This message is slightly off-topic, and apologies for that. I believe, however, that it is in the spirit of this list. The ACM Curriculum board has re-opened the 2001 design for review. Although ACM is a US-based organization, the curriculum is not only influential at the middle tier of US colleges and universities, it is also taken seriously by many evolving and developing educational institutions overseas. As you may recall, I alerted the readers of this list in the late 90s that the curriculum has relegated the study of PL and type systems to a peripheral status. We may now have an opening to make a small change. The ACM Curriculum board has agreed to consider a proposal on including FP as an equal to OOP (10 "hours" each) in the standard curriculum. See forwarded message below. This was the most concrete outcome of the PLC workshop at Harvard two weeks ago. (Stuart Reges, Shriram Krishnamurthi, and I drafted the proposal; Larry Snyder volunteered to submit it once the workshop expressed its unanimous support. The three of us came to the conclusion that only an inclusion of FP in the general curriculum will prepare students for properly designed though possibly optional PL courses, including a thorough study of type systems.) Please consider contributing comments to the web site. A simple "Yes, I think this is a great idea" will be helpful. A short explanation is even better. Thanks -- Matthias >> Begin forwarded message: >> >>> From: Larry Snyder >>> Date: June 9, 2008 6:58:43 PM EDT >>> To: PL-CURRC-WKSHP-INVITEES at LISTSERV.ACM.ORG >>> Subject: Revenue-neutral Adjustment for Functional Programming >>> Reply-To: Larry Snyder >>> >>> Colleagues: >>> >>> The ACM Education Board accepted our last minute input for adding >>> Functional Programming to the core of the revised CC2001-CS >>> curriculum, has posted our proposed changes on it's Web site >>> >>> http://wiki.acm.org/cs2001/index.php?title=SIGPLAN_Proposal >>> >>> and invited comments. Feel free to endorse our "revenue neutral" >>> workshop motion. (I quickly wrote the text in support of this for >>> use by the Ed Board, not expecting it to be included in the >>> posting; so apologies if I missed points or messed them up.) >>> Accordingly, crisp arguments for this change will doubtless be >>> helpful. -- LS >>> >> > ------------------------------ Message: 9 Date: Wed, 11 Jun 2008 12:12:38 +0200 From: Luigi Liquori INRIA Subject: [TYPES] Paper announcement: Intersection types ? la Church To: types at lists.chalmers.se, types-list at lists.seas.upenn.edu Cc: Luigi Liquori INRIA Message-ID: <52DF8FBA-7F2A-4BD0-8E77-9464FC131EB1 at sophia.inria.fr> Content-Type: text/plain; charset=UTF-8; delsp=yes; format=flowed I'm pleased to announce the available of a new paper on Intersection Types ? la Church: http://dx.doi.org/10.1016/j.ic.2007.03.005 http://www-sop.inria.fr/members/Luigi.Liquori/PAPERS/ic-07.pdf As always, comments and suggestions are welcome. Luigi Liquori and Simona Ronchi Della Rocca. Intersection-Types ? la Church by Luigi Liquori INRIA Sophia Antipolis, France Simona Ronchi Della Rocca Dipartimento di Informatica, Universit? di Torino, Italy Abstract In this paper, we present ?t?, a fully typed ?-calculus based on the intersection-type system discipline, which is a counterpart ? la Church of the type assignment system as invented by Coppo and Dezani. The relationship between ?t? and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable. Key words: Logics and Intersection-Types, ?-calculus ? la Curry and ? la Church -- Luigi Liquori, H.d.R., Ph.D. INRIA Researcher, Sophia Antipolis M?diterran?e LogNet Research Team Vox : +33 4 92 38 71 93 Fax : +33 4 92 38 79 71 Hom : +33 4 93 67 09 72 MobFr : +33 6 65 39 51 32 MobIt : +39 3 49 16 56 45 1 SIP : luigi_liquori at voip.wengo.fr Url : www-sop.inria.fr/members/Luigi.Liquori Url : www.inria.fr/recherche/equipes/lognet.en.html Email : Let (*,#)=(.,@) in Luigi*Liquori#inria*fr Addr : INRIA, 2004 Route des Lucioles - BP 93 FR-06902 Sophia Antipolis, France ? Pensez ? la plan?te et n'imprimez ce message que si n?cessaire ! Earth will kind ask you to print this message only if really needed! ? ------------------------------ _______________________________________________ Types-list mailing list Types-list at lists.seas.upenn.edu http://lists.seas.upenn.edu/mailman/listinfo/types-list End of Types-list Digest, Vol 46, Issue 2 ***************************************** From minari at unifi.it Mon Jun 30 07:28:29 2008 From: minari at unifi.it (Pierluigi Minari) Date: Mon, 30 Jun 2008 13:28:29 +0200 Subject: [TYPES] Confluence of combinatory strong reduction Message-ID: <002401c8daa4$6f1afaf0$0201a8c0@PC258022432669> We are pleased to announce our papers (presently under review in different Journals): - Ren? David, A direct proof of the confluence of combinatory strong reduction, - Pierluigi Minari, A solution to Curry and Hindley's problem on combinatory strong reduction, providing two different *direct* proofs of confluence for combinatory strong reduction, and so two different solutions to Curry and Hindley's problem dating back to 1958 --- see http://tlca.di.unito.it/opltlca/, Problem #1. Both papers can be downloaded from the links indicated at the TLCA-list webpage above. Ren? David, Pierluigi Minari Ren? David LAMA Universit? de Savoie david at univ-savoie.fr Pierluigi Minari Dipartimento di Filosofia Universit? di Firenze minari at unifi.it From brianh at cs.pdx.edu Tue Jul 22 19:04:24 2008 From: brianh at cs.pdx.edu (Brian Huffman) Date: Tue, 22 Jul 2008 16:04:24 -0700 Subject: [TYPES] ordering lemmas about powerdomain operations Message-ID: <20080722160424.yvgxvwdq1c8wccwg@webmail.pdx.edu> Hello all, I have been formalizing some properties of powerdomains and their operations in the Isabelle theorem prover. For example, one of the lemmas that I have proved is the following one about the upper powerdomain: xs + ys << {z} if and only if xs << {z} or ys << {z} where (+) is the binary union operation, {-} is the monadic unit or singleton, and (<<) is the information-ordering relation. Someone must have proved some ordering lemmas like this previously, but I haven't come across any in the papers I have looked at. Descriptions of upper or lower powerdomains usually mention that they are semilattices with the binary union acting as the meet or join; being a semilattice entails a bunch of lemmas about (+) alone, but doesn't say anything about properties of (+) combined with {-} as in my example above. Does anyone have a reference to a paper that proves (or even just lists) any of these ordering lemmas for powerdomains? - Brian Huffman From brianh at cs.pdx.edu Thu Jul 24 21:23:10 2008 From: brianh at cs.pdx.edu (Brian Huffman) Date: Thu, 24 Jul 2008 18:23:10 -0700 Subject: [TYPES] ordering lemmas about powerdomain operations In-Reply-To: <20080724095513.GA12290@mathematik.tu-darmstadt.de> References: <20080722160424.yvgxvwdq1c8wccwg@webmail.pdx.edu> <20080724095513.GA12290@mathematik.tu-darmstadt.de> Message-ID: <20080724182310.xx1gotn98ys8cc00@webmail.pdx.edu> Quoting Thomas Streicher : > The lemma you mention is obvious from the way how the Smyth (i.e. > upper) powerdomin > is constructed, namely as nonempty compact upward closed subsets of > the domain > ordered by \supseteq. From this it is trivial. > Moreover one has in the Smyth powerdomain x \sqsubseteq y if x \cup y = x. > > Information about powerdomains can be found in the respective papers > by Plotkin > and Smyth from the 70ies. > You might want to have a look at > > http://homepages.inf.ed.ac.uk/gdp/publications/Domains.ps > > for example. > > Thomas I'm not sure that I am familiar with the construction of the upper powerdomain that you describe, unless you are referring to the construction of Smyth powerdomains over flat element types from the linked paper. I failed to specify in my original question, but I am interested in element types that are arbitrary omega-bifinite domains. In my formalization I construct three varieties of powerdomains using ideal completion, with a basis Pfin(K(a)) consisting of nonempty finite sets of compact elements, as described in Abramsky and Jung (1994) and elsewhere. For the upper powerdomain, the preorder relation is xs << ys == forall y in ys, exists x in xs, such that x << y. That is, everything in ys is above something in xs. From this definition it is indeed obvious that the following property holds for elements of the *basis*, where (+) is ordinary set-union and {-} is the singleton set: xs + ys << {z} if and only if xs << {z} or ys << {z} However, I am more interested in the version of this lemma for the completed powerdomain, where (+) and {-} refer to the continuous extensions of the union and singleton operations on the basis. Some properties (like xs + ys << xs, or xs + ys = ys + xs) are easy to transfer from the basis to the ideal completion, since they are admissible predicates in either variable. However, a property like (xs + ys << {z} --> xs << {z} or ys << {z}) is not an admissible predicate, because it has an implication. The only proof I could find is rather tricky, and relies on the underlying element type being bifinite. Here is the full list of other (seemingly-obvious) lemmas that required a similar trick to prove: {x} << ys + zs iff {x} << ys or {x} << zs (lower) {x} << ys + zs iff {x} << ys and {x} << zs (convex) xs + ys << {z} iff xs << {z} and ys << {z} (convex) {x} << {y} iff x << y (upper, lower, and convex) Of course, it is entirely possible that these have much easier proofs that I just failed to find. Alternatively, using a different construction besides ideal completion might yield easier proofs of these properties, but I have only seen such an alternative construction for the lower powerdomain (described in the Plotkin notes you linked, as well as the Wikipedia "Power domains" article). - Brian From brianh at metamilk.com Mon Aug 25 21:55:05 2008 From: brianh at metamilk.com (Brian Hulley) Date: Tue, 26 Aug 2008 02:55:05 +0100 Subject: [TYPES] Typing extensible records without row variables? Message-ID: <48B36279.1050804@metamilk.com> Hi, Many of the papers I've read that deal with the typing of extensible records use the concept of "row variables" ([1] [2] [3] [4]). Therefore if we use the syntax(*): 'val r = {[title = "Duma"] [genre = Drama]} to bind a record with 2 fields to (r) and {[certificate = U] :: r} to denote the extension of (r) by a new field, with row variables the extension operator has type: {[_ : _] :: _} : 'forall (l : LABEL) (t : *) (r : ROW) . Lab[l] -> t -> Rec[r] -> Rec{| [l : t] :: r |} where {| [l : t] :: r |} denotes the row r extended by the label/type association, and (Rec) is a built-in type constructor of kind (ROW -> *). (Curried application is denoted by glued square brackets which can be omitted if the argument is itself a bracketed form, and keywords always start with a prime.) For brevity the above can be written: {[_ : _] :: _} : Lab[l] t Rec[r] -> Rec{| [l : t] :: r |} | [l : LABEL] [t : *] [r : ROW] where the postfix bar/square brackets are just an alternative way of introducing universally quantified variables so that the interesting "shape" part of the type can be written (and read) first, and the function has an arity (as in Clean) so there is only one arrow. Some record systems only allow one occurrence of any given label per record, which is represented by a "lacks" predicate, which ensures that the row does not already contain the specified label: {[_ : _] :: _} : Lab[l] t Rec[r] -> Rec{| [l : t] :: r |} | [l : LABEL] [t : *] [r : ROW] Lacks[l r] Now my question is: suppose instead of using a row variable we simply used a normal type variable (of kind *) but used a *predicate* to restrict this type variable to the subset of (*) which are records: {[_ : _] :: _} : Lab[l] t r -> { [l : t] :: r } | [l : LABEL] [t r : *] Record[r] Lacks[l r] The point of doing this is that it gives (to my mind) a much more intuitive type for the extension operation: we no longer need to explicitly lift a row into a record using (Rec) or deal with the extra concept at all. Also, just as with (Lacks) predicates, the presence of the (Record) predicate could often be deduced from the shape of the type and therefore would often not need to be written explicitly by the programmer. Of course one justification for breaking down the record concept into row + lift-to-record is that a variant can be represented by row + lift-to-variant and hence there is the possiblity to turn records into variants and vice versa at the term level ([1] 6.1). However to my mind there are several fundamental differences between records and variants in terms of how they are used in practical programming languages: 1) For variants it is important that the compiler can issue exhaustiveness warnings whereas for a record it doesn't matter if there are extra fields that are not needed by an operation. 2) To use variants in practice (e.g. in patterns) a syntax like would be far too verbose and therefore the mainstream functional languages use curried constructors (Haskell) or 0/1 constructors (SML) (which the implementation may or may not try to optimize by turning a constructor that takes one tuple of arity n into a constructor of arity n by erasing the tuple behind the scenes). However if we choose to use curried constructors as in Haskell the type associated with each variant label would have to be a "lifted tuple" (i.e. a tuple which is regarded as a container of zero or more elements so that a 1-tuple is not the same as the value itself) since we need to be able to distinguish between a function of arity one whose argument is a pair, and a function of arity two. Therefore the row corresponding to a variant would always have to be of a specific form and so there could not be free interchange between records and variants. 3) While it is obviously useful to have extensible records it is not at all clear to me whether or not extensible variants are similarly useful since there are other ways of achieving extensiblility in functional programming e.g. by adding new combinators to a combinator library and keeping the underlying representation variant completely hidden. In any case the question of interchange between records and variants seems to be orthogonal to the question of whether rows need to be represented explicitly in the type system, since we could simply use built-in predicates and operations like: plus-elim : 'record-to[a r] v -> a | a r v Record[r] Variant[v] EqRV[r v] where EqRV[r v] ensures that each label in record type (r) is associated with the same type as the corresponding label in variant type (v), and that the set of labels in (r) and (v) is the same, i.e. it replaces the need to explicitly construct (r) and (v) from the same row variable. (This is my translation of (plusElim) from ([1] 6.1), and the prime before the "record-to" helps to emphasize that this is a built-in type function.) Anyway since the separate concept of row variable is so ubiquitous in the literature, and since I have not so far seen (Record) or (Variant) predicates used instead, I would be very interested to know if there's any other reason for using row variables that is not covered by the above, or if I'm missing something important, or if anyone else has had the same idea. Thanks, Brian. [1] " A Polymorphic Type System for Extensible Records and Variants" Benedict R. Gaster and Mark P. Jones [2] "Lightweight Extensible Records for Haskell" Mark P. Jones and Simon Peyton Jones [3] "First-class labels for extensible rows" Daan Leijen [4] "Extensible records with scoped labels" Daan Leijen (*) This is the comma-free(! :-)) syntax I've developed for the language I'm working on. From blume at tti-c.org Mon Aug 25 23:40:34 2008 From: blume at tti-c.org (Matthias Blume) Date: Mon, 25 Aug 2008 22:40:34 -0500 Subject: [TYPES] Typing extensible records without row variables? In-Reply-To: <48B36279.1050804@metamilk.com> References: <48B36279.1050804@metamilk.com> Message-ID: <9F1106F5-E376-4708-98E0-F36E3F3AE277@tti-c.org> On Aug 25, 2008, at 8:55 PM, Brian Hulley wrote: > 3) While it is obviously useful to have extensible records it is not > at > all clear to me whether or not extensible variants are similarly > useful > since there are other ways of achieving extensiblility in functional > programming e.g. by adding new combinators to a combinator library and > keeping the underlying representation variant completely hidden. In our ICFP'06 paper[*] we suggest that extensible variants (actually: extensible cases) might be a useful programming concept that integrates gracefully into an ML- (or Haskell-) like language after all. ou might also be interested in having a look at our upcoming APLAS paper[**], where we point out that the same idea not only straightforwardly extends to the typing of exceptions (a fact that has been exploited several times in previous work on exception analysis by other authors), but also can be taken as a starting point for a language design that (a) rules out any uncaught exceptions, and (b) integrates well with the notion of extensible records and cases. Matthias [*] Extensible Programming with First-Class Cases. Matthias Blume, Umut A. Acar and Wonseok Chae. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP'06). Portland, Oregon. Sep 18-20, 2006. [**] Exception Handlers as Extensible Cases. Matthias Blume, Umut A. Acar, and Wonseok Chae. To appear in Proceedings of the Sixth ASIAN Symposium on Programming Languages and Systems (APLAS 2008). Bangalore, India, Dec 9-11, 2008. An expanded version is available as University of Chicago CS Technical Report TR-2008-03. From brianh at metamilk.com Tue Aug 26 08:48:59 2008 From: brianh at metamilk.com (Brian Hulley) Date: Tue, 26 Aug 2008 13:48:59 +0100 Subject: [TYPES] Typing extensible records without row variables? In-Reply-To: <9F1106F5-E376-4708-98E0-F36E3F3AE277@tti-c.org> References: <48B36279.1050804@metamilk.com> <9F1106F5-E376-4708-98E0-F36E3F3AE277@tti-c.org> Message-ID: <48B3FBBB.6010806@metamilk.com> Matthias Blume wrote: > > On Aug 25, 2008, at 8:55 PM, Brian Hulley wrote: > >> 3) While it is obviously useful to have extensible records it is not at >> all clear to me whether or not extensible variants are similarly useful >> since there are other ways of achieving extensiblility in functional >> programming e.g. by adding new combinators to a combinator library and >> keeping the underlying representation variant completely hidden. > > In our ICFP'06 paper[*] we suggest that extensible variants (actually: > extensible cases) might be a useful programming concept that integrates > gracefully into an ML- (or Haskell-) like language after all. Thanks - I found the above useful especially for the way extensible variants are given meaning at the term level by splitting the usual case construct into match + cases and making the cases part the first class dual of extensible records. Also of special interest is the fact that the "lacks" predicates of various other papers I'd read are directly incorporated into the kind of the row variable so that everything is dealt with in the same place instead of being represented by a special kind *and* a special predicate, and of course the details of how all this is implemented efficiently, and some other points too. In terms of integration, if these variants are to replace the normal non-extensible datatype variants of ML/Haskell, there is still (afaics) the issue of syntactic convenience vs theoretical completeness of the duality due to the fact that the extensible variant constructors must each take exactly one argument yet the programmer would probably prefer to avoid having to supply "redundant" units, and on the other hand, if one were to also keep the normal datatypes then there would be two sorts of variant in the language. (Of course perhaps this is just a minor inconvenience compared with the advantages of extensible cases.) > > ou might also be interested in having a look at our upcoming APLAS > paper[**], where we point out that the same idea not only > straightforwardly extends to the typing of exceptions (a fact that has > been exploited several times in previous work on exception analysis by > other authors), but also can be taken as a starting point > for a language design that (a) rules out any uncaught exceptions, and > (b) integrates well with the notion of extensible records and cases. > > Matthias > > [*] Extensible Programming with First-Class Cases. > Matthias Blume, Umut A. Acar and Wonseok Chae. > In Proceedings of the 11th ACM SIGPLAN International Conference on > Functional Programming (ICFP'06). > Portland, Oregon. Sep 18-20, 2006. > > [**] Exception Handlers as Extensible Cases. > Matthias Blume, Umut A. Acar, and Wonseok Chae. > To appear in Proceedings of the Sixth ASIAN Symposium on > Programming Languages and Systems (APLAS 2008). > Bangalore, India, Dec 9-11, 2008. > An expanded version is available as University of Chicago CS > Technical Report TR-2008-03. > Thanks also for the second reference, Brian. From m.schellekens at cs.ucc.ie Tue Sep 2 05:43:21 2008 From: m.schellekens at cs.ucc.ie (Michel Schellekens) Date: Tue, 02 Sep 2008 10:43:21 +0100 Subject: [TYPES] New book/please advertise on Types List Message-ID: <48BD0AB9.4000609@cs.ucc.ie> Hello, could the following new Springer book please be advertised on the types list? Best wishes, Michel Schellekens New Springer book on static modular average-case analysis. The following new Springer book addresses the fundamental problem of compositional static timing of software, with a focus on average-case analysis. The book also outlines (informal) typing for the new language, based on random bags. http://www.springer.com/computer/foundations/book/978-0-387-73383-8 A Modular Calculus for the Average Cost of Data Structuring Schellekens, Michel 2008, XXIV, 246 p. 20 illus. With CD-ROM., Hardcover ISBN: 978-0-387-73383-8 A Modular Calculus for the Average Cost of Data Structuring introduces MOQA, a new domain-specific programming language which guarantees the average-case time analysis of its programs to be modular. "Time" in this context refers to a broad notion of cost, which can be used to estimate the actual running time, but also other quantitative information such as power consumption, while modularity means that the average time of a program can be easily computed from the times of its constituents--something that no programming language of this scope has been able to guarantee so far. MOQA principles can be incorporated in any standard programming language. MOQA supports tracking of data and their distributions throughout computations, based on the notion of random bag preservation. This allows a unified approach to average-case time analysis, and resolves fundamental bottleneck problems in the area. The main techniques are illustrated in an accompanying Flash tutorial, where the visual nature of this method can provide new teaching ideas for algorithms courses. This volume, with forewords by Greg Bollella and Dana Scott, presents novel programs based on the new advances in this area, including the first randomness-preserving version of Heapsort. Programs are provided, along with derivations of their average-case time, to illustrate the radically different approach to average-case timing. The automated static timing tool applies the Modular Calculus to extract the average-case running time of programs directly from their MOQA code. A Modular Calculus for the Average Cost of Data Structuring is designed for a professional audience composed of researchers and practitioners in industry, with an interest in algorithmic analysis and also static timing and power analysis--areas of growing importance. It is also suitable as an advanced-level text or reference book for students in computer science, electrical engineering and mathematics. Michel Schellekens obtained his PhD from Carnegie Mellon University, following which he worked as a Marie Curie Fellow at Imperial College London. Currently he is an Associate Professor at the Department of Computer Science in University College Cork - National University of Ireland, Cork, where he leads the Centre for Efficiency-Oriented Languages (CEOL) as a Science Foundation Ireland Principal Investigator. Written for: Researchers and students interested in algorithm analysis, static analysis, real-time programming, programming language semantics Keywords: * random structures * real-time languages * series-parallel data structures * software timing/power analysis * sorting and search algorithms * static analysis -- Prof. M. P. Schellekens Science Foundation Ireland Investigator Director of Centre for Efficiency-Oriented Languages (CEOL) National University of Ireland, Cork (UCC) Department of Computer Science Center for Efficiency-Oriented Languages (CEOL) Lancaster Hall Little Hanover Street 6 Cork, Ireland WWW: http://www.ceol.ucc.ie/ Tel. + 353 (0)21 490 1917 From swarat at cse.psu.edu Thu Sep 4 09:13:55 2008 From: swarat at cse.psu.edu (Swarat Chaudhuri) Date: Thu, 04 Sep 2008 09:13:55 -0400 Subject: [TYPES] POPL logo design contest Message-ID: <48BFDF13.7050306@cse.psu.edu> Dear POPL community members: We know that you are all holding your breath for POPL 2009; here's some diversion to take your mind off the wait. We are planning to select a logo for POPL---after all, if the Olympics can have one, why not us? Accordingly, we announce the first-ever Contest on POPL Logo Design and Implementation (not to be confused with the other, gentler PLDI). Participants should send submissions in jpg, gif or png formats to Swarat Chaudhuri (swarat at cse.psu.edu) by November 20, 2008. The submission should contain: 1) A logo that doesn't mention the year (e.g., 2010) of the conference. 2) Logos mentioning the years 2010, 2011, and 2012. The contest will be judged by: * Luca Cardelli (Microsoft Cambridge) * Benjamin Pierce (Penn) * Shriram Krishnamurthi (Brown) We do not currently need high-resolution images, but will request them from the winner(s). From 2010 on, the logo will appear on POPL's webpage---in addition to the winning logo, the POPL 2010 webpage will also link to any other logo the judges find noteworthy. The winner(s) and runners-up will be presented t-shirts and cookies during the PC Chair's presentation at POPL 2009. So here's to citius, altius, etc. Get your design juices flowing! Best, Swarat Chaudhuri (Penn State) Publicity chair POPL 2010-2012 From michael.lienhardt at inrialpes.fr Tue Sep 9 04:59:25 2008 From: michael.lienhardt at inrialpes.fr (Michael Lienhardt) Date: Tue, 9 Sep 2008 10:59:25 +0200 Subject: [TYPES] Reference to typed first class pattern matching Message-ID: Hello, I was wondering if there was any existing work on typed first class pattern matching. Typically, I have a ML-like calculus with abstraction of the form $ \lambda P.e$, were $P$ is a pattern matching for instance type constructors and tuples. Moreover, one can combine abstraction like in $\lambda P.e + \lambda P'.e'$, thus assembling pattern matching branches dynamically. One can also define a function $\lambda g.\lambda f.(f + g)$: we have first class pattern matching. I am interested to type such a calculus, using for instance intersection types to deal with the $+$ constructor. Is there any previous work on first class pattern matching that can help me design such a type system ? Michael Lienhardt PhD student. From devriese at cs.tcd.ie Tue Sep 9 09:29:08 2008 From: devriese at cs.tcd.ie (Edsko de Vries) Date: Tue, 9 Sep 2008 14:29:08 +0100 Subject: [TYPES] Reference to typed first class pattern matching In-Reply-To: References: Message-ID: <20080909132908.GA6367@netsoc.tcd.ie> On Tue, Sep 09, 2008 at 10:59:25AM +0200, Michael Lienhardt wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello, > > I was wondering if there was any existing work on typed first class > pattern matching. > > Typically, I have a ML-like calculus with abstraction of the form $ > \lambda P.e$, were $P$ is a pattern matching for instance type > constructors and tuples. > Moreover, one can combine abstraction like in $\lambda P.e + \lambda > P'.e'$, thus assembling pattern matching branches dynamically. > One can also define a function $\lambda g.\lambda f.(f + g)$: we have > first class pattern matching. > > I am interested to type such a calculus, using for instance > intersection types to deal with the $+$ constructor. > Is there any previous work on first class pattern matching that can > help me design such a type system ? This kind of thing can be done with extensible records: A polymorphic type system for extensible records and variants (1996) by Benedict R. Gaster, Mark P. Jones See also: Extensible records with scoped labels. [bib, pdf] Daan Leijen. The 2005 Symposium on Trends in Functional Programming (TFP'05), Tallin, Estonia, September 2005. Also published in the 3rd volume of Trends in Functional Programming. Edsko From blume at tti-c.org Tue Sep 9 09:50:11 2008 From: blume at tti-c.org (Matthias Blume) Date: Tue, 9 Sep 2008 08:50:11 -0500 Subject: [TYPES] Reference to typed first class pattern matching In-Reply-To: References: Message-ID: Hi Michael, this might not be as general as you would like, but our ICFP'06 paper on first-class cases goes in that direction. Some of the things you seem to be after can be coded up in that system: Extensible Programming with First-Class Cases. Matthias Blume, Umut A. Acar and Wonseok Chae. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP'06). Portland, Oregon. Sep 18-20, 2006. The type system is based straightforwardly on Remy-style row polymorphism, here applied to sums. It is also quite closely related to polymorphic variants as found in OCaml. (However, one crucial difference is that in OCaml one cannot extend a match without knowing what is being extended. If I am guessing correctly, this probably means that OCaml-style polymorphic variants won't work for you.) Matthias On Sep 9, 2008, at 3:59 AM, Michael Lienhardt wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hello, > > I was wondering if there was any existing work on typed first class > pattern matching. > > Typically, I have a ML-like calculus with abstraction of the form $ > \lambda P.e$, were $P$ is a pattern matching for instance type > constructors and tuples. > Moreover, one can combine abstraction like in $\lambda P.e + \lambda > P'.e'$, thus assembling pattern matching branches dynamically. > One can also define a function $\lambda g.\lambda f.(f + g)$: we have > first class pattern matching. > > I am interested to type such a calculus, using for instance > intersection types to deal with the $+$ constructor. > Is there any previous work on first class pattern matching that can > help me design such a type system ? > > Michael Lienhardt > PhD student. From eduardo at sol.lifia.info.unlp.edu.ar Wed Sep 10 15:13:59 2008 From: eduardo at sol.lifia.info.unlp.edu.ar (eduardo@sol.lifia.info.unlp.edu.ar) Date: Wed, 10 Sep 2008 16:13:59 -0300 Subject: [TYPES] Reference to typed first class pattern matching In-Reply-To: References: Message-ID: <20080910161359.7lwxqymkros0844s@webmail.lifia.info.unlp.edu.ar> Dear Micheal, There are a number of references that are related to your question and that you might find useful (listed in no particular order): 1) Old (1990) work by Vincent van Oostrom on a lambda calculus allowing one to abstract over arbitrary terms ("Lambda calculus with patterns"). Untyped setting. [1] 2) Previous work revised and extended (joint with Klop and De Vrijer)[2] 3) Work by Gilles Barthe et al on PTS with patterns [3] 4) Work of Barry Jay on his Bondi programming language (see his homepage) 5) Delia Kesner and Barry Jay's First-Class Patterns (see Delia Kesner's homepage) 6) The rho calculus (see Horatiu Cirstea's homepage) Regards, E. [1] Vincent van Oostrom Lambda Calculus with Patterns Technical Report IR-228, Vrije Universiteit, Amsterdam, 40 pages, November 1990 [2] Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer Lambda Calculus with Patterns Theoretical Computer Science, Volume 398, Issues 1-3, 28 May 2008, pages 16-31, Elsevier [3] Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori: Pure patterns type systems. POPL 2003: 250-261 Quoting Michael Lienhardt : > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello, > > I was wondering if there was any existing work on typed first class > pattern matching. > > Typically, I have a ML-like calculus with abstraction of the form $ > \lambda P.e$, were $P$ is a pattern matching for instance type > constructors and tuples. > Moreover, one can combine abstraction like in $\lambda P.e + \lambda > P'.e'$, thus assembling pattern matching branches dynamically. > One can also define a function $\lambda g.\lambda f.(f + g)$: we have > first class pattern matching. > > I am interested to type such a calculus, using for instance > intersection types to deal with the $+$ constructor. > Is there any previous work on first class pattern matching that can > help me design such a type system ? > > Michael Lienhardt > PhD student. > ---------------------------------------------------------------- Este mensaje ha sido enviado utilizando IMP desde LIFIA. From wadler at inf.ed.ac.uk Thu Sep 11 05:23:22 2008 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Thu, 11 Sep 2008 10:23:22 +0100 Subject: [TYPES] Reference to typed first class pattern matching In-Reply-To: <20080910161359.7lwxqymkros0844s@webmail.lifia.info.unlp.edu.ar> References: <20080910161359.7lwxqymkros0844s@webmail.lifia.info.unlp.edu.ar> Message-ID: <6BEF5033-86D0-4CC1-B9E5-7500F9EA50F7@inf.ed.ac.uk> Another work that may be relevant is: Noam Zeilberger: Focusing and higher-order abstract syntax. POPL 2008: 359-369 Yours, -- P On 10 Sep 2008, at 20:13, eduardo at sol.lifia.info.unlp.edu.ar wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > Dear Micheal, > > There are a number of references that are related to your > question and that you might find useful (listed in no particular > order): > > 1) Old (1990) work by Vincent van Oostrom on a lambda calculus > allowing one to abstract over arbitrary terms ("Lambda calculus with > patterns"). Untyped setting. [1] > 2) Previous work revised and extended (joint with Klop and De > Vrijer)[2] > 3) Work by Gilles Barthe et al on PTS with patterns [3] > 4) Work of Barry Jay on his Bondi programming language (see > his homepage) > 5) Delia Kesner and Barry Jay's First-Class Patterns (see Delia > Kesner's homepage) > 6) The rho calculus (see Horatiu Cirstea's homepage) > > Regards, > E. > > > [1] Vincent van Oostrom > Lambda Calculus with Patterns > Technical Report IR-228, Vrije Universiteit, Amsterdam, 40 pages, > November 1990 > > [2] Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer > Lambda Calculus with Patterns > Theoretical Computer Science, Volume 398, Issues 1-3, 28 May 2008, > pages 16-31, Elsevier > > [3] Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori: > Pure patterns type systems. POPL 2003: 250-261 > > > Quoting Michael Lienhardt : > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ >> types-list ] >> >> Hello, >> >> I was wondering if there was any existing work on typed first class >> pattern matching. >> >> Typically, I have a ML-like calculus with abstraction of the form $ >> \lambda P.e$, were $P$ is a pattern matching for instance type >> constructors and tuples. >> Moreover, one can combine abstraction like in $\lambda P.e + \lambda >> P'.e'$, thus assembling pattern matching branches dynamically. >> One can also define a function $\lambda g.\lambda f.(f + g)$: we have >> first class pattern matching. >> >> I am interested to type such a calculus, using for instance >> intersection types to deal with the $+$ constructor. >> Is there any previous work on first class pattern matching that can >> help me design such a type system ? >> >> Michael Lienhardt >> PhD student. >> > > > > ---------------------------------------------------------------- > Este mensaje ha sido enviado utilizando IMP desde LIFIA. > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. From uuomul at yahoo.com Tue Oct 14 00:24:03 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Mon, 13 Oct 2008 21:24:03 -0700 (PDT) Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus Message-ID: <836074.37017.qm@web56102.mail.re3.yahoo.com> Apologies for asking an untyped question on a typed forum. :) Assume (pure) untyped lambda calculus under beta reduction (and the infix notation for application associates to the left as usual). I would like to know if there exists a set A of strongly normalizing terms such that the following holds: For all terms T, [T is in A] iff [the term T T_1 ... T_n is strongly normalizing for all natural numbers n and terms T_1,...,T_n in A] I do not even know where to start for trying to construct such a set (a greatest fixed point definition is not possible, since the property is contravariant). Or is there any obvious (or known) reason for why such a set could not exist? Thank you in advance for any hint on this, Andrei Popescu From robin at cs.rhul.ac.uk Wed Oct 15 11:01:05 2008 From: robin at cs.rhul.ac.uk (Robin Adams) Date: Wed, 15 Oct 2008 16:01:05 +0100 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: <836074.37017.qm@web56102.mail.re3.yahoo.com> References: <836074.37017.qm@web56102.mail.re3.yahoo.com> Message-ID: <200810151601.05720.robin@cs.rhul.ac.uk> On Tuesday 14 October 2008 05:24:03 Andrei Popescu wrote: > > I would like to know if there exists a set A of strongly normalizing terms > such that the following holds: > > For all terms T, > [T is in A] > iff > [the term T T_1 ... T_n is strongly normalizing > for all natural numbers n and terms T_1,...,T_n in A] There cannot be such a set. Proof: Suppose A satisfies the conditions above. For any T_1, ..., T_n in A, we have T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. Therefore, \x.xx is in A. Therefore, (\x.xx)(\x.xx) is strongly normalizing. This is a contradiction. -- Robin Adams Royal Holloway, University of London From dezani at di.unito.it Thu Oct 16 04:00:11 2008 From: dezani at di.unito.it (Mariangiola Dezani) Date: Thu, 16 Oct 2008 10:00:11 +0200 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: <836074.37017.qm@web56102.mail.re3.yahoo.com> References: <836074.37017.qm@web56102.mail.re3.yahoo.com> Message-ID: > For all terms T, > [T is in A] > iff > [the term T T_1 ... T_n is strongly normalizing > for all natural numbers n and terms T_1,...,T_n in A] a strict subset of A is the set PSN of persistently strongly normalizing terms defined by [T is in PSN] iff [the term T T_1 ... T_n is strongly normalizing for all natural numbers n and strongly normalizing terms T_1,...,T_n] The set PSN has been characterised (also with types) in: M. Tatsuta and M. Dezani-Ciancaglini. Normalisation is Insensible to Lambda-term Identity or Difference, LICS'06. In Rajeev Alur ed(s)., pages 327-336, 2006, IEEE Computer Society. http://www.di.unito.it/ ?dezani/papers/td.pdf Characterisations of other sets of lambda terms related to normalization properties can be found in: M. Dezani-Ciancaglini, F. Honsell and Y. Motohama. Compositional Characterization of ?-terms using Intersection Types, Theoretical Computer Science, 340(3):459-495, 2005. http://www.di.unito.it/~dezani/papers/tcsf.pdf Best Regards Mariangiola Dezani @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Mariangiola Dezani-Ciancaglini Dipartimento di Informatica Universita' di Torino c.Svizzera 185, 10149 Torino (Italy) e-mail : dezani at di.unito.it phone: 39-011-6706850 fax : 39-011-751603 mobile: 39-320-4359903 (preferred) 39-348-2251592 http://www.di.unito.it/~dezani ********************************************************************** Unless unavoidable, no Word, Excel or PowerPoint attachments, please. See http://www.gnu.org/philosophy/no-word-attachments.html ********************************************************************** "L'ITALIA RIPUDIA LA GUERRA come strumento di offesa alla libert? degli altri popoli e come mezzo di risoluzione delle controversie internazionali." (Art. 11 della Costituzione della Repubblica Italiana) From Luigi.Liquori at sophia.inria.fr Thu Oct 16 09:43:08 2008 From: Luigi.Liquori at sophia.inria.fr (Luigi.Liquori@work) Date: Thu, 16 Oct 2008 15:43:08 +0200 Subject: [TYPES] Reference to typed first class pattern matching Message-ID: Dear Michael, The Typed Rewriting calculus can be one possible reference. http://rho.loria.fr/ Best Luigi ----------------- Luigi Liquori, H.d.R., Ph.D. INRIA Researcher, Sophia Antipolis M?diterran?e LogNet Research Team Vox : +33 4 92 38 71 93 Fax : +33 4 92 38 50 29 Hom : +33 4 93 67 09 72 GsmWork : +33 6 78 35 80 88 GsmPerso1 : +33 6 65 39 51 32 GsmPerso2 : +39 3 49 16 56 45 1 SIP : luigi_liquori at voip.wengo.fr Url : www-sop.inria.fr/members/Luigi.Liquori Url : www.inria.fr/recherche/equipes/lognet.en.html Email : Let (*,#)=(.,@) in Luigi*Liquori#inria*fr Snailm : INRIA, 2004 Route des Lucioles - BP 93 FR-06902 Sophia Antipolis, France ? Pensez ? la plan?te et n'imprimez ce message que si n?cessaire ! Earth will kind ask you to print this message only if really needed! ? From jonathan.seldin at uleth.ca Thu Oct 16 15:32:50 2008 From: jonathan.seldin at uleth.ca (Jonathan Seldin) Date: Thu, 16 Oct 2008 13:32:50 -0600 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: <200810151601.05720.robin@cs.rhul.ac.uk> References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> Message-ID: I think this proof is invalid. The inference > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). > Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. seems to use the inference If M reduces to N and N is SN, so is M. This is false. Consider (\uv.u)(\x.x)((\z.zz)(\z.zz)). This term is clearly not SN, but it reduces to (\x.x), which is SN (and is, in fact, in normal form). On 15-Oct-08, at 9:01 AM, Robin Adams wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > On Tuesday 14 October 2008 05:24:03 Andrei Popescu wrote: >> >> I would like to know if there exists a set A of strongly >> normalizing terms >> such that the following holds: >> >> For all terms T, >> [T is in A] >> iff >> [the term T T_1 ... T_n is strongly normalizing >> for all natural numbers n and terms T_1,...,T_n in A] > > There cannot be such a set. > > Proof: Suppose A satisfies the conditions above. For any T_1, ..., > T_n in A, > we have > > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). > Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. > Therefore, \x.xx is in A. > Therefore, (\x.xx)(\x.xx) is strongly normalizing. > > This is a contradiction. > > -- > Robin Adams > Royal Holloway, University of London > 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 rendel at daimi.au.dk Thu Oct 16 18:01:51 2008 From: rendel at daimi.au.dk (Tillmann Rendel) Date: Fri, 17 Oct 2008 00:01:51 +0200 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> Message-ID: <48F7B9CF.4090609@daimi.au.dk> Jonathan Seldin wrote: > I think this proof is invalid. The inference > >> T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). >> Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. > > seems to use the inference > > If M reduces to N and N is SN, so is M. > > This is false. Consider > > (\uv.u)(\x.x)((\z.zz)(\z.zz)). > > This term is clearly not SN, but it reduces to (\x.x), which is SN > (and is, in fact, in normal form). I don't think this is a problem here. Since T_1, T_2 ... T_n are SN, every reduction strategy will reduce (1) (\x.xx) T_1 T_2 ... T_n in a finite number of steps to a term of the form (2) U_1 U_1 U_2 ... U_n with T_i reduces to U_i. On the other hand, the SN term (3) T_1 T_1 T_2 ... T_n reduces to (2), so (2) must be SN. Now, if every reduction strategy reduces (1) to a SN term, (1) is SN itself. Tillmann Rendel From dreyer at mpi-sws.mpg.de Fri Oct 17 03:29:07 2008 From: dreyer at mpi-sws.mpg.de (Derek Dreyer) Date: Fri, 17 Oct 2008 09:29:07 +0200 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> Message-ID: <7fa251b70810170029t4d6b7d38re4696f22e14f9759@mail.gmail.com> Actually, Jonathan, I'm pretty sure this proof step is perfectly valid, but the lemma you were assuming it depended on is too strong. The appropriate one to use is the "head expansion" lemma: If P[Q/x] T_2 ... T_n is SN, and Q is SN, then (\x.P) Q T_2 ... T_n is SN. Instantiate P = xx, and Q = T_1. Derek On Thu, Oct 16, 2008 at 9:32 PM, Jonathan Seldin wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I think this proof is invalid. The inference > >> T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). >> Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. > > seems to use the inference > > If M reduces to N and N is SN, so is M. > > This is false. Consider > > (\uv.u)(\x.x)((\z.zz)(\z.zz)). > > This term is clearly not SN, but it reduces to (\x.x), which is SN > (and is, in fact, in normal form). > > On 15-Oct-08, at 9:01 AM, Robin Adams wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> ] >> >> On Tuesday 14 October 2008 05:24:03 Andrei Popescu wrote: >>> >>> I would like to know if there exists a set A of strongly >>> normalizing terms >>> such that the following holds: >>> >>> For all terms T, >>> [T is in A] >>> iff >>> [the term T T_1 ... T_n is strongly normalizing >>> for all natural numbers n and terms T_1,...,T_n in A] >> >> There cannot be such a set. >> >> Proof: Suppose A satisfies the conditions above. For any T_1, ..., >> T_n in A, >> we have >> >> T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). >> Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. >> Therefore, \x.xx is in A. >> Therefore, (\x.xx)(\x.xx) is strongly normalizing. >> >> This is a contradiction. >> >> -- >> Robin Adams >> Royal Holloway, University of London >> > > 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 regnier at iml.univ-mrs.fr Fri Oct 17 08:29:13 2008 From: regnier at iml.univ-mrs.fr (Laurent Regnier) Date: Fri, 17 Oct 2008 14:29:13 +0200 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> Message-ID: <48F88519.9040708@iml.univ-mrs.fr> Hello, > The inference > >> > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). >> > Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. > > seems to use the inference > > If M reduces to N and N is SN, so is M. > > This is false. Actually this is false in general but true in the case investigated here. More precisely Adams implicitely uses a standard result in lambda-calculus theory, sometimes known as the strict lemma, that states that: If M reduces to N by a *strict* reduction (involving no K-redex) and if N is SN then so is M. This is proved in a form or another by various authors (Barendregt, Danos, De Vrijer, Tortora, ...); I have a proof of it in my 1994 TCS paper "Une ?quivalence sur les lambda-termes" (the paper is in french). I can't find another precise reference at the moment but certainly somebody on this list may provide one. I therefore believe Adam's argument is correct; I furthermore found it elegant and concise, I wish I had found it myself! Laurent Regnier --------------- (1) Precisely the strict lemma used by Adams is that: From pierre.hyvernat at univ-savoie.fr Fri Oct 17 08:37:34 2008 From: pierre.hyvernat at univ-savoie.fr (Pierre Hyvernat) Date: Fri, 17 Oct 2008 14:37:34 +0200 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> Message-ID: <20081017123734.GA12139@d53.lama.univ-savoie.fr> Hello. Someone else is bound to have answered before my message gets through, but here we go: > I think this proof is invalid. The inference > > > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). Hence > > (\x.xx)T_1 T_2 ... T_n is strongly normalizing. > > seems to use the inference > > If M reduces to N and N is SN, so is M. > > As you pointed out, this is false; but the proof doesn't use this. It relies on the following general observation: if M[x:=N] N1 ... Nk is SN and if N is SN then (\x.M) N N1 ... Nk is also SN (This is true.) Pierre -- Real programmers don't comment their code. It was hard to write, it should be hard to understand. From regnier at iml.univ-mrs.fr Fri Oct 17 10:51:53 2008 From: regnier at iml.univ-mrs.fr (Laurent Regnier) Date: Fri, 17 Oct 2008 16:51:53 +0200 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: <48F88519.9040708@iml.univ-mrs.fr> References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> <48F88519.9040708@iml.univ-mrs.fr> Message-ID: <48F8A689.7080201@iml.univ-mrs.fr> > I have a proof of it in my 1994 TCS paper "Une ?quivalence sur les > lambda-termes". Sorry, I've been tricked by my memory, my paper proves a similar result but not the strict lemma. A correct reference is Barendregt's book "The lambda-calculus" where it is called the "Conservation theorem" (chapter 13 "Reduction strategies", in section 4 "An effective perpetual strategy"). Laurent Regnier From mir at itu.dk Fri Oct 17 16:07:22 2008 From: mir at itu.dk (Morten Rhiger) Date: Fri, 17 Oct 2008 22:07:22 +0200 Subject: [TYPES] Reference to typed first class pattern matching In-Reply-To: <6BEF5033-86D0-4CC1-B9E5-7500F9EA50F7@inf.ed.ac.uk> References: <20080910161359.7lwxqymkros0844s@webmail.lifia.info.unlp.edu.ar> <6BEF5033-86D0-4CC1-B9E5-7500F9EA50F7@inf.ed.ac.uk> Message-ID: <34e60ef30810171307m4f224851tfdc70ceabee5b3d9@mail.gmail.com> In an article that is going to appear as a Functional Pearl in the Journal of Functional Programming, I present a library of typed first class pattern combinators implemented in Haskell. Using this library, one can, among other things, construct both or-patterns and clauses dynamically, so the $+$ that Michael wants is within reach. The article is available at http://www.itu.dk/people/mir/typesafepatterns.pdf -- Morten On Thu, Sep 11, 2008 at 11:23 AM, Philip Wadler wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Another work that may be relevant is: > > Noam Zeilberger: Focusing and higher-order abstract syntax. POPL > 2008: 359-369 > > Yours, -- P > > On 10 Sep 2008, at 20:13, eduardo at sol.lifia.info.unlp.edu.ar wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ >> types-list ] >> >> Dear Micheal, >> >> There are a number of references that are related to your >> question and that you might find useful (listed in no particular >> order): >> >> 1) Old (1990) work by Vincent van Oostrom on a lambda calculus >> allowing one to abstract over arbitrary terms ("Lambda calculus with >> patterns"). Untyped setting. [1] >> 2) Previous work revised and extended (joint with Klop and De >> Vrijer)[2] >> 3) Work by Gilles Barthe et al on PTS with patterns [3] >> 4) Work of Barry Jay on his Bondi programming language (see >> his homepage) >> 5) Delia Kesner and Barry Jay's First-Class Patterns (see Delia >> Kesner's homepage) >> 6) The rho calculus (see Horatiu Cirstea's homepage) >> >> Regards, >> E. >> >> >> [1] Vincent van Oostrom >> Lambda Calculus with Patterns >> Technical Report IR-228, Vrije Universiteit, Amsterdam, 40 pages, >> November 1990 >> >> [2] Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer >> Lambda Calculus with Patterns >> Theoretical Computer Science, Volume 398, Issues 1-3, 28 May 2008, >> pages 16-31, Elsevier >> >> [3] Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori: >> Pure patterns type systems. POPL 2003: 250-261 >> >> >> Quoting Michael Lienhardt : >> >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ >>> types-list ] >>> >>> Hello, >>> >>> I was wondering if there was any existing work on typed first class >>> pattern matching. >>> >>> Typically, I have a ML-like calculus with abstraction of the form $ >>> \lambda P.e$, were $P$ is a pattern matching for instance type >>> constructors and tuples. >>> Moreover, one can combine abstraction like in $\lambda P.e + \lambda >>> P'.e'$, thus assembling pattern matching branches dynamically. >>> One can also define a function $\lambda g.\lambda f.(f + g)$: we have >>> first class pattern matching. >>> >>> I am interested to type such a calculus, using for instance >>> intersection types to deal with the $+$ constructor. >>> Is there any previous work on first class pattern matching that can >>> help me design such a type system ? >>> >>> Michael Lienhardt >>> PhD student. >>> >> >> >> >> ---------------------------------------------------------------- >> Este mensaje ha sido enviado utilizando IMP desde LIFIA. >> > > > -- > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > > ________________________________ Morten Rhiger http://www.itu.dk/people/mir/ From jonathan.seldin at uleth.ca Fri Oct 17 16:22:18 2008 From: jonathan.seldin at uleth.ca (Jonathan Seldin) Date: Fri, 17 Oct 2008 14:22:18 -0600 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: <48F7B9CF.4090609@daimi.au.dk> References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> <48F7B9CF.4090609@daimi.au.dk> Message-ID: Yes, as Tillman Rendel and a number of others have written (some to me alone and some to the Types list), Robin Adams proof is, in fact, correct. It does not require the lemma I thought it required, but a weaker one that is valid. The proof is valid, and, as somebody wrote, it is, indeed, very elegant. On 16-Oct-08, at 4:01 PM, Tillmann Rendel wrote: > Jonathan Seldin wrote: >> I think this proof is invalid. The inference >>> T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A). >>> Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing. >> seems to use the inference >> If M reduces to N and N is SN, so is M. >> This is false. Consider >> (\uv.u)(\x.x)((\z.zz)(\z.zz)). >> This term is clearly not SN, but it reduces to (\x.x), which is SN >> (and is, in fact, in normal form). > > I don't think this is a problem here. Since T_1, T_2 ... T_n are SN, > every reduction strategy will reduce > > (1) (\x.xx) T_1 T_2 ... T_n > > in a finite number of steps to a term of the form > > (2) U_1 U_1 U_2 ... U_n > > with T_i reduces to U_i. On the other hand, the SN term > > (3) T_1 T_1 T_2 ... T_n > > reduces to (2), so (2) must be SN. Now, if every reduction strategy > reduces (1) to a SN term, (1) is SN itself. > > Tillmann Rendel 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 eduardo at sol.lifia.info.unlp.edu.ar Fri Oct 17 16:50:13 2008 From: eduardo at sol.lifia.info.unlp.edu.ar (eduardo@sol.lifia.info.unlp.edu.ar) Date: Fri, 17 Oct 2008 18:50:13 -0200 Subject: [TYPES] questiuon about strong normalization in untyped lambda-calculus In-Reply-To: <20081017123734.GA12139@d53.lama.univ-savoie.fr> References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> <20081017123734.GA12139@d53.lama.univ-savoie.fr> Message-ID: <20081017185013.evmnft9icggswos8@webmail.lifia.info.unlp.edu.ar> >> > As you pointed out, this is false; but the proof doesn't use this. > It relies on the following general observation: > > if M[x:=N] N1 ... Nk is SN and if N is SN > then (\x.M) N N1 ... Nk is also SN > > (This is true.) You, of course, require x to occur free in M. This is an example of a perpetual reduction step (contrapositive reading of the above): 1) M has an infinite reduction sequence 2) M -> N implies N has an infinite reduction sequence. Perpetual strategies for arbitrary orthogonal higher-order rewrite systems (thus including beta) have been studied in: Zurab Khasidashvili, Mizuhito Ogawa, and Vincent van Oostrom Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems Information and Computation, Volume 164, pp. 118 - 151, 2001 How to use perpetual strategies for inductively characterizing the set of SN terms has been given here: Femke van Raamsdonk, Paula Severi, Morten Heine S?rensen, Hongwei Xi: Perpetual Reductions in Lambda-Calculus. Inf. Comput. 149(2): 173-225 (1999) Regards, E. Disclaimer: These references are stated merely as starting points. You should consult the references they cite for further pointers. ---------------------------------------------------------------- Este mensaje ha sido enviado utilizando IMP desde LIFIA. From eduardo at sol.lifia.info.unlp.edu.ar Fri Oct 17 16:58:48 2008 From: eduardo at sol.lifia.info.unlp.edu.ar (eduardo@sol.lifia.info.unlp.edu.ar) Date: Fri, 17 Oct 2008 18:58:48 -0200 Subject: [TYPES] Errata In-Reply-To: <20081017185013.evmnft9icggswos8@webmail.lifia.info.unlp.edu.ar> References: <836074.37017.qm@web56102.mail.re3.yahoo.com> <200810151601.05720.robin@cs.rhul.ac.uk> <20081017123734.GA12139@d53.lama.univ-savoie.fr> <20081017185013.evmnft9icggswos8@webmail.lifia.info.unlp.edu.ar> Message-ID: <20081017185848.bsbbgguresgs88k0@webmail.lifia.info.unlp.edu.ar> Quoting eduardo at sol.info.unlp.edu.ar: >>> >> As you pointed out, this is false; but the proof doesn't use this. >> It relies on the following general observation: >> >> if M[x:=N] N1 ... Nk is SN and if N is SN >> then (\x.M) N N1 ... Nk is also SN >> >> (This is true.) > > You, of course, require x to occur free in M. > Oops! Didn't notice the "and if N is SN". Sorry. E. ---------------------------------------------------------------- Este mensaje ha sido enviado utilizando IMP desde LIFIA. From David.Teller at ens-lyon.org Tue Oct 21 06:38:41 2008 From: David.Teller at ens-lyon.org (David Rajchenbach-Teller) Date: Tue, 21 Oct 2008 12:38:41 +0200 Subject: [TYPES] Looking for a type system Message-ID: <1224585521.6334.13.camel@Blefuscu> Dear list, I've been working for a few months on a type system for applied system security. I've started with dependent types and progressively managed to trim it down to something which, with a few simplifications, has the following grammar: T ::= T -> T | P (primitive type) | forall a T (polymorphism) | a (type variable) | K(T) (constructor) | T union T (set union) Now, I'd say that all of the above is very common stuff except for the union (let me stress that this is set union, not disjoint union). As that construction seems quite natural, I cannot help but assume that such a type system has been amply studied. Could anyone help me put a name on that type system so that I can look for some literature? Thanks, David, Who already feels foolish for asking, because the answer is bound to be somewhere on the lambda-cube or so -- David Teller-Rajchenbach Security of Distributed Systems http://www.univ-orleans.fr/lifo/Members/David.Teller Angry researcher: French Universities need reforms, but the LRU act brings liquidations. -- David Teller-Rajchenbach Security of Distributed Systems http://www.univ-orleans.fr/lifo/Members/David.Teller Angry researcher: French Universities need reforms, but the LRU act brings liquidations. From dezani at di.unito.it Tue Oct 21 10:58:56 2008 From: dezani at di.unito.it (Mariangiola Dezani) Date: Tue, 21 Oct 2008 16:58:56 +0200 Subject: [TYPES] Looking for a type system In-Reply-To: <1224585521.6334.13.camel@Blefuscu> References: <1224585521.6334.13.camel@Blefuscu> Message-ID: You can look at F. Barbanera, M. Dezani-Ciancaglini and U. de' Liguoro. Intersection and Union Types: Syntax and Semantics, Information and Computation, 119:202-230, 1995. and the references there. Regards Mariangiola @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Mariangiola Dezani-Ciancaglini Dipartimento di Informatica Universita' di Torino c.Svizzera 185, 10149 Torino (Italy) e-mail : dezani at di.unito.it phone: 39-011-6706850 fax : 39-011-751603 mobile: 39-320-4359903 (preferred) 39-348-2251592 http://www.di.unito.it/~dezani ********************************************************************** Unless unavoidable, no Word, Excel or PowerPoint attachments, please. See http://www.gnu.org/philosophy/no-word-attachments.html ********************************************************************** "L'ITALIA RIPUDIA LA GUERRA come strumento di offesa alla libert? degli altri popoli e come mezzo di risoluzione delle controversie internazionali." (Art. 11 della Costituzione della Repubblica Italiana) From david.hopwood at industrial-designers.co.uk Tue Oct 21 18:38:49 2008 From: david.hopwood at industrial-designers.co.uk (David-Sarah Hopwood) Date: Tue, 21 Oct 2008 23:38:49 +0100 Subject: [TYPES] Looking for a type system In-Reply-To: References: <1224585521.6334.13.camel@Blefuscu> Message-ID: <48FE59F9.4020707@industrial-designers.co.uk> Mariangiola Dezani wrote: > You can look at > > F. Barbanera, M. Dezani-Ciancaglini and U. de' Liguoro. Intersection > and Union Types: Syntax and Semantics, Information and > Computation, 119:202-230, 1995. > > and the references there. Also Giuseppe Castagna, Alain Frisch A Gentle Introduction to Semantic Subtyping -- David-Sarah Hopwood From gc at pps.jussieu.fr Wed Oct 22 03:29:05 2008 From: gc at pps.jussieu.fr (gc@pps.jussieu.fr) Date: Wed, 22 Oct 2008 09:29:05 +0200 Subject: [TYPES] Looking for a type system In-Reply-To: <48FE59F9.4020707@industrial-designers.co.uk> References: <1224585521.6334.13.camel@Blefuscu> <48FE59F9.4020707@industrial-designers.co.uk> Message-ID: <48FED641.1060505@pps.jussieu.fr> David-Sarah Hopwood wrote: > > Also > > Giuseppe Castagna, Alain Frisch > A Gentle Introduction to Semantic Subtyping > > Indeed. The reference above is, as the title goes, a gentle introduction that avoids technicalities as much as possible. It is the right reference to have an idea of the general framework. For the full story and gory details please refer to: A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, vol.?55, n.?4, pag.?1?64, 2008. http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf which contains the previous reference. For polymorphism ... we are working on it: few key theorems still missing :-( In the meanwhile if missing T->T is not a concern you can check this work by Hosoya (mainly) H. Hosoya, A. Frisch, and G. Castagna: Parametric Polymorphism for XML. In POPL?'05, 32nd ACM Symposium on Principles of Programming Languages, pag.?50-62, ACM Press, 2005. http://www.pps.jussieu.fr/~gc/papers/popl05.pdf ---Beppe--- P.S. For the very few persons who may be interested, please notice that http://www.di.ens.fr/users/castagna no longer is my home page. I moved two years ago: http://www.pps.jussieu.fr/~gc From cbj at it.uts.edu.au Thu Oct 23 03:11:33 2008 From: cbj at it.uts.edu.au (Barry Jay) Date: Thu, 23 Oct 2008 09:11:33 +0200 Subject: [TYPES] Looking for a type system In-Reply-To: <48FED641.1060505@pps.jussieu.fr> References: <1224585521.6334.13.camel@Blefuscu> <48FE59F9.4020707@industrial-designers.co.uk> <48FED641.1060505@pps.jussieu.fr> Message-ID: <490023A5.6000303@it.uts.edu.au> Hi Beppe, it's good to know that you are still working on sub-typing. I've finished drafting the book, including some improvements to my sub-typed calculus, so it will come out some time next year (early, I hope!) I still have your XML paper to hand, and hope to get to it soon. When are you coming to Sydney? Best, Barry gc at pps.jussieu.fr wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > David-Sarah Hopwood wrote: > >> Also >> >> Giuseppe Castagna, Alain Frisch >> A Gentle Introduction to Semantic Subtyping >> >> >> > > Indeed. The reference above is, as the title goes, a gentle introduction that > avoids technicalities as much as possible. It is the right reference to have an > idea of the general framework. For the full story and gory details please refer to: > > A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping: dealing > set-theoretically with function, union, intersection, and negation types. > Journal of the ACM, vol.?55, n.?4, pag.?1?64, 2008. > http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf > > which contains the previous reference. > > For polymorphism ... we are working on it: few key theorems still missing :-( > > In the meanwhile if missing T->T is not a concern you can check this work by > Hosoya (mainly) > > H. Hosoya, A. Frisch, and G. Castagna: Parametric Polymorphism for XML. In > POPL?'05, 32nd ACM Symposium on Principles of Programming Languages, pag.?50-62, > ACM Press, 2005. > http://www.pps.jussieu.fr/~gc/papers/popl05.pdf > > > ---Beppe--- > > P.S. For the very few persons who may be interested, please notice that > http://www.di.ens.fr/users/castagna no longer is my home page. I moved two years > ago: http://www.pps.jussieu.fr/~gc > > From David.Teller at ens-lyon.org Fri Oct 24 10:44:50 2008 From: David.Teller at ens-lyon.org (David Rajchenbach-Teller) Date: Fri, 24 Oct 2008 16:44:50 +0200 Subject: [TYPES] Looking for a type system In-Reply-To: <1224585521.6334.13.camel@Blefuscu> References: <1224585521.6334.13.camel@Blefuscu> Message-ID: <1224859490.6390.39.camel@Blefuscu> Thank you all for the references. Cheers, David On Tue, 2008-10-21 at 12:38 +0200, David Rajchenbach-Teller wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear list, > > I've been working for a few months on a type system for applied system > security. I've started with dependent types and progressively managed to > trim it down to something which, with a few simplifications, has the > following grammar: -- David Teller-Rajchenbach Security of Distributed Systems http://www.univ-orleans.fr/lifo/Members/David.Teller Angry researcher: French Universities need reforms, but the LRU act brings liquidations. From joshua.dunfield at gmail.com Fri Oct 24 23:44:33 2008 From: joshua.dunfield at gmail.com (Joshua Dunfield) Date: Fri, 24 Oct 2008 23:44:33 -0400 Subject: [TYPES] Looking for a type system In-Reply-To: <1224859490.6390.39.camel@Blefuscu> References: <1224585521.6334.13.camel@Blefuscu> <1224859490.6390.39.camel@Blefuscu> Message-ID: 2008/10/24 David Rajchenbach-Teller : > On Tue, 2008-10-21 at 12:38 +0200, David Rajchenbach-Teller wrote: [inquiring about a type system with union types] Belatedly: You may also be interested in my dissertation, which describes a type system with unions (and intersections). The type system itself might not be exactly what you're looking for, but the references may be useful even so. http://www.cs.cmu.edu/~joshuad/papers/thesis/ Best, -j. From stefan at cs.uu.nl Fri Nov 7 03:24:29 2008 From: stefan at cs.uu.nl (Stefan Holdermans) Date: Fri, 7 Nov 2008 09:24:29 +0100 Subject: [TYPES] Minimal type reconstruction Message-ID: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> Hi all, One way to look at type inference in Hindley-Milner-like disciplines is not just as the problem of finding a principal type scheme for a term in a given type environment, but as the problem of reconstructing an explicitly typed term in the style of System F that corresponds to such a principal type scheme. As an obvious example, consider the "completion" of the implicitly typed polymorphic identity function ?x. x , resulting in the explicitly typed ??. ?x : ?. x . Typically, type inference for Hindley-Milner-like systems proceeds by assigning each let-bound variable its principal type. For example, completion of let id = ?x. x in id 2 + id 3 ni yields let id = ??. ?x : ?. x in id [?] 2 + id [?] 3 ni . However, in this particular example the type abstraction in the definition of id and, hence, the type applications in the body of the local definition are unnecessary; another perfectly valid completion would be let id = ?x : ?. x in id 2 + id 3 ni . That is, if a let-bound variable is not used polymorphically, we may just as well infer a monomorphic type for it. In some specific situations, such a "minimal" completion may even be preferable over a fully polymorphic one. (Looking through a Curry-Howard lens, we are after the "simplest" proofs.) Although I'm quite sure it has been considered before, I have not found any discussion in literature of the problem of finding minimal completions. Can anyone on this list provide me with pointers to such discussions? Thanks in advance, Stefan Holdermans From josefs at chalmers.se Fri Nov 7 10:06:08 2008 From: josefs at chalmers.se (Josef Svenningsson) Date: Fri, 7 Nov 2008 16:06:08 +0100 Subject: [TYPES] Minimal type reconstruction In-Reply-To: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> References: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> Message-ID: <8dde104f0811070706g7635c717i5bc1fc9c7ff5d7e@mail.gmail.com> See: Minimal typing derivations Nikolaj Skallerud Bj?rner http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9102 Josef On Fri, Nov 7, 2008 at 9:24 AM, Stefan Holdermans wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi all, > > One way to look at type inference in Hindley-Milner-like disciplines > is not just as the problem of finding a principal type scheme for a > term in a given type environment, but as the problem of reconstructing > an explicitly typed term in the style of System F that corresponds to > such a principal type scheme. As an obvious example, consider the > "completion" of the implicitly typed polymorphic identity function > > ?x. x , > > resulting in the explicitly typed > > ??. ?x : ?. x . > > Typically, type inference for Hindley-Milner-like systems proceeds by > assigning each let-bound variable its principal type. For example, > completion of > > let id = ?x. x in id 2 + id 3 ni > > yields > > let id = ??. ?x : ?. x in id [?] 2 + id [?] 3 ni . > > However, in this particular example the type abstraction in the > definition of id and, hence, the type applications in the body of the > local definition are unnecessary; another perfectly valid completion > would be > > let id = ?x : ?. x in id 2 + id 3 ni . > > That is, if a let-bound variable is not used polymorphically, we may > just as well infer a monomorphic type for it. In some specific > situations, such a "minimal" completion may even be preferable over a > fully polymorphic one. (Looking through a Curry-Howard lens, we are > after the "simplest" proofs.) Although I'm quite sure it has been > considered before, I have not found any discussion in literature of > the problem of finding minimal completions. Can anyone on this list > provide me with pointers to such discussions? > > Thanks in advance, > > Stefan Holdermans From akenn at microsoft.com Fri Nov 7 10:06:38 2008 From: akenn at microsoft.com (Andrew Kennedy) Date: Fri, 7 Nov 2008 15:06:38 +0000 Subject: [TYPES] Minimal type reconstruction In-Reply-To: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> References: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> Message-ID: <8E144E0A808A2A4AA6940401CD70C57415AEB5FE75@EA-EXMSG-C332.europe.corp.microsoft.com> Hi Stefan I think that "Minimal Typing Derivations", N Bjorner, ACM Workshop on ML and its Applications, 1994 is probably what you're after. (Should be on citeseer but I don't seem to get access right now). Cheers Andrew. -----Original Message----- From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Stefan Holdermans Sent: 07 November 2008 08:24 To: types-list at lists.seas.upenn.edu Subject: [TYPES] Minimal type reconstruction [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hi all, One way to look at type inference in Hindley-Milner-like disciplines is not just as the problem of finding a principal type scheme for a term in a given type environment, but as the problem of reconstructing an explicitly typed term in the style of System F that corresponds to such a principal type scheme. As an obvious example, consider the "completion" of the implicitly typed polymorphic identity function ?x. x , resulting in the explicitly typed ??. ?x : ?. x . Typically, type inference for Hindley-Milner-like systems proceeds by assigning each let-bound variable its principal type. For example, completion of let id = ?x. x in id 2 + id 3 ni yields let id = ??. ?x : ?. x in id [?] 2 + id [?] 3 ni . However, in this particular example the type abstraction in the definition of id and, hence, the type applications in the body of the local definition are unnecessary; another perfectly valid completion would be let id = ?x : ?. x in id 2 + id 3 ni . That is, if a let-bound variable is not used polymorphically, we may just as well infer a monomorphic type for it. In some specific situations, such a "minimal" completion may even be preferable over a fully polymorphic one. (Looking through a Curry-Howard lens, we are after the "simplest" proofs.) Although I'm quite sure it has been considered before, I have not found any discussion in literature of the problem of finding minimal completions. Can anyone on this list provide me with pointers to such discussions? Thanks in advance, Stefan Holdermans From Didier.Remy at inria.fr Fri Nov 7 10:30:58 2008 From: Didier.Remy at inria.fr (Didier Remy) Date: Fri, 07 Nov 2008 16:30:58 +0100 Subject: [TYPES] Minimal type reconstruction In-Reply-To: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> References: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> Message-ID: <49145F32.5010306@inria.fr> > That is, if a let-bound variable is not used polymorphically, we may > just as well infer a monomorphic type for it. In some specific > situations, such a "minimal" completion may even be preferable over a > fully polymorphic one. (Looking through a Curry-Howard lens, we are > after the "simplest" proofs.) Although I'm quite sure it has been > considered before, I have not found any discussion in literature of > the problem of finding minimal completions. Can anyone on this list > provide me with pointers to such discussions? Dear Stefan, I think that this is exactly the problem studied by Nikolaj Bjorner in the case of ML in his paper "Minimal Typing Deriviations" presented at the ML workshop in 1994 [http://theory.stanford.edu/people/nikolaj/ml-work94.ps] Best wishes, Didier From gmb at microsoft.com Fri Nov 7 10:35:14 2008 From: gmb at microsoft.com (Gavin Bierman) Date: Fri, 7 Nov 2008 15:35:14 +0000 Subject: [TYPES] Minimal type reconstruction In-Reply-To: <8E144E0A808A2A4AA6940401CD70C57415AEB5FE75@EA-EXMSG-C332.europe.corp.microsoft.com> References: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> <8E144E0A808A2A4AA6940401CD70C57415AEB5FE75@EA-EXMSG-C332.europe.corp.microsoft.com> Message-ID: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9102 Gavin -----Original Message----- From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Andrew Kennedy Sent: 07 November 2008 15:07 To: 'Stefan Holdermans'; types-list at lists.seas.upenn.edu Subject: Re: [TYPES] Minimal type reconstruction [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hi Stefan I think that "Minimal Typing Derivations", N Bjorner, ACM Workshop on ML and its Applications, 1994 is probably what you're after. (Should be on citeseer but I don't seem to get access right now). Cheers Andrew. -----Original Message----- From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Stefan Holdermans Sent: 07 November 2008 08:24 To: types-list at lists.seas.upenn.edu Subject: [TYPES] Minimal type reconstruction [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hi all, One way to look at type inference in Hindley-Milner-like disciplines is not just as the problem of finding a principal type scheme for a term in a given type environment, but as the problem of reconstructing an explicitly typed term in the style of System F that corresponds to such a principal type scheme. As an obvious example, consider the "completion" of the implicitly typed polymorphic identity function ?x. x , resulting in the explicitly typed ??. ?x : ?. x . Typically, type inference for Hindley-Milner-like systems proceeds by assigning each let-bound variable its principal type. For example, completion of let id = ?x. x in id 2 + id 3 ni yields let id = ??. ?x : ?. x in id [?] 2 + id [?] 3 ni . However, in this particular example the type abstraction in the definition of id and, hence, the type applications in the body of the local definition are unnecessary; another perfectly valid completion would be let id = ?x : ?. x in id 2 + id 3 ni . That is, if a let-bound variable is not used polymorphically, we may just as well infer a monomorphic type for it. In some specific situations, such a "minimal" completion may even be preferable over a fully polymorphic one. (Looking through a Curry-Howard lens, we are after the "simplest" proofs.) Although I'm quite sure it has been considered before, I have not found any discussion in literature of the problem of finding minimal completions. Can anyone on this list provide me with pointers to such discussions? Thanks in advance, Stefan Holdermans From stefan at cs.uu.nl Sat Nov 8 03:47:45 2008 From: stefan at cs.uu.nl (Stefan Holdermans) Date: Sat, 8 Nov 2008 09:47:45 +0100 Subject: [TYPES] Minimal type reconstruction In-Reply-To: <49146BD4.3020505@cs.ru.nl> References: <83CFC4DF-7E8B-4854-9B36-A4A334805C32@cs.uu.nl> <49146BD4.3020505@cs.ru.nl> Message-ID: <84D33E99-8BEC-40F9-BD71-17EC78BE9514@cs.uu.nl> Josef, Andrew, Didier, Gavin, and Christian, I asked: > I have not found any discussion in literature of the problem of > finding minimal completions. Can anyone on this list provide me > with pointers to such discussions? Thank you so much for your very helpful answers; I will look into the papers you mentioned. Cheers, Stefan From uuomul at yahoo.com Wed Nov 12 14:26:36 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Wed, 12 Nov 2008 11:26:36 -0800 (PST) Subject: [TYPES] HOAS versus meta reasoning Message-ID: <720364.67916.qm@web56102.mail.re3.yahoo.com> Dear Type Theorists and Practioners, I would like to know what is the state of the art in taming the interaction between HOAS (higher order abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions. (I am aware of some of the work, but very probably I am not aware of the latest progress.) Thank you in advance, Andrei Popescu From andrew.gacek at gmail.com Wed Nov 12 16:36:00 2008 From: andrew.gacek at gmail.com (Andrew Gacek) Date: Wed, 12 Nov 2008 15:36:00 -0600 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <720364.67916.qm@web56102.mail.re3.yahoo.com> References: <720364.67916.qm@web56102.mail.re3.yahoo.com> Message-ID: Hi Andrei, There has been research on this topic for over a decade, begun by Dale Miller and Ray McDowell (who picked up on earlier work by Peter Schroeder-Heister and Girard), continued by Alwen Tiu and Dale Miller and now including several others like David Baelde, Gopalan Nadathur and myself. There is also a system called Abella (http://abella.cs.umn.edu) that incorporates this style of reasoning. Some of the highlights of this research are: * Reasoning with higher-order abstract syntax in a logical framework, by Raymond McDowell and Dale Miller (ToCL 2002). In this paper McDowell and Miller present a logic with HOAS, recursive definitions, and natural number induction. Using this logic they are able to prove various theorems such as subject reduction for the lambda calculus, but in each theorem when they use the inductive hypothesis, they do so on closed HOAS terms. The reason is that they have trouble encoding the free variables in a logical way. * A proof theory for generic judgments, by Dale Miller and Alwen Tiu (LICS 2005), and A logical framework for reasoning about logical specifications, by Alwen Tiu (PhD 2004). In the first paper Miller and Tiu introduce a new logical quantifier called nabla which allows them to overcome the previous issue with encoding free variables. In particular, they are able to elegantly encode many notions from the pi-calculus. The second work is Tiu's PhD thesis in which he adds a notion of induction and coinduction on recursive definitions to the logic. * A logic for reasoning about generic judgments, by Alwen Tiu (LFMTP 2006) and Combining generic judgments with recursive definitions, by Andrew Gacek, Dale Miller, and Gopalan Nadathur (LICS 2008). In the first paper Tiu notices that the original formulation of nabla is often too strict when reasoning inductively, and so he defines an alternative treatment of nabla which acts more naturally. In the latter paper, Miller, Nadathur, and I note that the typical treatment of recursive definitions does not allow us to analyze the structure of terms that are built up using nabla, thus we propose an extension to recursive definitions to handle this. * Reasoning in Abella about structural operational semantics specifications, by Andrew Gacek, Dale Miller, and Gopalan Nadathur (LFMTP 2008). I highlight this paper because it presents an extended example (weak normalization for simply-typed lambda calculus) of how reasoning is conducted using the logic developed in the LICS 2008 paper. For a practical perspective of reasoning, this may be the most up-to-date and relevant work. The Abella website has links to many of these papers and some additional references. Also, if you are looking for practical examples, the website has various applications that have been developed using the logic from the LICS 2008 paper. This includes things like POPLmark, Church-Rosser, normalization results on the lambda-calculus, and cut-elimination for a sequent calculus. If you are more interested in how exactly we allow HOAS to interact with induction, I can sketch that here. The idea is that we allow induction on recursive definitions, and not specifically on HOAS terms. Thus, for example, if one is reasoning about evaluation of an expression E to a value V, we will induct on the predicate (eval E V). Thus we can do induction on the structure of a HOAS term by writing down a predicate which recognizes the terms of interest and then inducting on that predicate. This is the essential idea, though things are more complicated in detail. Finally, there is a lot of work in this area based on LF and Twelf that I have not mentioned, but hopefully somebody who is more involved in that work can describe it here. -Andrew Gacek On Wed, Nov 12, 2008 at 1:26 PM, Andrei Popescu wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Type Theorists and Practioners, > > I would like to know what is the state of the art in taming the interaction between HOAS (higher order abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions. (I am aware of some of the work, but very probably I am not aware of the latest progress.) > > Thank you in advance, > Andrei Popescu > > > > > > From crary at cs.cmu.edu Wed Nov 12 17:43:42 2008 From: crary at cs.cmu.edu (Karl Crary) Date: Wed, 12 Nov 2008 17:43:42 -0500 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <720364.67916.qm@web56102.mail.re3.yahoo.com> References: <720364.67916.qm@web56102.mail.re3.yahoo.com> Message-ID: <491B5C1E.7070203@cs.cmu.edu> The Twelf wiki (twelf.plparty.org) has a lot of material on how to do things with higher-order representations. What specifically are you looking to tame? -- Karl Crary Andrei Popescu wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Type Theorists and Practioners, > > I would like to know what is the state of the art in taming the interaction between HOAS (higher order abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions. (I am aware of some of the work, but very probably I am not aware of the latest progress.) > > Thank you in advance, > Andrei Popescu > > > > > > > From uuomul at yahoo.com Wed Nov 12 18:50:57 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Wed, 12 Nov 2008 15:50:57 -0800 (PST) Subject: [TYPES] HOAS versus meta reasoning Message-ID: <997300.19725.qm@web56101.mail.re3.yahoo.com> Dear Andrew and Karl, I thank you very much for your comments and references. To answer Karl's question, I used the word "taming" because, as far as I see, the interaction between meta-reasoning (by which I understand reasoning about the object system) and HOAS is a wild issue. Going back one level and (case-)analyzing the meta-logic inference itself in a meta-meta logic seems like an elegant, but extreme measure to take -- for one thing, it breaks the ties with more conventional frameworks for developing mathematics, such as the ones of Coq, Isabelle/HOL or PVS, where a working mathematician feels immediately comfortable (thanks to the standard foundations), and where many libraries of theories are available. Staying in a conventional framework, on the other hand, requires compromises on the hassle-free (i.e., typing-context-free, substitution-free, bound-variables-free etc.) aspect of the representation. I was not looking for taming any aspect in particular, but for getting a picture of the recent progress within the above approaches and maybe others in between. Regards, Andrei Popescu --- On Thu, 11/13/08, Karl Crary wrote: > From: Karl Crary > Subject: Re: [TYPES] HOAS versus meta reasoning > To: uuomul at yahoo.com > Cc: types-list at lists.seas.upenn.edu > Date: Thursday, November 13, 2008, 12:43 AM > The Twelf wiki (twelf.plparty.org) has a lot of material on > how to do things with higher-order representations. What > specifically are you looking to tame? > -- Karl Crary > > > Andrei Popescu wrote: > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Dear Type Theorists and Practioners, > > I would like to know what is the state of the art in > taming the interaction between HOAS (higher order abstract > syntax) and meta-reasoning/inductive reasoning/recursive > definitions. (I am aware of some of the work, but very > probably I am not aware of the latest progress.) > > Thank you in advance, Andrei Popescu > > > > > > > > From drl at cs.cmu.edu Thu Nov 13 03:03:02 2008 From: drl at cs.cmu.edu (Dan Licata) Date: Thu, 13 Nov 2008 03:03:02 -0500 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <720364.67916.qm@web56102.mail.re3.yahoo.com> References: <720364.67916.qm@web56102.mail.re3.yahoo.com> Message-ID: <20081113080301.GB7958@cs.cmu.edu> On Nov12, Andrei Popescu wrote: > I would like to know what is the state of the art in taming the > interaction between HOAS (higher order abstract syntax) and > meta-reasoning/inductive reasoning/recursive definitions. (I am aware > of some of the work, but very probably I am not aware of the latest > progress.) Hi Andrei, Funny you should ask! You can get a hands-on feel for how this issue is addressed in Twelf by coming to the Twelf Tutorial on January 19, co-located with this year's POPL: http://twelftutorial.plparty.org/ Registration is now open! If you can't make the tutorial, there are tons of examples of induction on HOAS on the Twelf Wiki: http://twelf.plparty.org/ You should also look at two newer functional languages for computing with LF terms, Delphin: http://cs-www.cs.yale.edu/homes/delphin/ and Beluga: http://www.cs.mcgill.ca/~complogic/beluga/ These LF-based approaches distinguish a representation layer (the LF logical framework) from a separate meta-language (Twelf/Delphin/Beluga). Inside LF, the types that you use to represent syntax are just base types, not inductive types, so there is no problem with constants like (lam : (exp -> exp) -> exp). Externally to LF, the canonical forms of LF are treated as an inductive definition in a meta-language (such as Twelf/Delphin/Beluga), which allows you to compute and reason by structural induction on syntax. An alternative approach, which I have been investigating with Noam Zeilberger and Bob Harper, is to integrate an LF-like function space for representing binding, along with a standard computational function space, as two different types in a single type theory. See our LICS'08 paper "Focusing on Binding and Computation", which is linked from here: http://www.cs.cmu.edu/~drl/pubs.html There has also been a good deal of work on representing variable binding using a computational function space (e.g., in Coq), but I will defer to others to provide the best citations. -Dan From jonathan.aldrich at cs.cmu.edu Thu Nov 13 10:24:35 2008 From: jonathan.aldrich at cs.cmu.edu (Jonathan Aldrich) Date: Thu, 13 Nov 2008 10:24:35 -0500 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <20081113080301.GB7958@cs.cmu.edu> References: <720364.67916.qm@web56102.mail.re3.yahoo.com> <20081113080301.GB7958@cs.cmu.edu> Message-ID: <491C46B3.30409@cs.cmu.edu> > These LF-based approaches distinguish a representation layer (the LF > logical framework) from a separate meta-language (Twelf/Delphin/Beluga). > Inside LF, the types that you use to represent syntax are just base > types, not inductive types, so there is no problem with constants like > (lam : (exp -> exp) -> exp). Externally to LF, the canonical forms of > LF are treated as an inductive definition in a meta-language (such as > Twelf/Delphin/Beluga), which allows you to compute and reason by > structural induction on syntax. One more LF-based approach is the education-focused SASyLF tool, which uses essentially the same meta-theory as Twelf, but is restricted to the Second-order Abstract Syntax (SASy) case. The benefit of this restriction is that we can provide a surface syntax for the representation language and meta-language that is almost identical to the notation one might use in a paper proof, thus greatly decreasing the learning curve for students. As in Twelf, binding in the represented language can be represented as binding in the representation language, and induction proceeds over canonical LF forms--but in the surface syntax, it just looks like induction over syntax and/or derivations. SASyLF is currently being used in a couple of graduate type theory courses; for the tool, examples, and more information see: http://www.sasylf.org/ Jonathan From marcin.zalewski at gmail.com Thu Nov 13 10:57:16 2008 From: marcin.zalewski at gmail.com (Marcin Zalewski) Date: Thu, 13 Nov 2008 16:57:16 +0100 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <720364.67916.qm@web56102.mail.re3.yahoo.com> References: <720364.67916.qm@web56102.mail.re3.yahoo.com> Message-ID: <7c0fdf4f0811130757k626b5d54n7499895e5ac9770c@mail.gmail.com> Andrei, I am not an expert and I am not exactly sure what are you looking for but I think that Parametric HOAS (PHOAS) may be of interest to you: http://adam.chlipala.net/ There is also a related project, that actually mentions "taming." :) Here it is: http://ltamer.sourceforge.net/ I hope that you find this reference useful. Marcin On Wed, Nov 12, 2008 at 8:26 PM, Andrei Popescu wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Type Theorists and Practioners, > > I would like to know what is the state of the art in taming the interaction between HOAS (higher order abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions. (I am aware of some of the work, but very probably I am not aware of the latest progress.) > > Thank you in advance, > Andrei Popescu > > > > > > From adam at poswolsky.com Thu Nov 13 15:09:37 2008 From: adam at poswolsky.com (Adam Poswolsky) Date: Thu, 13 Nov 2008 15:09:37 -0500 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <720364.67916.qm@web56102.mail.re3.yahoo.com> References: <720364.67916.qm@web56102.mail.re3.yahoo.com> Message-ID: <491C8981.3060805@poswolsky.com> Hi Andrei, I would like to draw your attention to Delphin which tackles reasoning over higher-order encodings using a functional paradigm. The system is available for download and a quick user manual is available in my dissertation. http://cs-www.cs.yale.edu/homes/delphin/delphin.htm --Adam Andrei Popescu wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Type Theorists and Practioners, > > I would like to know what is the state of the art in taming the interaction between HOAS (higher order abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions. (I am aware of some of the work, but very probably I am not aware of the latest progress.) > > Thank you in advance, > Andrei Popescu > > > > > > From crary at cs.cmu.edu Thu Nov 13 15:13:05 2008 From: crary at cs.cmu.edu (Karl Crary) Date: Thu, 13 Nov 2008 15:13:05 -0500 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <997300.19725.qm@web56101.mail.re3.yahoo.com> References: <997300.19725.qm@web56101.mail.re3.yahoo.com> Message-ID: <491C8A51.50906@cs.cmu.edu> I see. You should probably look at Licata, Harper, and Zeilberger's paper from the most latest LICS. They show that you can sort (one might say tame) the HOAS issues by taking a view based in focusing (which arises from theorem proving). The basic idea to focusing is to sort the connectives into positive and negative. Positive connectives are eliminated via pattern matching, while negative connectives are introduced via pattern matching. For example, sums are positive because they are eliminated using pattern matching, but functions are negative because they are introduced using pattern matching (on the argument). Products can be taken either way, resulting in two different connectives. (Equivalently, you can view positive connectives as ones with a closed-scope elimination form and negative connectives as ones with an open-scope elimination form.) They observe that the representational arrow used in HOAS is not the usual negative function space, but a *positive* function space. The positivity of the function space ensures that the function is parametric, which higher-order representations depend on. In essence, A -pos-> B refers to a B that is constructed using a new introduction form for A. (Note that A must be atomic; otherwise positive functions would be creating new intro forms for connectives.) Functions that analyze their arguments employ the usual negative function space. Although most existing LF-based systems have (what we can now recognize as) negative functions only at a meta-level, there's no reason it must be so. We can integrate positive and negative functions into the same system, and there's good reason to do so. When you do so, the two function spaces can interact in interesting and surprising ways. In short, some of the structural properties that one expects can fail when the two are combined. (I suspect this is the sort of thing you are looking to tame.) Licata, et al.'s framework shows exactly when/how this happens, and what you need to do to if you want to prevent it from happening. Their framework also shows that the concern that is sometimes raised over negative instances arising in HOAS is really a red herring. The problem, as I understand it, is as follows: Suppose I take the higher-order representation of the lambda calculus: lam : (exp -> exp) -> exp. app : exp -> exp -> exp. and try to make it into a recursive definition. Then I obtain something like: mu X . (X -> X) + (X * X) and this doesn't work the way it is supposed to, because of the negative occurrence of X. Consequently, you cannot use HOAS in this manner. Some people find this mysterious, but the mystery disappears when you consider which arrow is being used. If I use the negative arrow this can be fine, but it has nothing to do with HOAS, which relies on the positive arrow. If, on the other hand, I use the positive arrow, then this is ill-formed (even if we have recursive types), because the domain of a positive function has to be atomic, and therefore cannot be the type variable X. -- Karl Crary Andrei Popescu wrote: > Dear Andrew and Karl, > > I thank you very much for your comments and references. > > To answer Karl's question, I used the word "taming" because, as far as I see, the interaction between meta-reasoning (by which I understand reasoning about the object system) and HOAS is a wild issue. Going back one level and (case-)analyzing the meta-logic inference itself in a meta-meta logic seems like an elegant, but extreme measure to take -- for one thing, it breaks the ties with more conventional frameworks for developing mathematics, such as the ones of Coq, Isabelle/HOL or PVS, where a working mathematician feels immediately comfortable (thanks to the standard foundations), and where many libraries of theories are available. Staying in a conventional framework, on the other hand, requires compromises on the hassle-free (i.e., typing-context-free, substitution-free, bound-variables-free etc.) aspect of the representation. I was not looking for taming any aspect in particular, > but for getting a picture of the recent progress within the above approaches and maybe others in between. > > Regards, > Andrei Popescu > > > From miculan at dimi.uniud.it Thu Nov 13 16:55:20 2008 From: miculan at dimi.uniud.it (Marino Miculan) Date: Thu, 13 Nov 2008 22:55:20 +0100 Subject: [TYPES] HOAS versus meta reasoning (Andrew Gacek) In-Reply-To: References: Message-ID: <327AD2A9-2B09-4A14-9EC0-096B253FDFD9@dimi.uniud.it> Andrew Gacek wrote: > I would like to know what is the state of the art in taming the > interaction between HOAS (higher order abstract syntax) and meta- > reasoning/inductive reasoning/recursive definitions. (I am aware of > some of the work, but very probably I am not aware of the latest > progress.) Also the Theory of Context should be mentioned, which goes back to ten years ago. The ToC is an axiomatic theory which allows for structural inductive definitions/proofs and recursive definitions over (weak) HOAS, within existing systems (we used Coq). The best references are An axiomatic approach to metareasoning on systems in higher-order abstract syntax Furio Honsell, Marino Miculan and Ivan Scagnetto In Proceedings of ICALP'01, Number 2076 in Lecture Notes in Computer Science, pages 963-978, 2001 ?-calculus in (Co)Inductive Type Theories Furio Honsell, Marino Miculan and Ivan Scagnetto Theoretical Computer Science, 253(2), pages 239-285, 2001. but other papers are available from my web page. -marino -- Marino Miculan - Dept Math Compu Sci, University of Udine miculan at dimi.uniud.it http://www.dimi.uniud.it/miculan/ From kurz at mcs.le.ac.uk Fri Nov 14 04:55:51 2008 From: kurz at mcs.le.ac.uk (Alexander Kurz) Date: Fri, 14 Nov 2008 09:55:51 +0000 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <491C8A51.50906@cs.cmu.edu> References: <997300.19725.qm@web56101.mail.re3.yahoo.com> <491C8A51.50906@cs.cmu.edu> Message-ID: <491D4B27.1040309@mcs.le.ac.uk> Karl Crary wrote: > Their framework also shows that the concern that is sometimes raised > over negative instances arising in HOAS is really a red herring. The > problem, as I understand it, is as follows: Suppose I take the > higher-order representation of the lambda calculus: > > lam : (exp -> exp) -> exp. > app : exp -> exp -> exp. > > and try to make it into a recursive definition. Then I obtain something > like: > > mu X . (X -> X) + (X * X) > > and this doesn't work the way it is supposed to, because of the negative > occurrence of X. Consequently, you cannot use HOAS in this manner. Can you expand on this? I would like to understand better what the problem is. In particular in the light of the work of Gabbay/Pitts, Fiore/Plotkin/Turi, and M.Hofmann, all at Lics'99, who showed that mu X . (X -> X) + (X * X) + Var is an initial algebra (lambda terms up to alpha equivalence) supporting proofs by induction. There has been a lot of work on this since then, in particular by Pitts and collaborators. Thanks in advance, Alexander From Andrew.Pitts at cl.cam.ac.uk Fri Nov 14 10:41:22 2008 From: Andrew.Pitts at cl.cam.ac.uk (Andrew Pitts) Date: Fri, 14 Nov 2008 15:41:22 +0000 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <491D4B27.1040309@mcs.le.ac.uk> References: <997300.19725.qm@web56101.mail.re3.yahoo.com> <491C8A51.50906@cs.cmu.edu> <491D4B27.1040309@mcs.le.ac.uk> Message-ID: Dear Alexander, 2008/11/14 Alexander Kurz : > Can you expand on this? I would like to understand better what the > problem is. In particular in the light of the work of Gabbay/Pitts, > Fiore/Plotkin/Turi, and M.Hofmann, all at Lics'99, who showed that > > mu X . (X -> X) + (X * X) + Var > > is an initial algebra (lambda terms up to alpha equivalence) supporting > proofs by induction. That's not quite accurate. We were looking at mu X . (Var => X) + (X * X) + Var (i.e. semi-HOAS) where either [Fiore/Plotkin/Turi, and M.Hofmann] the equation is interpreted in a category of presheaves and "Var=>(-)" is the ordinary function space, right adjoint to Var x (-)) [good]; but the category does not suppurt the law of excluded middle [not so good]; or [Gabbay/Pitts] the equation is interpreted in the category of nominal sets and Var=>(-) is not the ordinary function space but rather is right adjoint to the separated product Var \otimes (-) [maybe not so good, but cf separation logic and the fact that Var=>(-) has a very concrete description related to alpha-equivalence]; and in this case the category does support the law of excluded middle [good]. >There has been a lot of work on this since then, in > particular by Pitts and collaborators. Quick tutorial on nominal sets in A. M. Pitts, Alpha-Structural Recursion and Induction, Journal of the ACM 53(2006)459-506. The catgory of nominal sets is probably a good place to look for denotational models of the Harper/Licata/Zeilberger "representational arrow" that Karl Crary mentioned in a previous message in this thread. Andy From brianh at cs.pdx.edu Fri Nov 14 18:20:45 2008 From: brianh at cs.pdx.edu (Brian Huffman) Date: Fri, 14 Nov 2008 15:20:45 -0800 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <20081113080301.GB7958@cs.cmu.edu> References: <720364.67916.qm@web56102.mail.re3.yahoo.com> <20081113080301.GB7958@cs.cmu.edu> Message-ID: <20081114152045.aioc73hx08c8occo@webmail.pdx.edu> Quoting Dan Licata : > There has also been a good deal of work on representing variable binding > using a computational function space (e.g., in Coq), but I will defer > to others to provide the best citations. > > -Dan > > I would also be interested in citations about variable binding using computational function space, if anyone knows any good ones. In particular, I am thinking about using domain theory (Isabelle/HOLCF) and the continuous function space for doing HOAS. I would appreciate any pointers to relevant work. - Brian From murdoch.gabbay at gmail.com Sat Nov 15 05:10:56 2008 From: murdoch.gabbay at gmail.com (murdoch gabbay) Date: Sat, 15 Nov 2008 10:10:56 +0000 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: References: <997300.19725.qm@web56101.mail.re3.yahoo.com> <491C8A51.50906@cs.cmu.edu> <491D4B27.1040309@mcs.le.ac.uk> Message-ID: Dear Alexander, In a recent paper Martin Hofmann and I make the weak HOAS-syle datatype mu X. (Var -> X) + (X x X) + Var compatible with a flavour of nominal techniques: http://www.gabbay.org.uk/papers.html#nomrs (In a final note we hypothesise how similar techniques might be applicable to model abstraction in strong HOAS "(X -> X)" style.) I've written a survey and update paper on nominal techniques, which is now under consideration for publication. http://www.gabbay.org.uk/papers.html#setfnt Comments are welcome. Jamie -- Murdoch James Gabbay www.gabbay.org.uk --- Which is worse, ignorance or apathy? --- Who knows? Who cares? From uuomul at yahoo.com Mon Nov 17 17:33:06 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Mon, 17 Nov 2008 14:33:06 -0800 (PST) Subject: [TYPES] HOAS versus meta reasoning Message-ID: <117665.23060.qm@web56101.mail.re3.yahoo.com> Thank you for your explanations! >> --- On Thu, 11/13/08, Karl Crary wrote: >> Their framework also shows that the concern that is sometimes raised >> over negative instances arising in HOAS is really a red herring. I would not call the above neither concern, nor a red herring, but rather state it in the form of a "naive" hope. Without trying to invent pseudo-paradoxes, I would just like to point that the idea behind the HOAS paradigm (as I see it) was in itself something that looked like a naive hope, coming from the "logical fallacy" of confusing the object-level with the meta-level: "When I consider the lambda term <> why can't I assume that "lambda" is not just a representation of a function abstraction, but it *is precisely function abstraction*? " Of course, this "naive" hope has received sophisticated solutions, and the references of this thread witness this. (A similar situation being the "naive, non-mathematical" equations written by Christopher Strachey to express the meaning of programs that later received mathematical justifications from the domain theory of Dana Scott.) A "constructor" like -- lam : (exp -> exp) -> exp. may be fallacious in classical logic, but one may hope that it would be valid (i.e., actually representing a constructor) in other logics. Of course, changing/restricting the function space is another possible solution (or this may be part of the solution). This "naive" hope driven style of inquiry becomes sharper, in my opinion, when we move from representing syntax to representing inference, and I think the latter is an equally important aspect of HOAS which unfortunately is not transparent in the name "HOAS". (By the way, approaches around weak HOAS, including Nominal Logic, do not seem to address this issue at all.) Consider a typing system with a familiar rule for typing abstraction, like Gamma, x : A |- Y : B ---------------------------- Gamma |- Lam(x:A,Y) : A -> B In idealized HOAS, one would represent it as something like (All x. typeOf(x,A) => typeOf(Y x,B)) => typeOf(Lam(A,Y), Arrow(A,B)) (*) (where we may assume that Lam is now an operator of type (Term -o-> Term) -> Term, for some appropriate choice of the space Term -o-> Term that comes with an appropriate application destructor.) The question is of course not whether the above clause is sound in a classical logic for the represented system (typically it will not be sound, and one reason for this is that it will type anything to an arrow type with uninhabited source), but: When and where is it sound? And, if so: When and where can it be viewed as something like an inductive clause (just like its object-level counterpart)? The answers in the style of the Miller-McDowell and Twelf approaches are instances of the following: consider a further meta-level layer and from there you can regard this clause (via its associated rule on sequents in the representation logic) as an inductive clause. However, isn't this shifting the burden of handling contexts from the contexts of the object logic to the ones of the representation logic? Andrei Popescu --- On Thu, 11/13/08, Karl Crary wrote: > From: Karl Crary > Subject: Re: [TYPES] HOAS versus meta reasoning > To: uuomul at yahoo.com > Cc: types-list at lists.seas.upenn.edu > Date: Thursday, November 13, 2008, 10:13 PM > I see. You should probably look at Licata, Harper, and > Zeilberger's paper from the most latest LICS. They show > that you can sort (one might say tame) the HOAS issues by > taking a view based in focusing (which arises from theorem > proving). > > The basic idea to focusing is to sort the connectives into > positive and negative. Positive connectives are eliminated > via pattern matching, while negative connectives are > introduced via pattern matching. For example, sums are > positive because they are eliminated using pattern matching, > but functions are negative because they are introduced using > pattern matching (on the argument). Products can be taken > either way, resulting in two different connectives. > (Equivalently, you can view positive connectives as ones > with a closed-scope elimination form and negative > connectives as ones with an open-scope elimination form.) > > They observe that the representational arrow used in HOAS > is not the usual negative function space, but a *positive* > function space. The positivity of the function space > ensures that the function is parametric, which higher-order > representations depend on. In essence, A -pos-> B refers > to a B that is constructed using a new introduction form for > A. (Note that A must be atomic; otherwise positive > functions would be creating new intro forms for > connectives.) > > Functions that analyze their arguments employ the usual > negative function space. Although most existing LF-based > systems have (what we can now recognize as) negative > functions only at a meta-level, there's no reason it > must be so. We can integrate positive and negative > functions into the same system, and there's good reason > to do so. > > When you do so, the two function spaces can interact in > interesting and surprising ways. In short, some of the > structural properties that one expects can fail when the two > are combined. (I suspect this is the sort of thing you are > looking to tame.) Licata, et al.'s framework shows > exactly when/how this happens, and what you need to do to if > you want to prevent it from happening. > > Their framework also shows that the concern that is > sometimes raised over negative instances arising in HOAS is > really a red herring. The problem, as I understand it, is > as follows: Suppose I take the higher-order representation > of the lambda calculus: > > lam : (exp -> exp) -> exp. > app : exp -> exp -> exp. > > and try to make it into a recursive definition. Then I > obtain something like: > > mu X . (X -> X) + (X * X) > > and this doesn't work the way it is supposed to, > because of the negative occurrence of X. Consequently, you > cannot use HOAS in this manner. > > Some people find this mysterious, but the mystery > disappears when you consider which arrow is being used. If > I use the negative arrow this can be fine, but it has > nothing to do with HOAS, which relies on the positive arrow. > If, on the other hand, I use the positive arrow, then this > is ill-formed (even if we have recursive types), because the > domain of a positive function has to be atomic, and > therefore cannot be the type variable X. > > -- Karl Crary > > > > Andrei Popescu wrote: > > Dear Andrew and Karl, > > I thank you very much for your comments and > references. > > To answer Karl's question, I used the word > "taming" because, as far as I see, the interaction > between meta-reasoning (by which I understand reasoning > about the object system) and HOAS is a wild issue. Going > back one level and (case-)analyzing the meta-logic inference > itself in a meta-meta logic seems like an elegant, but > extreme measure to take -- for one thing, it breaks the > ties with more conventional frameworks for developing > mathematics, such as the ones of Coq, Isabelle/HOL or PVS, > where a working mathematician feels immediately comfortable > (thanks to the standard foundations), and where many > libraries of theories are available. Staying in a > conventional framework, on the other hand, requires > compromises on the hassle-free (i.e., typing-context-free, > substitution-free, bound-variables-free etc.) aspect of the > representation. I was not looking for taming any aspect in > particular, but for getting a picture of the recent progress > within the above approaches and maybe others in between. > > Regards, Andrei Popescu > > > > From uuomul at yahoo.com Mon Nov 17 17:37:26 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Mon, 17 Nov 2008 14:37:26 -0800 (PST) Subject: [TYPES] HOAS versus meta reasoning Message-ID: <932497.75268.qm@web56104.mail.re3.yahoo.com> I very much appreciate the comments and references that were posted on this thread. Thank you for establishing my reading schedule for the next month or so. :) Regards, Andrei From drl at cs.cmu.edu Tue Nov 18 00:29:20 2008 From: drl at cs.cmu.edu (Dan Licata) Date: Tue, 18 Nov 2008 00:29:20 -0500 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <117665.23060.qm@web56101.mail.re3.yahoo.com> References: <117665.23060.qm@web56101.mail.re3.yahoo.com> Message-ID: <20081118052920.GB28826@cs.cmu.edu> Hi Andrei, On Nov17, Andrei Popescu wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > This "naive" hope driven style of inquiry becomes sharper, in my > opinion, when we move from representing syntax to representing > inference, and I think the latter is an equally important aspect of > HOAS which unfortunately is not transparent in the name "HOAS". We've used the term "higher-order judgements" for this on the Twelf Wiki. > Consider a typing system with a familiar rule for typing abstraction, > like > > Gamma, x : A |- Y : B > ---------------------------- > Gamma |- Lam(x:A,Y) : A -> B > > In idealized HOAS, one would represent it as something like > > (All x. typeOf(x,A) => typeOf(Y x,B)) => > typeOf(Lam(A,Y), Arrow(A,B)) (*) Here is this example in Twelf: http://twelf.plparty.org/wiki/Higher-order_judgements > When and where is it sound? > > And, if so: > > When and where can it be viewed as something like an inductive clause > (just like its object-level counterpart)? > > The answers in the style of the Miller-McDowell and Twelf approaches > are instances of the following: consider a further meta-level layer > and from there you can regard this clause (via its associated rule on > sequents in the representation logic) as an inductive clause. I won't speak for Miller-McDowell, but in LF, this clause is a generator that helps populate the LF base type 'typeOf'. So when you consider the canonical LF terms of type 'typeOf(E,T)', one case will be that the term has the form of-lam (\x.\dx.D(x,dx)) where \x.\dx.D(x,dx) is an LF function of type Pi x. typeOf(x,A) => typeOf(Y x,B) I think of LF as a fancy version of the ML datatype mechanism, one that gives you two new ingredients: (1) a notion of binding and scope, and (2) dependent types. > However, isn't this shifting the burden of handling contexts from the > contexts of the object logic to the ones of the representation logic? If I understand you correctly, then yes, and that's a good thing! By representing the object language context as the LF context, you can inherit properties like substitution from LF. See this page for a little explanation: http://twelf.plparty.org/wiki/Substitution I hope that answers some of your questions, -Dan From uuomul at yahoo.com Tue Nov 18 02:56:39 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Mon, 17 Nov 2008 23:56:39 -0800 (PST) Subject: [TYPES] HOAS versus meta reasoning - correction Message-ID: <820439.72119.qm@web56108.mail.re3.yahoo.com> Please ignore my remark from the previous posting: "By the way, approaches around weak HOAS, including Nominal Logic, do not seem to address this issue [that is, representation of inference] at all." This is of course not true. What I meant to say is that it appears that only strong-HOAS-like settings address the issue of representing inference in such a way that typing contexts do not appear explicitly in the representation (but are rather embedded shallowly into representation-logic contexts). Andrei From crary at cs.cmu.edu Tue Nov 18 11:01:41 2008 From: crary at cs.cmu.edu (Karl Crary) Date: Tue, 18 Nov 2008 11:01:41 -0500 Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <117665.23060.qm@web56101.mail.re3.yahoo.com> References: <117665.23060.qm@web56101.mail.re3.yahoo.com> Message-ID: <4922E6E5.2050909@cs.cmu.edu> Well, let me just say that rather than try to peer into the mind of the authors of LF, I would prefer to let the mathematics stand for itself. I'm not aware that the theory of adequacy developed in LF was somehow deficient. It's been known from the start that the power of LF stemmed from its apparent weakness. In the years since LF was invented, there has been a lot of effort to carry out the LF methodology (now often called higher-order abstract syntax, or higher-order representations) in a stronger settting, in order to use higher-order representations and simultaneously do something else. That's what I thought we were talking about. -- Karl Crary Andrei Popescu wrote: > I would not call the above neither concern, nor a red herring, but rather > state it in the form of a "naive" hope. > Without trying to invent pseudo-paradoxes, I would just like to point > that the idea > behind the HOAS paradigm (as I see it) was in itself something that > looked like a naive hope, coming from the "logical fallacy" of confusing > the object-level with the meta-level: > > "When I consider the lambda term <> why can't I assume that > "lambda" is not just a representation of a function abstraction, but > it *is precisely function abstraction*? " > > Of course, this "naive" hope has received sophisticated solutions, > and the references of this thread witness this. (A > similar situation being the "naive, non-mathematical" equations written > by Christopher Strachey to > express the meaning of programs that later received mathematical > justifications from the domain theory of Dana Scott.) > From uuomul at yahoo.com Tue Nov 18 19:11:00 2008 From: uuomul at yahoo.com (Andrei Popescu) Date: Tue, 18 Nov 2008 16:11:00 -0800 (PST) Subject: [TYPES] HOAS versus meta reasoning In-Reply-To: <4922E6E5.2050909@cs.cmu.edu> Message-ID: <519458.42036.qm@web56102.mail.re3.yahoo.com> 1) I did not use the word "naive" pejoratively. (True, because of its connotation, I should have avoided this word altogether.) I meant it as referring to a pure, not necessarily (or immediately) mathematical (or mathematically consistent) idea, just like Cantor's "naive" notion of a set described by comprehension. I certainly did not want to sound as if I am trying to trivialize the idea (although, unavoidably, I have reduced it by casting it into my own understanding). Also, I was not trying to peer (in any sense of the word :) ) into the mind of the LF creators, but rather into the mind of a common working-class person that works at representing logics and reasoning about and wants to have her/his job simplified. 2) LF was designed for encoding logics for the purpose of reasoning *in* these logics. It does this job beautifully for structural logics, and is also able to do this for some non- (or less-) structural logics. Most logics in current use fall in these categories. End of the story. I have no questions here. Encoding a logic in a meta-logic higher-order- abstract-syntactically proceeds axiomatically (stating axioms in the meta-logic). This approach (LF, Pfenning and Elliott, (generic) Isabelle, etc.) uses frameworks which are, as Karl Crary reminded me, very weak purposely for accommodating logic definitions. In the above light, thinking of HOAS as a mechanism for encoding a logic L in a meta-logic M for reasoning *in L*, there is nothing of the sort of things I have talked about. My "psychological interpretation" of the HOAS idea only makes sense after one poses the question of meta-reasoning *about L*, hopefully in M or a natural extension of M. For this, one needs to induct in M about L-inferences. One way to try to achieve this is by replacing M with a stronger (more "committed") logic M' so to allow induction principles and try to use the same (or a similar) style of representation for L in M' as for L in M, retaining the HOAS flavor (and convenience). (Having his precious M already accommodating adequacy nicely, one may alternatively prefer to leave M unaltered and take M' as a meta-logic for M rather than as an extension of M. Then reasoning about L-inferences becomes reasoning in M' about M-inferences. This preserves the HOAS nature of syntax encoding, but, as far as I see, re-introduces a level of indirection in dealing with inferences present in non-HOAS encodings -- I detail this below at point 3. ) But one does not need to go through logical frameworks (i.e., through the notion of representing L for the purpose of reasoning *in L*) to reach the latter idea. Thus, for instance, one can start directly with a stronger logic M' and try to HOAS-represent L in it definitionally (or partly definitionally, partly axiomatically), rather than entirely axiomatically. (And this has been done.) Typically M' shall be strong enough so that it is able to define any (recursively specifiable) logic in a way that mirrors the informal definition of L (without employing HOAS) -- e.g., if M' is HOL or ZF and L is simply-typed lambda calculus, then the representation of L in M' would be the standard definition of this calculus in M' (with alpha-equivalence and substitution defined as usual, etc.). In such a logic M' (say, for now, that M' is HOL), since one has the standard definition to refer to, one can now ask my question: For the term "lambda x : T. E", can I assume that "lambda" is really function abstraction (so that in HOL lambda-terms will be functions, and, regarded from a meta-logic for which both HOL and L are objects, so that the L-bindings are captured by HOL-bindings)? (The answer to the question may require modification of the principles of the logic and/or of the notion of a function, etc.) The above statement of the goal of HOAS-representing syntax has in itself the assumption that one will also want to reason *about* this syntax. What turned out, due to my not very careful choice of the words, as a conjecture that this was the original motivation behind HOAS is indeed anachronistic, since, indeed, an approach that first visits logical frameworks already has a HOAS representation of syntax and wants to extend it with inductive reasoning. 3) Regarding the situation of M' being a meta-logic for M rather than an extension of M (or M itself). I think this retains the HOAS convenience for dealing with syntax (as Dan Licata pointed out), but loses, to some extent, the convenience of dealing with inference/judgments. I can best explain what I mean by taking an object-logic example that does not possess any bindings -- this symbolizes a situation where the syntax representation has already been dealt with adequately, and we may focus on inference. The object system L is the following: Syntax: n ::= 0 | S(n) Gamma ::= [] | Gamma,n Inference: Gamma |- 0 Gamma,n |- n Gamma |- n ----------- Gamma,m |- n Gamma |- n -------------- Gamma |- S(S(n)) Since L is a structural "logic", we may encode this axiomatically in blank intuitionistic HOL (or, alternatively, in an explicit-proof-term fashion, in LF) as follows: type nat op S : nat --> nat Deduce(0) Deduce(n) => Deduce(S(n)) This is fine (adequate) if we want to reason *in L*. For being able to reason *about L* while retaining a similar representation, one may assume (a carefully chosen version of) HOL with induction and recursion principles included and: -- use the HOL type nat of natural numbers for encoding the syntax -- use a predicate Deduce : nat --> bool defined recursively by the above axioms (now regarded as inductive clauses). Now, if an adequacy result includes at least the following: [] |- n (in L) iff HOL |- Deduce(n) then we would be able to reason in HOL about L (at least w.r.t. properties holding in L with empty context), while retaining a shallow encoding of L-inference (and not only of L-syntax). On the other hand, if we choose to keep the original blank HOL (which allows axiomatic adequacy) and move one level up to a meta logic M' that accommodates induction over HOL inferences, then we would not speak of a predicate "Deduce", but rather of a predicate "HOL |- Deduce(n)", which does not seem more convenient than using directly a definition of L in M' and speak about a predicate "[] |- n". This approach keeps the HOAS encoding of syntax, but looses the HOAS-encoding of inference. True, my example of a logic L does not illustrate the problem of judgments whose natural shallow embedding has negative occurrences of atomic formulas that seem to stand against inductive interpretations. Moreover, properties of L that require the consideration of typing contexts essentially, such as: "If Gamma |- n, then there exists Gamma' that includes Gamma and has even cardinality such that Gamma' |- n", cannot hope for a formulation in a context-free representation, just like properties that refer to bindings and free variables cannot be formulated in a HOAS representation. Probably these are reasons for not going after a shallow embedding of inference after all. Regarding the second aspect though: many properties of interest, including type preservation and normalization, have the empty-context case holding the essence of the property (and the main difficulty in a presumptive proof), with the extension of the result to a contextual version being a mere formality. Regards and apologies for the length of this message, Andrei --- On Tue, 11/18/08, Karl Crary wrote: > From: Karl Crary > Subject: Re: [TYPES] HOAS versus meta reasoning > To: uuomul at yahoo.com > Cc: types-list at lists.seas.upenn.edu > Date: Tuesday, November 18, 2008, 6:01 PM > Well, let me just say that rather than try to peer into the > mind of the authors of LF, I would prefer to let the > mathematics stand for itself. I'm not aware that the > theory of adequacy developed in LF was somehow deficient. > > It's been known from the start that the power of LF > stemmed from its apparent weakness. In the years since LF > was invented, there has been a lot of effort to carry out > the LF methodology (now often called higher-order abstract > syntax, or higher-order representations) in a stronger > settting, in order to use higher-order representations and > simultaneously do something else. That's what I thought > we were talking about. > > -- Karl Crary > > > Andrei Popescu wrote: > > I would not call the above neither concern, nor a red > herring, but rather state it in the form of a > "naive" hope. Without trying to invent > pseudo-paradoxes, I would just like to point that the idea > behind the HOAS paradigm (as I see it) was in itself > something that looked like a naive hope, coming from the > "logical fallacy" of confusing the object-level > with the meta-level: > > "When I consider the lambda term < x. E>> why can't I assume that "lambda" > is not just a representation of a function abstraction, but > it *is precisely function abstraction*? " > > > > Of course, this "naive" hope has received > sophisticated solutions, and the references of this thread > witness this. (A similar situation being the "naive, > non-mathematical" equations written > > by Christopher Strachey to express the meaning of > programs that later received mathematical justifications > from the domain theory of Dana Scott.) > > From types at cis.upenn.edu Fri Dec 19 17:55:55 2008 From: types at cis.upenn.edu (news@health.Pfizer.azn) Date: Fri, 19 Dec 2008 17:55:55 -0500 Subject: [TYPES] Sexual Health Viagra Inc ? Message-ID: <20081220-35811.6526.qmail@MELODY18> "Dear types at cis.upenn.edu!" BEST PRICE ON NET http://www.fadewills.com Satisfaction Guaranteed - Company wants you to be absolutely satisfied with your pharmacyy.If within 30 days of receiving your purchase you?re not completely satisfied, return it for the price you paid for, or we will gladly replace it.