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 > > > Th