From P.B.Levy at cs.bham.ac.uk Thu Feb 2 14:11:20 2017 From: P.B.Levy at cs.bham.ac.uk (Paul B Levy) Date: Thu, 2 Feb 2017 19:11:20 +0000 Subject: [TYPES] semantic coherence for simply typed lambda-calculus Message-ID: Dear all, Take simply typed lambda-calculus with ->, x, +, 0, 1 types. Specifically the Curry-style formulation with no type annotations whatsoever, neither on lambda nor on inl nor on anything else. Here are the two "coherence" statements I'm interested in. (1) Any two derivations of Gamma |- M : A have the same denotation. (2) More generally, for any bicartesian closed category C, any two derivations of Gamma |- M : A have the same denotation in C. I can see roughly how to prove these, but before working it out would like to ask: do these results appear in the literature? My impression is that people have studied semantic coherence for fancy languages (e.g. with subtypes and dependent types), so surely the above statements, or at least (1), are a simple case of some result in the literature. Best regards, Paul -- Paul Blain Levy School of Computer Science, University of Birmingham http://www.cs.bham.ac.uk/~pbl From p.giarrusso at gmail.com Fri Feb 3 21:17:27 2017 From: p.giarrusso at gmail.com (Paolo Giarrusso) Date: Sat, 4 Feb 2017 03:17:27 +0100 Subject: [TYPES] semantic coherence for simply typed lambda-calculus In-Reply-To: References: Message-ID: On Thursday, 2 February 2017, Paul B Levy wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear all, > > Take simply typed lambda-calculus with ->, x, +, 0, 1 types. > Specifically the Curry-style formulation with no type annotations > whatsoever, neither on lambda nor on inl nor on anything else. > > Here are the two "coherence" statements I'm interested in. > > (1) Any two derivations of Gamma |- M : A have the same denotation. > > (2) More generally, for any bicartesian closed category C, any two > derivations of Gamma |- M : A have the same denotation in C. > To double-check: Gamma, M and A are all fixed, right? It seems one can remove the ambiguity in typing by normalizing M first and then relying on the subformula property. Here's a potential proof sketch?I'd love to know if this approach makes sense. (And I'm not even sure if all the steps I'm relying on have actually been proven). Use untyped normalization on M to obtain M'. Since M is typable, normalization terminates?even untyped normalization (right?), since types don't affect evaluation. By preservation, M' should have the same type (even though it's untyped evaluation, right?). By the subformula property of normalization, all types in the derivation of M' are "subformulas" of A so there is no ambiguity in its derivation of Gamma |- M' : A.* Let's call that derivation D. Since normalization preserves the denotation, if we have two derivations D1 and D2 of Gamma |- M : A, we have that [[ D1 ]] = [[ D ]] = [[ D2 ]] hence we have (1) (and I expect (2) as well). * I think this is not so trivial; however, this step is confirmed by the theory of bidirectional typechecking. Quoting Dunfield and Krishnaswami (2013): > As shown by Watkins et al. (2004), bidirectional typechecking can be understood in terms of the normalization of intuitionistic type theory, in which normal forms correspond to the checking mode of bidirectional typechecking, and neutral (or atomic) terms correspond to the synthesis mode. This enables a proof of the elegant property that type annotations are only necessary at reducible expressions, and that normal forms need no annotations at all. Dunfield and Krishnaswami (2013). Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, ICFP 2013, ACM. -- Paolo G. Giarrusso - Ph.D. Student, T?bingen University *http://ps.informatik.uni-tuebingen.de/team/giarrusso/ * From gabriel.scherer at gmail.com Sat Feb 4 07:32:39 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Sat, 4 Feb 2017 13:32:39 +0100 Subject: [TYPES] semantic coherence for simply typed lambda-calculus In-Reply-To: References: Message-ID: Paolo, I had the exact same argument in mind, but I think that beta-normal forms don't cut it when you have types of both polarities. Consider for example the ?-normal form (match x with | inj? () -> ?y.t | inj? () -> ?y.t ) (u) This does not satisfy the subformula property, as the principal type of the "blocked" redex ((?y.t) u) is arbitrary. You need your notion of reduction to have enough commuting conversions to recover the subformula property. A sequent-calculus presentation gives this for free (there are ugly-but-simple sequent terms for this calculus in my thesis manuscript, Section 4.1.4, http://www.ccs.neu.edu/home/gasche/phd_thesis/scherer-thesis.pdf; a proper abstract machine calculus would be more elegant), or looking at cut-free focused term also does the job ? completeness of focusing then embeds the suitable normalization procedure. On Sat, Feb 4, 2017 at 3:17 AM, Paolo Giarrusso wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > On Thursday, 2 February 2017, Paul B Levy wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> ] >> >> Dear all, >> >> Take simply typed lambda-calculus with ->, x, +, 0, 1 types. >> Specifically the Curry-style formulation with no type annotations >> whatsoever, neither on lambda nor on inl nor on anything else. >> >> Here are the two "coherence" statements I'm interested in. >> >> (1) Any two derivations of Gamma |- M : A have the same denotation. >> >> (2) More generally, for any bicartesian closed category C, any two >> derivations of Gamma |- M : A have the same denotation in C. >> > > To double-check: Gamma, M and A are all fixed, right? > > It seems one can remove the ambiguity in typing by normalizing M first and > then relying on the subformula property. Here's a potential proof > sketch?I'd love to know if this approach makes sense. (And I'm not even > sure if all the steps I'm relying on have actually been proven). > > Use untyped normalization on M to obtain M'. Since M is typable, > normalization terminates?even untyped normalization (right?), since types > don't affect evaluation. > By preservation, M' should have the same type (even though it's untyped > evaluation, right?). By the subformula property of normalization, all types > in the derivation of M' are "subformulas" of A so there is no ambiguity in > its derivation of Gamma |- M' : A.* Let's call that derivation D. > > Since normalization preserves the denotation, if we have two derivations D1 > and D2 of Gamma |- M : A, we have that > [[ D1 ]] = [[ D ]] = [[ D2 ]] > hence we have (1) (and I expect (2) as well). > > * I think this is not so trivial; however, this step is confirmed by the > theory of bidirectional typechecking. Quoting Dunfield and Krishnaswami > (2013): > >> As shown by Watkins et al. (2004), bidirectional typechecking can be > understood in terms of the normalization of intuitionistic type theory, in > which normal forms correspond to the checking mode of bidirectional > typechecking, and neutral (or atomic) terms correspond to the synthesis > mode. This enables a proof of the elegant property that type annotations > are only necessary at reducible expressions, and that normal forms need no > annotations at all. > > Dunfield and Krishnaswami (2013). Complete and Easy Bidirectional > Typechecking for Higher-Rank Polymorphism, ICFP 2013, ACM. > > > -- > Paolo G. Giarrusso - Ph.D. Student, T?bingen University > *http://ps.informatik.uni-tuebingen.de/team/giarrusso/ > * From p.giarrusso at gmail.com Sat Feb 4 09:29:08 2017 From: p.giarrusso at gmail.com (Paolo Giarrusso) Date: Sat, 4 Feb 2017 15:29:08 +0100 Subject: [TYPES] semantic coherence for simply typed lambda-calculus In-Reply-To: References: Message-ID: On 4 February 2017 at 13:32, Gabriel Scherer wrote: > Paolo, I had the exact same argument in mind, but I think that > beta-normal forms don't cut it when you have types of both > polarities. Consider for example the ?-normal form > > (match x with > | inj? () -> ?y.t > | inj? () -> ?y.t > ) (u) > > This does not satisfy the subformula property, as the principal type > of the "blocked" redex ((?y.t) u) is arbitrary. > > You need your notion of reduction to have enough commuting conversions > to recover the subformula property. A sequent-calculus presentation > gives this for free (there are ugly-but-simple sequent terms for this > calculus in my thesis manuscript, Section 4.1.4, > http://www.ccs.neu.edu/home/gasche/phd_thesis/scherer-thesis.pdf; > a proper abstract machine calculus would be more elegant), or looking > at cut-free focused term also does the job ? completeness of focusing > then embeds the suitable normalization procedure. Gabriel, thanks for the answer and fair point! Another approach is a suitable form of hereditary substitution?I recently learned from Mietek Bak & others it can do the job (amazingly to me), where match expressions are pushed out. I don't master the relation with the techniques you mentioned, but I do understand the appropriate syntax of normal forms. A definition of the appropriate syntax is here, for those familiar with Agda: https://github.com/mietek/hilbert-gentzen/blob/master/IPC/Syntax/GentzenSpinalNormalForm.agda (the rest of the repo also contains the normalization procedure). * *Another version is at https://github.com/gallais/potpourri/blob/master/agda/papers/hs99/STLCSum.agda, with a pointer to Short Proofs of Normalization by Joachimski & Matthes (1999). > On Sat, Feb 4, 2017 at 3:17 AM, Paolo Giarrusso wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> On Thursday, 2 February 2017, Paul B Levy wrote: >> >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >>> ] >>> >>> Dear all, >>> >>> Take simply typed lambda-calculus with ->, x, +, 0, 1 types. >>> Specifically the Curry-style formulation with no type annotations >>> whatsoever, neither on lambda nor on inl nor on anything else. >>> >>> Here are the two "coherence" statements I'm interested in. >>> >>> (1) Any two derivations of Gamma |- M : A have the same denotation. >>> >>> (2) More generally, for any bicartesian closed category C, any two >>> derivations of Gamma |- M : A have the same denotation in C. >>> >> >> To double-check: Gamma, M and A are all fixed, right? >> >> It seems one can remove the ambiguity in typing by normalizing M first and >> then relying on the subformula property. Here's a potential proof >> sketch?I'd love to know if this approach makes sense. (And I'm not even >> sure if all the steps I'm relying on have actually been proven). >> >> Use untyped normalization on M to obtain M'. Since M is typable, >> normalization terminates?even untyped normalization (right?), since types >> don't affect evaluation. >> By preservation, M' should have the same type (even though it's untyped >> evaluation, right?). By the subformula property of normalization, all types >> in the derivation of M' are "subformulas" of A so there is no ambiguity in >> its derivation of Gamma |- M' : A.* Let's call that derivation D. >> >> Since normalization preserves the denotation, if we have two derivations D1 >> and D2 of Gamma |- M : A, we have that >> [[ D1 ]] = [[ D ]] = [[ D2 ]] >> hence we have (1) (and I expect (2) as well). >> >> * I think this is not so trivial; however, this step is confirmed by the >> theory of bidirectional typechecking. Quoting Dunfield and Krishnaswami >> (2013): >> >>> As shown by Watkins et al. (2004), bidirectional typechecking can be >> understood in terms of the normalization of intuitionistic type theory, in >> which normal forms correspond to the checking mode of bidirectional >> typechecking, and neutral (or atomic) terms correspond to the synthesis >> mode. This enables a proof of the elegant property that type annotations >> are only necessary at reducible expressions, and that normal forms need no >> annotations at all. >> >> Dunfield and Krishnaswami (2013). Complete and Easy Bidirectional >> Typechecking for Higher-Rank Polymorphism, ICFP 2013, ACM. >> >> >> -- >> Paolo G. Giarrusso - Ph.D. Student, T?bingen University >> *http://ps.informatik.uni-tuebingen.de/team/giarrusso/ >> * -- Paolo G. Giarrusso - Ph.D. Student, T?bingen University http://ps.informatik.uni-tuebingen.de/team/giarrusso/ From andreas.abel at ifi.lmu.de Wed Feb 8 05:24:35 2017 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Wed, 8 Feb 2017 11:24:35 +0100 Subject: [TYPES] semantic coherence for simply typed lambda-calculus In-Reply-To: References: Message-ID: Hello Paul, I ran into the problem you describe when writing up my thesis, see http://www.cse.chalmers.se/~abela/diss.pdf The interesting part starts on page 34 in paragraph The remainder of this section is devoted to the proof that two well-kindedness derivations for the same constructors do not yield different semantics. More precisely, assume two derivations D :: ? ? F : ? and D' :: ?' ? F : ? and two valuations ? ? [[?]] and ?' ? [[?']]. If ?(X)= ?'(X) for all X ? FV(F), then [[D]]? =[[D']]?'. This result is not completely trivial, i. e., cannot be proven directly by induction on the derivations, since in derivations for non-?-normal F, some kinds in the middle of derivations can be canceled out. For example, consider F =(?X.Y)G. Some kind ? for X (and G) is mentioned in the middle of a well-kindness derivation of F, but it can differ from derivation to derivation. Still, the semantics of F in environment ? should be just ?(Y), independent of kind ?. The solution is the same. Start with normal forms and then show that the denotation is preserved by beta-expansion. The idea for this proof was from my supervisor Martin Hofmann. Best, Andreas On 04.02.2017 15:29, Paolo Giarrusso wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > On 4 February 2017 at 13:32, Gabriel Scherer wrote: >> Paolo, I had the exact same argument in mind, but I think that >> beta-normal forms don't cut it when you have types of both >> polarities. Consider for example the ?-normal form >> >> (match x with >> | inj? () -> ?y.t >> | inj? () -> ?y.t >> ) (u) >> >> This does not satisfy the subformula property, as the principal type >> of the "blocked" redex ((?y.t) u) is arbitrary. >> >> You need your notion of reduction to have enough commuting conversions >> to recover the subformula property. A sequent-calculus presentation >> gives this for free (there are ugly-but-simple sequent terms for this >> calculus in my thesis manuscript, Section 4.1.4, >> http://www.ccs.neu.edu/home/gasche/phd_thesis/scherer-thesis.pdf; >> a proper abstract machine calculus would be more elegant), or looking >> at cut-free focused term also does the job ? completeness of focusing >> then embeds the suitable normalization procedure. > > Gabriel, thanks for the answer and fair point! > > Another approach is a suitable form of hereditary substitution?I > recently learned from Mietek Bak & others it can do the job (amazingly > to me), where match expressions are pushed out. I don't master the > relation with the techniques you mentioned, but I do understand the > appropriate syntax of normal forms. > > A definition of the appropriate syntax is here, for those familiar with Agda: > https://github.com/mietek/hilbert-gentzen/blob/master/IPC/Syntax/GentzenSpinalNormalForm.agda > (the rest of the repo also contains the normalization procedure). * > > *Another version is at > https://github.com/gallais/potpourri/blob/master/agda/papers/hs99/STLCSum.agda, > with a pointer to > Short Proofs of Normalization by Joachimski & Matthes (1999). > >> On Sat, Feb 4, 2017 at 3:17 AM, Paolo Giarrusso wrote: >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >>> >>> On Thursday, 2 February 2017, Paul B Levy wrote: >>> >>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >>>> ] >>>> >>>> Dear all, >>>> >>>> Take simply typed lambda-calculus with ->, x, +, 0, 1 types. >>>> Specifically the Curry-style formulation with no type annotations >>>> whatsoever, neither on lambda nor on inl nor on anything else. >>>> >>>> Here are the two "coherence" statements I'm interested in. >>>> >>>> (1) Any two derivations of Gamma |- M : A have the same denotation. >>>> >>>> (2) More generally, for any bicartesian closed category C, any two >>>> derivations of Gamma |- M : A have the same denotation in C. >>>> >>> >>> To double-check: Gamma, M and A are all fixed, right? >>> >>> It seems one can remove the ambiguity in typing by normalizing M first and >>> then relying on the subformula property. Here's a potential proof >>> sketch?I'd love to know if this approach makes sense. (And I'm not even >>> sure if all the steps I'm relying on have actually been proven). >>> >>> Use untyped normalization on M to obtain M'. Since M is typable, >>> normalization terminates?even untyped normalization (right?), since types >>> don't affect evaluation. >>> By preservation, M' should have the same type (even though it's untyped >>> evaluation, right?). By the subformula property of normalization, all types >>> in the derivation of M' are "subformulas" of A so there is no ambiguity in >>> its derivation of Gamma |- M' : A.* Let's call that derivation D. >>> >>> Since normalization preserves the denotation, if we have two derivations D1 >>> and D2 of Gamma |- M : A, we have that >>> [[ D1 ]] = [[ D ]] = [[ D2 ]] >>> hence we have (1) (and I expect (2) as well). >>> >>> * I think this is not so trivial; however, this step is confirmed by the >>> theory of bidirectional typechecking. Quoting Dunfield and Krishnaswami >>> (2013): >>> >>>> As shown by Watkins et al. (2004), bidirectional typechecking can be >>> understood in terms of the normalization of intuitionistic type theory, in >>> which normal forms correspond to the checking mode of bidirectional >>> typechecking, and neutral (or atomic) terms correspond to the synthesis >>> mode. This enables a proof of the elegant property that type annotations >>> are only necessary at reducible expressions, and that normal forms need no >>> annotations at all. >>> >>> Dunfield and Krishnaswami (2013). Complete and Easy Bidirectional >>> Typechecking for Higher-Rank Polymorphism, ICFP 2013, ACM. >>> >>> >>> -- >>> Paolo G. Giarrusso - Ph.D. Student, T?bingen University >>> *http://ps.informatik.uni-tuebingen.de/team/giarrusso/ >>> * > > > -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www.cse.chalmers.se/~abela/ From xu at math.lmu.de Thu Apr 6 09:55:29 2017 From: xu at math.lmu.de (Chuangjie Xu) Date: Thu, 06 Apr 2017 15:55:29 +0200 Subject: [TYPES] Autumn school "Proof and Computation" Message-ID: <20170406155529.13472smo1ojqqj0x@webmail.mathematik.uni-muenchen.de> Autumn school "Proof and Computation" Herrsching, Germany, 23rd to 26th September 2017 http://www.mathematik.uni-muenchen.de/~schwicht/pc17.php An international autumn school "Proof and Computation" will be held from 23rd to 26th September 2017 at Haus der bayerischen Landwirtschaft Herrsching in Herrsching near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy. SCORE -------------------- - Predicative Foundations - Constructive Mathematics and Type Theory - Computation in Higher Types - Extraction of Programs from Proofs - Algorithmic Aspects in Financial Mathematics COURSES -------------------- - Mark Bickford on Constructive Analysis in NuPrl - Laura Crosilla on Foundations of Predicative Mathematics - Hajime Ishihara on Constructive Reverse Mathematics - Ulrich Kohlenbach on Proof Mining - Davide Rinaldi on Constructivising Transfinite Algebra - Andrei Rodin on Foundations of Axiomatic Mathematics - Gregor Svindland on Algorithmic Aspects in Financial Mathematics WORKING GROUPS -------------------- There will be an opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of constructing correct programs from proofs. APPLICATIONS -------------------- Graduate or PhD students and young postdoctoral researches are invited to apply. Applications must be accompanied by a letter of recommendation, preferably from the thesis adviser, and should be sent to Chuangjie Xu (xu at math.lmu.de). DEADLINE for applications: **30th May 2017**. Applicants will be notified by 30th June 2017. FINANCIAL SUPPORT -------------------- The workshop is supported by the Udo Keller Stiftung (Hamburg), the CID (Computing with Infinite Data) programme of the European Commission and a JSPS core-to-core project. Successful applicants will be offered full-board accommodation for the days of the autumn school. There are no funds, however, to reimburse travel or further expenses, which successful applicants will have to cover otherwise. Klaus Mainzer Peter Schuster Helmut Schwichtenberg ---------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program. From Guillaume.Munch at Inria.fr Thu May 4 12:09:11 2017 From: Guillaume.Munch at Inria.fr (Guillaume Munch-Maccagnoni) Date: Thu, 4 May 2017 18:09:11 +0200 Subject: [TYPES] semantic coherence for simply typed lambda-calculus In-Reply-To: References: Message-ID: Dear Paul, Since there was (several replies but) no answer to your question (asking for a reference), this may be of interest to the list. Our coherence theorem for Call-by-Push-Value from the paper in collaboration with M. Fiore and P.-L. Curien [1] extends to Curry's style with the help of a concise strong normalisation proof adapted from [2,3]. In this setting strong normalisation is essentially the completeness of focusing, so enough to reach the useful normal forms. This is written in the following short note: (section 6.5). It holds for any CBPV model (for any sensible interpretation including call-by-name and call-by-value) though you only asked for the case of BiCCCs (where the various sensible interpretations coincide). In Curry's style, it turns out, one has to be clear about how conversions are defined, since the notion of type-preserving conversion between terms does not coincide with that of conversion between derivations. For instance if x does not appear in M then (?x.M) * ? (?x.M) N preserves the typing whatever the type of N, but this does not correspond to a conversion between derivations if the type of x must change. A similar example involves the empty type instead of the unit type. But, using strong normalisation again one can prove that their equivalence closures are the same. This note substantiates Gabriel's and Paolo's good insights. Best regards, Guillaume [1] P.-L. Curien, M. Fiore, and G. MM, ?A Theory of Effects and Resources: Adjunction Models and Polarised Calculi?, in Proc. POPL, 2016. [2] G. MM, ?Focalisation and Classical Realisability?, in Proc. CSL, 2009. [3] G. MM, ??-calcul, machines et orthogonalit??, manuscript, June 2012. Le 02/02/2017 ? 20:11, Paul B Levy a ?crit : > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear all, > > Take simply typed lambda-calculus with ->, x, +, 0, 1 types. > Specifically the Curry-style formulation with no type annotations > whatsoever, neither on lambda nor on inl nor on anything else. > > Here are the two "coherence" statements I'm interested in. > > (1) Any two derivations of Gamma |- M : A have the same denotation. > > (2) More generally, for any bicartesian closed category C, any two > derivations of Gamma |- M : A have the same denotation in C. > > I can see roughly how to prove these, but before working it out would > like to ask: do these results appear in the literature? My impression > is that people have studied semantic coherence for fancy languages (e.g. > with subtypes and dependent types), so surely the above statements, or > at least (1), are a simple case of some result in the literature. > > Best regards, > Paul > > > -- Guillaume Munch-Maccagnoni Researcher at Inria Bretagne Atlantique Team Gallinette From huohuohuomumu at gmail.com Mon Jun 26 10:51:48 2017 From: huohuohuomumu at gmail.com (Yanlin Wang) Date: Mon, 26 Jun 2017 07:51:48 -0700 (PDT) Subject: [TYPES] Any formal models of method lookup mechanism in C++? Message-ID: <36BD8FDE-58C8-4974-9B27-AF9DAEE81F3C@gmail.com> Dear all, I am formalizing a C++-like multiple inheritance model, please look at this piece of code: //g++ 5.4.0#include class Deck { public: virtual void draw () { std::cout << "Deck::draw" << std::endl; } virtual void shuffleAndDraw () { std::cout << "Deck::shuffle" << std::endl; draw(); }};class LDeck : public Deck { public: virtual void draw () { std::cout << "L::draw" << std::endl; }};class Paint { public: virtual void draw () { std::cout << "Paint::draw" << std::endl; }};class Top : public LDeck, public Paint {};int main(){ Top b; Top *a = &b; a->shuffleAndDraw();//shuffle and Ldraw a->Deck::draw(); //draw a->Paint::draw();//paint ((Deck*)a)->draw();//LDraw ((Paint*)a)->draw();//paint return 0;} For resolving the method call ? ((Deck*)a)->draw()?, C++ uses both the static (Deck) and dynamic(Top) type information of object a, so that the method call ?draw()? dispatches to LDeck::draw().? I was wondering whether there are any formal models that describes this method lookup mechanism in C++. If anyone knows, could you please let me know? Thank you! Best regards, Yanlin Wang From delesley at gmail.com Mon Jun 26 13:10:52 2017 From: delesley at gmail.com (DeLesley Hutchins) Date: Mon, 26 Jun 2017 10:10:52 -0700 Subject: [TYPES] Any formal models of method lookup mechanism in C++? In-Reply-To: <36BD8FDE-58C8-4974-9B27-AF9DAEE81F3C@gmail.com> References: <36BD8FDE-58C8-4974-9B27-AF9DAEE81F3C@gmail.com> Message-ID: I'm not aware of any existing models; formalizing C++ in its entirety is borderline-hopeless. Method lookup in C++ is extremely complicated. In the simple case, it depends on the name of the method, the number and types of arguments (including const), any visible type implicit type conversions, and whether arguments can be considered l-value or r-value references. Once you add templates and operator overloading, search can expand to the namespaces in which the argument types are declared, and you have to take template specializations and various type equivalence and pattern matching rules into account. Inheriting from a template also disables many forms of lookup. Formalizing all that will be a real challenge. However, all of that complexity is on the static side, and the end result is that the compiler selects a method declaration which, for linking purposes, must have a unique mangled name. In a formal model, you could potentially rely on the mangled name to identify methods, and assume that all template instantiation has already occurred, which would bypass most of the mess. Virtual methods cannot be templatized. The dynamic dispatch is comparatively trivial, being simple single-dispatch with manual resolution of any MI ambiguities; your main challenge will be formalizing the virtual/non-virtual inheritance distinction. On Mon, Jun 26, 2017 at 7:51 AM, Yanlin Wang wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear all, > > > I am formalizing a C++-like multiple inheritance model, please look at > this piece of code: > > > //g++ 5.4.0#include class Deck { public: virtual void > draw () { > std::cout << "Deck::draw" << std::endl; > } virtual void shuffleAndDraw () { > std::cout << "Deck::shuffle" << std::endl; draw(); > }};class LDeck : public Deck { public: > virtual void draw () { > std::cout << "L::draw" << std::endl; > }};class Paint { public: > virtual void draw () { > std::cout << "Paint::draw" << std::endl; > }};class Top : public LDeck, public Paint {};int main(){ Top > b; Top *a = &b; a->shuffleAndDraw();//shuffle and Ldraw > a->Deck::draw(); //draw a->Paint::draw();//paint > ((Deck*)a)->draw();//LDraw ((Paint*)a)->draw();//paint return 0;} > > > > > For resolving the method call ? ((Deck*)a)->draw()?, C++ uses both the > static (Deck) and dynamic(Top) type information of object a, so that the > method call ?draw()? dispatches to LDeck::draw(). > > > I was wondering whether there are any formal models that describes this > method lookup mechanism in C++. If anyone knows, could you please let me > know? Thank you! > > > Best regards, > Yanlin Wang > > > > From gabriel.scherer at gmail.com Mon Jun 26 13:51:50 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Mon, 26 Jun 2017 13:51:50 -0400 Subject: [TYPES] Any formal models of method lookup mechanism in C++? In-Reply-To: <36BD8FDE-58C8-4974-9B27-AF9DAEE81F3C@gmail.com> References: <36BD8FDE-58C8-4974-9B27-AF9DAEE81F3C@gmail.com> Message-ID: My entry point to the "formalizing C++" litterature is Tahina Ramananandro's PhD thesis work, which does model (multiple) inheritance and casts, but focuses in particular on object initialization/destruction and object layout -- formalized in Coq. Mechanized Formal Semantics and Verified Compilation for C++ Objects Tahina Ramananandro, 2011 http://gallium.inria.fr/~tramanan/cpp/ It contains a nice "Related Work" section mention several earlier works on C++ inheritance and casts, and in particular builds upon Daniel Wasserab's 2010 thesis (formalized in Isabelle) and the corresponding conference article An operational semantics and type safety proof for multiple inheritance in C++ Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, and Frank Tip 2006 and Michael Norrish's more complete HOL formalization A Formal Semantics for C++ Michael Norrish. 2008 On Mon, Jun 26, 2017 at 10:51 AM, Yanlin Wang wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear all, > > > I am formalizing a C++-like multiple inheritance model, please look at this piece of code: > > > //g++ 5.4.0#include class Deck { public: virtual void draw () { > std::cout << "Deck::draw" << std::endl; > } virtual void shuffleAndDraw () { > std::cout << "Deck::shuffle" << std::endl; draw(); }};class LDeck : public Deck { public: > virtual void draw () { > std::cout << "L::draw" << std::endl; > }};class Paint { public: > virtual void draw () { > std::cout << "Paint::draw" << std::endl; > }};class Top : public LDeck, public Paint {};int main(){ Top b; Top *a = &b; a->shuffleAndDraw();//shuffle and Ldraw a->Deck::draw(); //draw a->Paint::draw();//paint ((Deck*)a)->draw();//LDraw ((Paint*)a)->draw();//paint return 0;} > > > > > For resolving the method call ? ((Deck*)a)->draw()?, C++ uses both the static (Deck) and dynamic(Top) type information of object a, so that the method call ?draw()? dispatches to LDeck::draw(). > > > I was wondering whether there are any formal models that describes this method lookup mechanism in C++. If anyone knows, could you please let me know? Thank you! > > > Best regards, > Yanlin Wang > > > From wand at ccs.neu.edu Mon Jun 26 14:24:50 2017 From: wand at ccs.neu.edu (Mitchell Wand) Date: Mon, 26 Jun 2017 14:24:50 -0400 Subject: [TYPES] Any formal models of method lookup mechanism in C++? In-Reply-To: References: <36BD8FDE-58C8-4974-9B27-AF9DAEE81F3C@gmail.com> Message-ID: Don't know if it's helpful, but here's another reference... --Mitch Jonathan~G. Rossie, Daniel~P. Friedman, and Mitchell Wand. Modeling Subobject-based Inheritance. In Pierre Cointe, editor, *Proc. European Conference on Object-Oriented Programming*, volume 1098 of *Lecture Notes in Computer Science*, pages 248--274, Berlin, Heidelberg, and New York, July 1996. Springer-Verlag. On Mon, Jun 26, 2017 at 1:51 PM, Gabriel Scherer wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > My entry point to the "formalizing C++" litterature is Tahina > Ramananandro's PhD thesis work, which does model (multiple) > inheritance and casts, but focuses in particular on object > initialization/destruction and object layout -- formalized in Coq. > > Mechanized Formal Semantics and Verified Compilation for C++ Objects > Tahina Ramananandro, 2011 > http://gallium.inria.fr/~tramanan/cpp/ > > It contains a nice "Related Work" section mention several earlier > works on C++ inheritance and casts, and in particular builds upon > Daniel Wasserab's 2010 thesis (formalized in Isabelle) and the > corresponding conference article > > An operational semantics and type safety proof for multiple inheritance > in C++ > Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, and Frank Tip > 2006 > > and Michael Norrish's more complete HOL formalization > > A Formal Semantics for C++ > Michael Norrish. > 2008 > > > On Mon, Jun 26, 2017 at 10:51 AM, Yanlin Wang > wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list ] > > > > Dear all, > > > > > > I am formalizing a C++-like multiple inheritance model, please look at > this piece of code: > > > > > > //g++ 5.4.0#include class Deck { public: virtual > void draw () { > > std::cout << "Deck::draw" << std::endl; > > } virtual void shuffleAndDraw () { > > std::cout << "Deck::shuffle" << std::endl; draw(); > }};class LDeck : public Deck { public: > > virtual void draw () { > > std::cout << "L::draw" << std::endl; > > }};class Paint { public: > > virtual void draw () { > > std::cout << "Paint::draw" << std::endl; > > }};class Top : public LDeck, public Paint {};int main(){ Top > b; Top *a = &b; a->shuffleAndDraw();//shuffle and Ldraw > a->Deck::draw(); //draw a->Paint::draw();//paint > ((Deck*)a)->draw();//LDraw ((Paint*)a)->draw();//paint return 0;} > > > > > > > > > > For resolving the method call ? ((Deck*)a)->draw()?, C++ uses both the > static (Deck) and dynamic(Top) type information of object a, so that the > method call ?draw()? dispatches to LDeck::draw(). > > > > > > I was wondering whether there are any formal models that describes this > method lookup mechanism in C++. If anyone knows, could you please let me > know? Thank you! > > > > > > Best regards, > > Yanlin Wang > > > > > > > From wadler at inf.ed.ac.uk Mon Jul 3 14:04:20 2017 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Mon, 3 Jul 2017 19:04:20 +0100 Subject: [TYPES] What are congruence rules called? Message-ID: Reduction for the simply-typed call-by-value lambda calculus consists of the ? rule, (?x.N)V ? N[x:=V] and the congruence rules L ? L? ------------ L M ? L? M M ? M? ------------ V M ? V M? Question: Is there a standard greek letter for naming the congruence rules, such as ? or ?? Or any other relevant naming convention? Cheers, -- P . \ Philip Wadler, Professor of Theoretical Computer Science . /\ School of Informatics, University of Edinburgh . / \ http://homepages.inf.ed.ac.uk/wadler/ -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: not available URL: From sestini.filippo at gmail.com Tue Jul 4 05:59:29 2017 From: sestini.filippo at gmail.com (Filippo Sestini) Date: Tue, 4 Jul 2017 11:59:29 +0200 Subject: [TYPES] What are congruence rules called? In-Reply-To: References: Message-ID: Hello, Not really that common in literature, but in Hindley and Selding?s book, Lambda Calculus and Combinators, they use respectively ? and ? to name those congruence rules, both in the untyped and the typed case. They claim to have taken that from Curry & Feys. Best regards -- Filippo Sestini sestini.filippo at gmail.com (+39) 333 6757668 > On Jul 3, 2017, at 8:04 PM, Philip Wadler wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Reduction for the simply-typed call-by-value lambda calculus consists of > the ? rule, > > (?x.N)V ? N[x:=V] > > and the congruence rules > > L ? L? > ------------ > L M ? L? M > > M ? M? > ------------ > V M ? V M? > > Question: Is there a standard greek letter for naming the congruence rules, > such as ? or ?? Or any other relevant naming convention? > > Cheers, -- P > > > . \ 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 francesco.gavazzo at gmail.com Tue Jul 4 06:21:03 2017 From: francesco.gavazzo at gmail.com (Francesco Gavazzo) Date: Tue, 4 Jul 2017 12:21:03 +0200 Subject: [TYPES] What are congruence rules called? In-Reply-To: References: Message-ID: Dear Philip, In Curry's Combinatory Logic, Volume I (section 2D) congruence rules are labeled with greek letters. I do not know whether this is the satandard notation, but I am sure I occasionally met the same notation in other books/papers. All the best, Francesco Gavazzo 2017-07-03 20:04 GMT+02:00 Philip Wadler : > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > > Reduction for the simply-typed call-by-value lambda calculus consists of > the ? rule, > > (?x.N)V ? N[x:=V] > > and the congruence rules > > L ? L? > ------------ > L M ? L? M > > M ? M? > ------------ > V M ? V M? > > Question: Is there a standard greek letter for naming the congruence rules, > such as ? or ?? Or any other relevant naming convention? > > Cheers, -- P > > > . \ 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 hindley at waitrose.com Tue Jul 4 10:28:31 2017 From: hindley at waitrose.com (J. R. Hindley) Date: Tue, 4 Jul 2017 15:28:31 +0100 Subject: [TYPES] What are congruence rules called? In-Reply-To: References: Message-ID: <774528BB-0B4E-45B6-8888-E04A4CA05C4C@waitrose.com> Hi Phil, Francesco and Filippo, Yes, as Filippo and Francesco say, Greek names were first proposed for these two rules by Curry. He proposed $\nu$ for the first rule and $\mu$ for the second. ("Combinatory Logic" Volume 1 p. 59.) (Perhaps Curry also used them in one of his pre-1940 papers; I forget now.) Happy summer! Yours, Roger Hindley ---------------- On 3 Jul 2017, at 19:04, Philip Wadler wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Reduction for the simply-typed call-by-value lambda calculus consists of > the ? rule, > > (?x.N)V ? N[x:=V] > > and the congruence rules > > L ? L? > ------------ > L M ? L? M > > M ? M? > ------------ > V M ? V M? > > Question: Is there a standard greek letter for naming the congruence rules, > such as ? or ?? Or any other relevant naming convention? > > Cheers, -- P > > > . \ 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 wadler at inf.ed.ac.uk Tue Jul 4 11:15:13 2017 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Tue, 4 Jul 2017 16:15:13 +0100 Subject: [TYPES] What are congruence rules called? In-Reply-To: <774528BB-0B4E-45B6-8888-E04A4CA05C4C@waitrose.com> References: <774528BB-0B4E-45B6-8888-E04A4CA05C4C@waitrose.com> Message-ID: Darn. Just as there are (possibly many) \beta rules at each type (e.g., \beta\arrow, \beta\times, \beta+_1, \beta+_2), I was hoping to have a single greek letter for congruence rules, possibly with more than one at each type. I was going to use \gamma\arrow_1, \gamma\arrow_2 for the two congruence rules I gave, but wondered if there was a more traditional choice than \gamma. Using either \mu or \nu seems problematic, since (like \lambda) these often appear as binding operators in terms. Thank you for the information! Cheers, -- P . \ Philip Wadler, Professor of Theoretical Computer Science . /\ School of Informatics, University of Edinburgh . / \ http://homepages.inf.ed.ac.uk/wadler/ On 4 July 2017 at 15:28, J. R. Hindley wrote: > Hi Phil, Francesco and Filippo, > > Yes, as Filippo and Francesco say, Greek names were first proposed for > these two rules by Curry. He proposed > $\nu$ for the first rule and $\mu$ for the second. ("Combinatory Logic" > Volume 1 p. 59.) > > (Perhaps Curry also used them in one of his pre-1940 papers; I forget now.) > > Happy summer! > Yours, Roger Hindley > > ---------------- > On 3 Jul 2017, at 19:04, Philip Wadler wrote: > > > [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list ] > > > > Reduction for the simply-typed call-by-value lambda calculus consists of > > the ? rule, > > > > (?x.N)V ? N[x:=V] > > > > and the congruence rules > > > > L ? L? > > ------------ > > L M ? L? M > > > > M ? M? > > ------------ > > V M ? V M? > > > > Question: Is there a standard greek letter for naming the congruence > rules, > > such as ? or ?? Or any other relevant naming convention? > > > > Cheers, -- P > > > > > > . \ 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. > > > -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: not available URL: From gabriel.scherer at gmail.com Tue Jul 4 12:09:38 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Tue, 4 Jul 2017 12:09:38 -0400 Subject: [TYPES] What are congruence rules called? In-Reply-To: References: <774528BB-0B4E-45B6-8888-E04A4CA05C4C@waitrose.com> Message-ID: In your 2003 paper "Call-by-value is dual to call-by-name", you use ? (\varsigma) for a rule that brings a subterm under an evaluation context to the head of the term -- this is a sequent calculus so the operational semantics is more like abstract machines than lambda terms. Guillaume Munch-Maccagnoni reused this letter, starting in "Focalisation and Classical Realisability", 2009, for rules that bring the head focus into reducible subterms, but his presentation does it in a more atomic way, with a family of rules for each connective. A non-deterministic presentation of these rules would be <(t, t') | u> ??(?)? > <(t', t) | u> ??(?)? > ??(?)? > ??(?)? > etc. (when t is not a value) I think it would be reasonable to name lambda-term congruence rules in the same way. They directly reduce a subterm instead of bringing it in head position in an abstract machine, but they are similar. Aside: note that these confluence rules may not be the most flexible way to describe reduction. If you want to describe parallel reduction (for a confluence proof for example), you need to give different rules. Both can be subsumed by defining multi-hole contexts E[??, ??, ..., ??], and having a single confluence rule over those; various flavors of parallel reduction, as well as the standard reduction, arise as special cases. Didier R?my and I used this presentation in "Full reduction in the face of absurdity", 2015. From nr at cs.tufts.edu Tue Jul 4 12:29:41 2017 From: nr at cs.tufts.edu (Norman Ramsey) Date: Tue, 04 Jul 2017 12:29:41 -0400 Subject: [TYPES] What are congruence rules called? In-Reply-To: (sfid-H-20170704-054022-+22.99-1@multi.osbf.lua) References: (sfid-H-20170704-054022-+22.99-1@multi.osbf.lua) Message-ID: <20170704162941.874947813BD@labrador.cs.tufts.edu> > Question: Is there a standard greek letter for naming the congruence rules, > such as ? or ?? Or any other relevant naming convention? In his January 2015 notes on lambda calculus, Prakash Panangaden uses ?, ?, and ? for congruence rules. Perhaps he can comment on sources? Norman From andru at cs.cornell.edu Tue Jul 4 13:44:48 2017 From: andru at cs.cornell.edu (Andrew Myers) Date: Tue, 04 Jul 2017 13:44:48 -0400 Subject: [TYPES] What are congruence rules called? Message-ID: <7jm53oxht1m6ixe1iiqa2g5p.1499189634080@email.android.com> Having a consistent way to name congruence rules is appealing, but since they are generated from the structure of terms, wouldn't it be better to index their names by the name of the syntactic form and the location of the relevant subterm rather than by types? E.g., App-1, App-2. That approach seems to scale more easily and clearly once you get beyond the lambda calculus. -- Andrew -------- Original message -------- From: Philip Wadler Date: 7/4/17 11:15 (GMT-05:00) To: "J. R. Hindley" Cc: Types list Subject: Re: [TYPES] What are congruence rules called? [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Darn. Just as there are (possibly many) \beta rules at each type (e.g., \beta\arrow, \beta\times, \beta+_1, \beta+_2), I was hoping to have a single greek letter for congruence rules, possibly with more than one at each type. I was going to use \gamma\arrow_1, \gamma\arrow_2 for the two congruence rules I gave, but wondered if there was a more traditional choice than \gamma. Using either \mu or \nu seems problematic, since (like \lambda) these often appear as binding operators in terms. Thank you for the information! Cheers, -- P .?? \ Philip Wadler, Professor of Theoretical Computer Science .?? /\ School of Informatics, University of Edinburgh .? /? \ http://homepages.inf.ed.ac.uk/wadler/ On 4 July 2017 at 15:28, J. R. Hindley wrote: > Hi Phil, Francesco and Filippo, > > Yes, as Filippo and Francesco say, Greek names were first proposed for > these two rules by Curry. He proposed > $\nu$ for the first rule and $\mu$ for the second.? ("Combinatory Logic" > Volume 1 p. 59.) > > (Perhaps Curry also used them in one of his pre-1940 papers; I forget now.) > > Happy summer! >? Yours, Roger Hindley > > ---------------- > On 3 Jul 2017, at 19:04, Philip Wadler wrote: > > > [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list ] > > > > Reduction for the simply-typed call-by-value lambda calculus consists of > > the ? rule, > > > >? (?x.N)V ? N[x:=V] > > > > and the congruence rules > > > >? L ? L? > >? ------------ > >? L M ? L? M > > > >? M ? M? > >? ------------ > >? V M ? V M? > > > > Question: Is there a standard greek letter for naming the congruence > rules, > > such as ? or ?? Or any other relevant naming convention? > > > > Cheers, -- P > > > > > > .?? \ 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. > > > The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. From wadler at inf.ed.ac.uk Fri Jul 7 13:02:07 2017 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Fri, 7 Jul 2017 18:02:07 +0100 Subject: [TYPES] What are congruence rules called? In-Reply-To: References: Message-ID: Thank you to all for the many suggestions, and to Vincent for pointing out that 'congruence' should perhaps be called 'compatibility'. Yours, -- P . \ Philip Wadler, Professor of Theoretical Computer Science . /\ School of Informatics, University of Edinburgh . / \ http://homepages.inf.ed.ac.uk/wadler/ On 3 July 2017 at 19:04, Philip Wadler wrote: > Reduction for the simply-typed call-by-value lambda calculus consists of > the ? rule, > > (?x.N)V ? N[x:=V] > > and the congruence rules > > L ? L? > ------------ > L M ? L? M > > M ? M? > ------------ > V M ? V M? > > Question: Is there a standard greek letter for naming the congruence rules, > such as ? or ?? Or any other relevant naming convention? > > Cheers, -- P > > > . \ Philip Wadler, Professor of Theoretical Computer Science > . /\ School of Informatics, University of Edinburgh > . / \ http://homepages.inf.ed.ac.uk/wadler/ > -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: not available URL: From andreas.abel at ifi.lmu.de Sat Jul 8 12:47:16 2017 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Sat, 8 Jul 2017 17:47:16 +0100 Subject: [TYPES] What are congruence rules called? In-Reply-To: <7jm53oxht1m6ixe1iiqa2g5p.1499189634080@email.android.com> References: <7jm53oxht1m6ixe1iiqa2g5p.1499189634080@email.android.com> Message-ID: <910e4d63-fe19-c0ac-8566-c971bdf1c6bd@ifi.lmu.de> On 04.07.2017 18:44, Andrew Myers wrote: > Having a consistent way to name congruence rules is appealing, but since they are generated from the structure of terms, wouldn't it be better to index their names by the name of the syntactic form and the location of the relevant subterm rather than by types? E.g., App-1, App-2. That approach seems to scale more easily and clearly once you get beyond the lambda calculus. > -- Andrew +1. That sounds most reasonable. > -------- Original message -------- > From: Philip Wadler > Date: 7/4/17 11:15 (GMT-05:00) > To: "J. R. Hindley" > Cc: Types list > Subject: Re: [TYPES] What are congruence rules called? > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > Darn. Just as there are (possibly many) \beta rules at each type (e.g., > \beta\arrow, \beta\times, \beta+_1, \beta+_2), I was hoping to have a > single greek letter for congruence rules, possibly with more than one at > each type. I was going to use \gamma\arrow_1, \gamma\arrow_2 for the two > congruence rules I gave, but wondered if there was a more traditional > choice than \gamma. Using either \mu or \nu seems problematic, since (like > \lambda) these often appear as binding operators in terms. Thank you for > the information! Cheers, -- P > > . \ Philip Wadler, Professor of Theoretical Computer Science > . /\ School of Informatics, University of Edinburgh > . / \ http://homepages.inf.ed.ac.uk/wadler/ > > On 4 July 2017 at 15:28, J. R. Hindley wrote: > >> Hi Phil, Francesco and Filippo, >> >> Yes, as Filippo and Francesco say, Greek names were first proposed for >> these two rules by Curry. He proposed >> $\nu$ for the first rule and $\mu$ for the second. ("Combinatory Logic" >> Volume 1 p. 59.) >> >> (Perhaps Curry also used them in one of his pre-1940 papers; I forget now.) >> >> Happy summer! >> Yours, Roger Hindley >> >> ---------------- >> On 3 Jul 2017, at 19:04, Philip Wadler wrote: >> >>> [ The Types Forum, http://lists.seas.upenn.edu/ >> mailman/listinfo/types-list ] >>> >>> Reduction for the simply-typed call-by-value lambda calculus consists of >>> the ? rule, >>> >>> (?x.N)V ? N[x:=V] >>> >>> and the congruence rules >>> >>> L ? L? >>> ------------ >>> L M ? L? M >>> >>> M ? M? >>> ------------ >>> V M ? V M? >>> >>> Question: Is there a standard greek letter for naming the congruence >> rules, >>> such as ? or ?? Or any other relevant naming convention? >>> >>> Cheers, -- P >>> >>> >>> . \ 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. >> >> >> > > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www.cse.chalmers.se/~abela/ From beta.ziliani at gmail.com Sun Jul 9 15:14:43 2017 From: beta.ziliani at gmail.com (Beta Ziliani) Date: Sun, 9 Jul 2017 16:14:43 -0300 Subject: [TYPES] What are congruence rules called? In-Reply-To: <7jm53oxht1m6ixe1iiqa2g5p.1499189634080@email.android.com> References: <7jm53oxht1m6ixe1iiqa2g5p.1499189634080@email.android.com> Message-ID: I second Andrew. Don't ask me where, but I've seen also "App-L" and "App-R", and "@_l" and "@_r" (the later for a system with an explicit app operator @). My 1ct. On Tue, Jul 4, 2017 at 2:44 PM, Andrew Myers wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > > > Having a consistent way to name congruence rules is appealing, but since > they are generated from the structure of terms, wouldn't it be better to > index their names by the name of the syntactic form and the location of the > relevant subterm rather than by types? E.g., App-1, App-2. That approach > seems to scale more easily and clearly once you get beyond the lambda > calculus. > -- Andrew > > -------- Original message -------- > From: Philip Wadler > Date: 7/4/17 11:15 (GMT-05:00) > To: "J. R. Hindley" > Cc: Types list > Subject: Re: [TYPES] What are congruence rules called? > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > > Darn. Just as there are (possibly many) \beta rules at each type (e.g., > \beta\arrow, \beta\times, \beta+_1, \beta+_2), I was hoping to have a > single greek letter for congruence rules, possibly with more than one at > each type. I was going to use \gamma\arrow_1, \gamma\arrow_2 for the two > congruence rules I gave, but wondered if there was a more traditional > choice than \gamma. Using either \mu or \nu seems problematic, since (like > \lambda) these often appear as binding operators in terms. Thank you for > the information! Cheers, -- P > > . \ Philip Wadler, Professor of Theoretical Computer Science > . /\ School of Informatics, University of Edinburgh > . / \ http://homepages.inf.ed.ac.uk/wadler/ > > On 4 July 2017 at 15:28, J. R. Hindley wrote: > > > Hi Phil, Francesco and Filippo, > > > > Yes, as Filippo and Francesco say, Greek names were first proposed for > > these two rules by Curry. He proposed > > $\nu$ for the first rule and $\mu$ for the second. ("Combinatory Logic" > > Volume 1 p. 59.) > > > > (Perhaps Curry also used them in one of his pre-1940 papers; I forget > now.) > > > > Happy summer! > > Yours, Roger Hindley > > > > ---------------- > > On 3 Jul 2017, at 19:04, Philip Wadler wrote: > > > > > [ The Types Forum, http://lists.seas.upenn.edu/ > > mailman/listinfo/types-list ] > > > > > > Reduction for the simply-typed call-by-value lambda calculus consists > of > > > the ? rule, > > > > > > (?x.N)V ? N[x:=V] > > > > > > and the congruence rules > > > > > > L ? L? > > > ------------ > > > L M ? L? M > > > > > > M ? M? > > > ------------ > > > V M ? V M? > > > > > > Question: Is there a standard greek letter for naming the congruence > > rules, > > > such as ? or ?? Or any other relevant naming convention? > > > > > > Cheers, -- P > > > > > > > > > . \ 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. > > > > > > > > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > From yangyp at connect.hku.hk Wed Aug 23 04:21:31 2017 From: yangyp at connect.hku.hk (Yang, Yanpeng) Date: Wed, 23 Aug 2017 16:21:31 +0800 Subject: [TYPES] Is one-step conversion rule of CC equivalent to the multi-step one? Message-ID: Dear all, The conversion rule of the Calculus of Constructions (CC) is usually defined as follows: G |- e : A G |- A : s A ==beta B ------------------- Conv G |- e : B I wonder if this rule is equivalent to the one using *one-step* beta reduction: G |- e : A G |- A : s A --> B \/ B --> A -------------------------- Conv-Step G |- e : B This "Conv-Step" rule is shown in Geuvers' paper [1, Definition 4.1] but which never mentions if it is equivalent to the original "Conv" rule. So, my question is: has it ever been proved that the two conversion rules are equivalent? If so, what is the appropriate article to refer to for this proof? Thanks a lot! Sincerely, Yanpeng [1] Geuvers, Herman. "A short and flexible proof of Strong Normalization for the Calculus of Constructions." International Workshop on Types for Proofs and Programs. Springer, Berlin, Heidelberg, 1994. URL: http://flint.cs.yale.edu/trifonov/cs629/Geuvers-SN-CC-2up.ps From jamesbkoppel at yahoo.com Wed Aug 23 20:24:15 2017 From: jamesbkoppel at yahoo.com (James Koppel) Date: Wed, 23 Aug 2017 20:24:15 -0400 Subject: [TYPES] Is one-step conversion rule of CC equivalent to the multi-step one? In-Reply-To: References: Message-ID: Beta equivalence is the reflexive symmetric transitive closure of one-step beta reduction. Every pair of beta-equivalent terms is witnessed by a chain of zero or more one-step beta reductions or inverse one-step beta reductions. That immediately implies that every use of the Conv rule could be replaced by zero or more uses of the Conv-Step rule. That is, unless it's somehow possible for one of the intermediate terms to be ill-typed (i.e.: fail the A : s condition). Presumably not doing so is a prerequisite to having beta-reduction be well-defined. On Wed, Aug 23, 2017 at 4:21 AM, Yang, Yanpeng wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear all, > > The conversion rule of the Calculus of Constructions (CC) is usually > defined as follows: > > G |- e : A > G |- A : s > A ==beta B > ------------------- Conv > G |- e : B > > I wonder if this rule is equivalent to the one using *one-step* beta > reduction: > > G |- e : A > G |- A : s > A --> B \/ B --> A > -------------------------- Conv-Step > G |- e : B > > This "Conv-Step" rule is shown in Geuvers' paper [1, Definition 4.1] but > which never mentions if it is equivalent to the original "Conv" rule. > > So, my question is: has it ever been proved that the two conversion rules > are equivalent? If so, what is the appropriate article to refer to for this > proof? > > Thanks a lot! > > Sincerely, > Yanpeng > > [1] Geuvers, Herman. "A short and flexible proof of Strong Normalization > for the Calculus of Constructions." International Workshop on Types for > Proofs and Programs. Springer, Berlin, Heidelberg, 1994. > URL: http://flint.cs.yale.edu/trifonov/cs629/Geuvers-SN-CC-2up.ps > From christian.doczkal at ens-lyon.fr Thu Aug 24 05:08:38 2017 From: christian.doczkal at ens-lyon.fr (Christian Doczkal) Date: Thu, 24 Aug 2017 11:08:38 +0200 Subject: [TYPES] Is one-step conversion rule of CC equivalent to the multi-step one? In-Reply-To: References: Message-ID: <49290b71-0a3f-eb7c-a4b2-6e6c23bcf321@ens-lyon.fr> This is fairly close to the question whether the presentation of CC using (typed) judgmental equality is equivalent to the presentation of CC with (untyped) conversion. This was answered positively for a large class of pure type systems by Siles & Herbelin [1]. Their work encompasses CC, but there is previous work, some of which might also encompass CC. Regards, Christian [1] Vincent Siles, Hugo Herbelin: Pure Type System conversion is always typable. J. Funct. Program. 22(2): 153-180 (2012) https://doi.org/10.1017/S0956796812000044 On 08/24/2017 02:24 AM, James Koppel wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Beta equivalence is the reflexive symmetric transitive closure of one-step > beta reduction. Every pair of beta-equivalent terms is witnessed by a chain > of zero or more one-step beta reductions or inverse one-step beta > reductions. That immediately implies that every use of the Conv rule could > be replaced by zero or more uses of the Conv-Step rule. > > That is, unless it's somehow possible for one of the intermediate terms to > be ill-typed (i.e.: fail the A : s condition). Presumably not doing so is a > prerequisite to having beta-reduction be well-defined. > > On Wed, Aug 23, 2017 at 4:21 AM, Yang, Yanpeng > wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> ] >> >> Dear all, >> >> The conversion rule of the Calculus of Constructions (CC) is usually >> defined as follows: >> >> G |- e : A >> G |- A : s >> A ==beta B >> ------------------- Conv >> G |- e : B >> >> I wonder if this rule is equivalent to the one using *one-step* beta >> reduction: >> >> G |- e : A >> G |- A : s >> A --> B \/ B --> A >> -------------------------- Conv-Step >> G |- e : B >> >> This "Conv-Step" rule is shown in Geuvers' paper [1, Definition 4.1] but >> which never mentions if it is equivalent to the original "Conv" rule. >> >> So, my question is: has it ever been proved that the two conversion rules >> are equivalent? If so, what is the appropriate article to refer to for this >> proof? >> >> Thanks a lot! >> >> Sincerely, >> Yanpeng >> >> [1] Geuvers, Herman. "A short and flexible proof of Strong Normalization >> for the Calculus of Constructions." International Workshop on Types for >> Proofs and Programs. Springer, Berlin, Heidelberg, 1994. >> URL: http://flint.cs.yale.edu/trifonov/cs629/Geuvers-SN-CC-2up.ps >> From yangyp at connect.hku.hk Thu Aug 24 06:10:54 2017 From: yangyp at connect.hku.hk (Yang, Yanpeng) Date: Thu, 24 Aug 2017 18:10:54 +0800 Subject: [TYPES] Is one-step conversion rule of CC equivalent to the multi-step one? In-Reply-To: <99D64430-9FA6-47B6-A6B4-05741AE0E09A@exmail.nottingham.ac.uk> References: <99D64430-9FA6-47B6-A6B4-05741AE0E09A@exmail.nottingham.ac.uk> Message-ID: Dear James and Thorsten, Thanks a lot for your replies! I feel sorry that there is a typo in rules that I presented in my first email, as pointed by Thorsten's reply. The second premise should be "G |- B : s" instead of "G |- A : s", as the latter one is usually admissible by the lemma "Correctness of Types". The following discussion is based on the corrected rules: G |- e : A G |- B : s # Should be B here A ==beta B ------------------- Conv G |- e : B G |- e : A G |- B : s # Should be B here A --> B \/ B --> A -------------------------- Conv-Step G |- e : B > If you want to use beta-equality as suggested you need to make sure that both types are well-typed, that is you have to add the assumption G |- B : s in both rules. My apologies. I should use the corrected rules above. Let's discuss if these two rules are equivalent. > That is, unless it's somehow possible for one of the intermediate terms to be ill-typed (i.e.: fail the A : s condition). I have the same concern here. In the original "Conv" rule, the premises only ensure B is well-typed but not the intermediate types which need to be well-typed in "Conv-Step" rules. Considering a reduction sequence A --> C --> B, we can apply "Conv" rule once and check if A and B are well-typed, but need to apply "Conv-Step" twice and check all A, B and C. Unless we know subject reduction holds in the system with "Conv-Step", we just need to check A and B. But I got stuck when tried to prove subject reduction since I cannot work out inversion lemmas using the "Conv-Step" rule. Any ideas on fixing the proof? Thanks again! Regards, Yanpeng On Thu, Aug 24, 2017 at 5:52 PM, Thorsten Altenkirch < Thorsten.Altenkirch at nottingham.ac.uk> wrote: > Conversion should be defined as a judgement only including typed terms > otherwise it is not clear what the system means semantically. > > If you want to use beta-equality as suggested you need to make sure that > both types are well-typed, that is you have to add the assumption G |- B : > s in both rules. Otherwise you get untypable types which make no sense and > do not correspond to typing judgement in the reference system using > judgements. > > Thorsten > > On 23/08/2017, 09:21, "Types-list on behalf of Yang, Yanpeng" < > types-list-bounces at LISTS.SEAS.UPENN.EDU on behalf of yangyp at connect.hku.hk> > wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list ] > > Dear all, > > The conversion rule of the Calculus of Constructions (CC) is usually > defined as follows: > > G |- e : A > G |- A : s > A ==beta B > ------------------- Conv > G |- e : B > > I wonder if this rule is equivalent to the one using *one-step* beta > reduction: > > G |- e : A > G |- A : s > A --> B \/ B --> A > -------------------------- Conv-Step > G |- e : B > > This "Conv-Step" rule is shown in Geuvers' paper [1, Definition 4.1] > but > which never mentions if it is equivalent to the original "Conv" rule. > > So, my question is: has it ever been proved that the two conversion > rules > are equivalent? If so, what is the appropriate article to refer to for > this > proof? > > Thanks a lot! > > Sincerely, > Yanpeng > > [1] Geuvers, Herman. "A short and flexible proof of Strong > Normalization > for the Calculus of Constructions." International Workshop on Types for > Proofs and Programs. Springer, Berlin, Heidelberg, 1994. > URL: http://flint.cs.yale.edu/trifonov/cs629/Geuvers-SN-CC-2up.ps > > > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please send it back to me, and immediately delete it. > > Please do not use, copy or disclose the information contained in this > message or in any attachment. Any views or opinions expressed by the > author of this email do not necessarily reflect the views of the > University of Nottingham. > > This message has been checked for viruses but the contents of an > attachment may still contain software viruses which could damage your > computer system, you are advised to perform your own checks. Email > communications with the University of Nottingham may be monitored as > permitted by UK legislation. > > From aarthur at seas.upenn.edu Thu Sep 28 12:15:23 2017 From: aarthur at seas.upenn.edu (Arthur Azevedo de Amorim) Date: Thu, 28 Sep 2017 16:15:23 +0000 Subject: [TYPES] Inverse limit for categories Message-ID: Is anybody aware of an analog of the inverse limit construction at the level of categories? That is, I want to build an entire category that has recursive structure, and not just a recursive object in a concrete category like CPO. Thanks, Arthur From b.bentzen at hotmail.com Thu Oct 12 03:56:59 2017 From: b.bentzen at hotmail.com (Bruno Bentzen) Date: Thu, 12 Oct 2017 07:56:59 +0000 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle Message-ID: Dear all, It is relatively well-known that the meaning explanations of Martin-L?f dependent type theory (MLTT) justifies many inference rules that may not be included in the formalism (the reflection rule, for instance). However, do the meaning explanations also justify (via the proposition-as-types correspondence) the invalidation of that law of excluded middle for all types? In other words, is the judgment ??(A : U) A + ?A true validated by the meaning explanations? I am strongly inclined to believe that the answer is 'yes'. Please correct me if I am wrong: because MLTT proves that H : ? (P : A -> U) ??(x : A) P(x) + ?P(x) ???(A : U) A + ?A true it is sufficient to demonstrate the validation of the categorical judgment ? (P : A -> U) ??(x : A) P(x) + ?P(x) true For this task we are required to exhibit a pair with a closed predicate P : A -> U such that we have a closed proof of ??(x : A) P(x) + ?P(x). Now let A := nat and P := ? (i, x : nat) T(e,i,x), where 'T' stands for Kleene's predicate. Given the meaning of the negation sign, the matter amounts to the question H : ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x)) ? empty true ? but there can be no such closed term H, otherwise we would have a decision procedure for the halting problem. Could anyone kindly confirm if this is correct? Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ From asal at itu.dk Thu Oct 12 09:10:13 2017 From: asal at itu.dk (Ahmad Salim Al-Sibahi) Date: Thu, 12 Oct 2017 13:10:13 +0000 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle Message-ID: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> Dear Bruno, As far as I understand, MLTT is not anti-classical so it leaves it open whether the law of excluded middle or its converse can be added to the theory without losing consistency. That is, you can add ` ?(A : U) A + ?A true` and get a consistent classical system; so traditionally ???(A : U) A + ?A true? should not be derivable in MLTT. Kind Regards/Med Venlig Hilsen, Ahmad Salim D. 12/10/2017 11.19 skrev "Types-list p? vegne af Bruno Bentzen" : [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear all, It is relatively well-known that the meaning explanations of Martin-L?f dependent type theory (MLTT) justifies many inference rules that may not be included in the formalism (the reflection rule, for instance). However, do the meaning explanations also justify (via the proposition-as-types correspondence) the invalidation of that law of excluded middle for all types? In other words, is the judgment ??(A : U) A + ?A true validated by the meaning explanations? I am strongly inclined to believe that the answer is 'yes'. Please correct me if I am wrong: because MLTT proves that H : ? (P : A -> U) ??(x : A) P(x) + ?P(x) ???(A : U) A + ?A true it is sufficient to demonstrate the validation of the categorical judgment ? (P : A -> U) ??(x : A) P(x) + ?P(x) true For this task we are required to exhibit a pair with a closed predicate P : A -> U such that we have a closed proof of ??(x : A) P(x) + ?P(x). Now let A := nat and P := ? (i, x : nat) T(e,i,x), where 'T' stands for Kleene's predicate. Given the meaning of the negation sign, the matter amounts to the question H : ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x)) ? empty true ? but there can be no such closed term H, otherwise we would have a decision procedure for the halting problem. Could anyone kindly confirm if this is correct? Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ From andrej.bauer at andrej.com Fri Oct 13 02:14:34 2017 From: andrej.bauer at andrej.com (Andrej Bauer) Date: Fri, 13 Oct 2017 08:14:34 +0200 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> Message-ID: Dear Bruno, the problem with your argument is that inside type theory you cannot extract the Godel code of an argument from the argument, and so your outline of a proof won't work. That is, we cannot derive H : ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x)) ? empty because for that we would need to go somewhat like this: 1. Suppose we have such an H. 2. Then there is a (a code of) Turing machine e which computes like H. 3. We diagonalize against this e, and we get a contradiction. You cannot pass from 1 to 2 in type theory. With kind regards, Andrej From andrej.bauer at andrej.com Fri Oct 13 02:27:19 2017 From: andrej.bauer at andrej.com (Andrej Bauer) Date: Fri, 13 Oct 2017 08:27:19 +0200 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> Message-ID: Perhaps it helps to solve the following simpler exercise first: Is there a term G : (nat ? nat) ? nat such that, for any closed term f : nat ? nat, G f is a G?del code of f ? With kind regards, Andrej From b.bentzen at hotmail.com Fri Oct 13 04:23:25 2017 From: b.bentzen at hotmail.com (Bruno Bentzen) Date: Fri, 13 Oct 2017 08:23:25 +0000 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk>, Message-ID: Dear Andrej and Ahmad, Thank you very much for your kind replies, with which I fully agree. At this point, I feel that I should emphasize that I am well aware that Martin-L?f type theory (MLTT) is fully compatible with classical logic formally speaking, which means that the theory has no derivation of the judgments (A) and (B) (A) ??(A : U) A + ?A true (B) H : ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x)) ? empty true However, regardless of not being derivable in MLTT, my question is: are (A) and (B) validated by the meaning explanation? In order to illustrate why I think this question may be plausible in principle, please let me recall you that both judgments (R) and (E) below are inderivable in (intensional) MLTT, yet they are both validated by Martin-L?f's (1982, 1984) meaning explanations. (R) ?(A : U)(x : A)(p : Id(A,x,x)) p = refl_x true (E) ?(p : Id(nat,0,1)) ? 1 : nat -> nat Consequently, a judgment that is inderivable in MLTT need not be invalid by the meaning explanations. In the context of MLTT, that is, from inside the theory, I could not agree more with Andrej's point here: >That is, we cannot derive > >H : ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x)) ? empty > >because for that we would need to go somewhat like this: > >1. Suppose we have such an H. >2. Then there is a (a code of) Turing machine e which computes like H. >3. We diagonalize against this e, and we get a contradiction. > >You cannot pass from 1 to 2 in type theory. but I would like to understand why, from the perspective of the meaning explanations alone (where terms are open-ended programs in a computation system resulted from an untyped notion of computation), the inference from 1 to 2 fails? Perhaps because programs are open-ended (as it was pointed out to me by Bob Harper), so that we have no means of recursively enumerate them all (because one can always extend the computational system with new programs)? But if this is the case, I fail to see why it is acceptable to rule out Kleene's T as a program (since programs are open-ended). Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ ________________________________ Von: Andrej Bauer Gesendet: Freitag, 13. Oktober 2017 04:14 An: types-list at lists.seas.upenn.edu; Bruno Bentzen Betreff: Re: [TYPES] Meaning explanations and the invalidity of the law of excluded middle Dear Bruno, the problem with your argument is that inside type theory you cannot extract the Godel code of an argument from the argument, and so your outline of a proof won't work. That is, we cannot derive H : ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x)) ? empty because for that we would need to go somewhat like this: 1. Suppose we have such an H. 2. Then there is a (a code of) Turing machine e which computes like H. 3. We diagonalize against this e, and we get a contradiction. You cannot pass from 1 to 2 in type theory. With kind regards, Andrej From p.giarrusso at gmail.com Fri Oct 13 08:37:21 2017 From: p.giarrusso at gmail.com (Paolo Giarrusso) Date: Fri, 13 Oct 2017 14:37:21 +0200 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> Message-ID: On 13 October 2017 at 10:23, Bruno Bentzen wrote: > but I would like to understand why, from the perspective of the meaning explanations alone (where terms are open-ended programs in a computation system resulted from an untyped notion of computation), the inference from 1 to 2 fails? > > Perhaps because programs are open-ended (as it was pointed out to me by Bob Harper), so that we have no means of recursively enumerate them all (because one can always extend the computational system with new programs)? But if this is the case, I fail to see why it is acceptable to rule out Kleene's T as a program (since programs are open-ended). Dear Bruno, I understand the meaning explanation can be seen as basically a realizability interpretation of type theory based on untyped realizers [1]? Then let me provide my 2 cents, based on my (partial) understanding of realizability and PER models. I welcome any corrections. Since we talk about truth in a model and not usual provability, I'll write ? ? t : T, instead of ? ? t : T true. I'm not 100% what you mean by open-ended ? with an open-ended set of terms, where you allow adding "postulates", you can't even validate (E) [1]. But once you fix your set of terms, you can do structural induction on them *in the metatheory*, but even untyped lambda terms cannot inspect the structure of their arguments (as Andrej explained), unlike Turing machines. So, let's write U for your type ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x)). Then, it should be provable metatheoretically that there is no closed value of of type U (as you say). This reasoning cannot be internalized into a lambda term, essentially by Andrej's argument; yet, I expect the metatheoretic argument is sufficient to prove that H: U ? ? (or, in your notation, that H : U ? empty true). Specifically, just like (E) p : Id(nat,0,1) ? 1 : nat -> nat holds because Id(nat,0,1) is empty, and vacuously for all members p of Id(nat,0,1) we have that 1 realizes nat -> nat, I think that judgement (B) p : U ? 1 : empty holds by a similar argument. In either case, if we add postulates to sets of realizers so that Id(nat,0,1) or U is non-empty [1], we get a different model where (E) and (B) fail?however, such postulates could not be reduced, destroying canonicity. Which is good: canonicity enables computation, so a realizer for excluded middle can't actually be computable in all cases. (Formally, IIUC, instead of considering closed values as realizers, we'd allow a few free variables, and make assumptions on what types those variables realize). On a related note, IIUC your judgement holds in NuPRL (by a different proof?), which appears to be also based on the meaning explanation [2]. That's how I interpret http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/quot_1/no-excluded-middle-quot-true2.html (where ? is defined in http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/per!type!1/quotient.html and quotients realizers together). [1] https://ncatlab.org/nlab/show/meaning+explanation [2] http://www.jonmsterling.com/pdfs/meaning-explanations.pdf Cheers, -- Paolo G. Giarrusso - Ph.D. Student, T?bingen University http://ps.informatik.uni-tuebingen.de/team/giarrusso/ From jon at jonmsterling.com Sat Oct 14 09:38:27 2017 From: jon at jonmsterling.com (Jon Sterling) Date: Sat, 14 Oct 2017 06:38:27 -0700 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> Message-ID: <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> Hi Paolo and Bruno, I just want to clarify that Nuprl is based on a very different and much more complex 'meaning explanation' than Martin-L?f's; while Nuprl's semantics validate the negation of the the principle of excluded middle for types, it is compatible with classical reasoning at the proof-irrelevant level (Constable calls this "virtual evidence semantics"). On the other hand, my impression is that the MLTT meaning explanation does not validate either the excluded middle for types, nor its negation. The argument given by Andrej explains why... Relatedly, both MLTT and Nuprl's meaning explanations refute Church's Thesis if formulated internally (not only does it fail to hold, it is false). Best, Jon On Fri, Oct 13, 2017, at 05:37 AM, Paolo Giarrusso wrote: > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > On 13 October 2017 at 10:23, Bruno Bentzen wrote: > > but I would like to understand why, from the perspective of the meaning explanations alone (where terms are open-ended programs in a computation system resulted from an untyped notion of computation), the inference from 1 to 2 fails? > > > > Perhaps because programs are open-ended (as it was pointed out to me by Bob Harper), so that we have no means of recursively enumerate them all (because one can always extend the computational system with new programs)? But if this is the case, I fail to see why it is acceptable to rule out Kleene's T as a program (since programs are open-ended). > > Dear Bruno, > > I understand the meaning explanation can be seen as basically a > realizability interpretation of type theory based on untyped realizers > [1]? Then let me provide my 2 cents, based on my (partial) > understanding of realizability and PER models. I welcome any > corrections. > > Since we talk about truth in a model and not usual provability, I'll > write ? ? t : T, instead of ? ? t : T true. > > I'm not 100% what you mean by open-ended ? with an open-ended set of > terms, where you allow adding "postulates", you can't even validate > (E) [1]. > But once you fix your set of terms, you can do structural induction on > them *in the metatheory*, but even untyped lambda terms cannot inspect > the structure of their arguments (as Andrej explained), unlike Turing > machines. > > So, let's write U for your type ?(e : nat) (? (i, x : nat) T(e,i,x)) + > ?(? (i, x : nat) T(e,i,x)). Then, it should be provable > metatheoretically that there is no closed value of of type U (as you > say). This reasoning cannot be internalized into a lambda term, > essentially by Andrej's argument; yet, I expect the metatheoretic > argument is sufficient to prove that H: U ? ? (or, in your notation, > that H : U ? empty true). > > Specifically, just like > > (E) p : Id(nat,0,1) ? 1 : nat -> nat > > holds because Id(nat,0,1) is empty, and vacuously for all members p of > Id(nat,0,1) we have that 1 realizes nat -> nat, I think that judgement > > (B) p : U ? 1 : empty > > holds by a similar argument. > > In either case, if we add postulates to sets of realizers so that > Id(nat,0,1) or U is non-empty [1], we get a different model where (E) > and (B) fail?however, such postulates could not be reduced, destroying > canonicity. Which is good: canonicity enables computation, so a > realizer for excluded middle can't actually be computable in all > cases. (Formally, IIUC, instead of considering closed values as > realizers, we'd allow a few free variables, and make assumptions on > what types those variables realize). > > On a related note, IIUC your judgement holds in NuPRL (by a different > proof?), which appears to be also based on the meaning explanation > [2]. That's how I interpret > http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/quot_1/no-excluded-middle-quot-true2.html > (where ? is defined in > http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/per!type!1/quotient.html > and quotients realizers together). > > [1] https://ncatlab.org/nlab/show/meaning+explanation > [2] http://www.jonmsterling.com/pdfs/meaning-explanations.pdf > > Cheers, > -- > Paolo G. Giarrusso - Ph.D. Student, T?bingen University > http://ps.informatik.uni-tuebingen.de/team/giarrusso/ From p.giarrusso at gmail.com Mon Oct 16 09:28:34 2017 From: p.giarrusso at gmail.com (Paolo Giarrusso) Date: Mon, 16 Oct 2017 15:28:34 +0200 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> Message-ID: On 14 October 2017 at 15:38, Jon Sterling wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi Paolo and Bruno, > > I just want to clarify that Nuprl is based on a very different and much > more complex 'meaning explanation' than Martin-L?f's; while Nuprl's > semantics validate the negation of the the principle of excluded middle > for types, it is compatible with classical reasoning at the > proof-irrelevant level (Constable calls this "virtual evidence > semantics"). > > On the other hand, my impression is that the MLTT meaning explanation > does not validate either the excluded middle for types, nor its > negation. The argument given by Andrej explains why... > > Relatedly, both MLTT and Nuprl's meaning explanations refute Church's > Thesis if formulated internally (not only does it fail to hold, it is > false). Thanks to Jon for his clarification (also elsewhere)! For those interested in more details, the same argument was laid out by Thierry Coquand. This thread (linked from nLab) clarifies why it does not apply to meaning explanations: http://uf-ias-2012.wikispaces.com/file/view/IAS+-+MEANING+EXPLANATION+DISCUSSION/390300226/IAS%20-%20MEANING%20EXPLANATION%20DISCUSSION Thierry Coquand writes A = forall n. exists m T(n,n,m) \/ not (exists m T(n,n,m)) T Kleene predicate (*almost* the same as the above U = ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x))), and gives a similar argument. IIUC, the discussion explains in more detail why the argument works in a realizability PER-model but not in the meaning explanations. These quotes appear to me most relevant (though I recommend the rest, especially on 'pre-mathematics' and the underlying philosophical considerations): > [Bob Constable:] The type A that Thierry is reasoning about is only known to be unrealizable if we accept Church's Thesis (CT). We don't accept that in CTT. If the reasoning is in the meta theory, using Church's Rule, then we might say that A is unrealizable based on an external analysis, but this is not expressible inside the theory and \x.0 is not a realizer inside for ~A. > [Bob Harper:] it is a delicate point about the nature of the meaning semantics and the concept of "pre-mathematics" that peter has been defending. the formula that thierry gave is indeed independent of HA viewed as a formal system, and if the meaning of the negation were given by provability in that formal system, then we would be in a situation where every unrealizable statement would be positively false. but that is not the case. the fact that thierry's A is unrealizable requires church's thesis, which we do not accept in the pre-mathematics (nor should we) in which the semantics is given. > [Peter Dybjer:] I agree with the conclusion of this discussion that if you consider the "meaning explanations" as being about a fixed language of computable realizers, then we can justify anti-classical principles. Relating this to my talk, I see this as one of the "global" conditions that we do not want to assume in the "meaning explanations". The meaning of a judgement should only depend on its constituent terms, not on properties of the language in which it is embedded. On Church's thesis in NuPRL, I also found https://existentialtype.wordpress.com/2012/08/09/churchs-law/ helpful. Cheers, -- Paolo G. Giarrusso - Ph.D. Student, T?bingen University http://ps.informatik.uni-tuebingen.de/team/giarrusso/ From b.bentzen at hotmail.com Mon Oct 16 11:22:28 2017 From: b.bentzen at hotmail.com (Bruno Bentzen) Date: Mon, 16 Oct 2017 15:22:28 +0000 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com>, Message-ID: Dear Paolo (and all), >For those interested in more details, the same >argument was laid out by Thierry Coquand. >This thread (linked from nLab) clarifies why it >does not apply to meaning explanations Thank you very much for this nice observation! For the record, it took me some time but I am now fully convinced that the argument I outlined here in this thread must necessarily fail for reasons that can be seen both from the perspective of syntax (as Andrej has pointed out) or semantics (as explained by Jon). (In both cases, it seems to me that the situation looks a bit like Skolem's "paradox" in set theory: internally we can show that there is no bijection from IN to IR, but externally the theory has a countable model.) First, we can see that the do not have access to the syntax of the theory internally, so we do not have a criterion to construct the G?del numbering function internally, even though we know externally that this function exists (besides such a function should also respect judgmental equality and assign the same G?del number to judgmentally equal terms). Second, the reason why the meaning explanations cannot invalidate the law of the excluded middle is because they do not circumscribe the collection of all possible programs (in other words, the collection of terms is left open-ended) so they cannot rule out that oracles could be also programs. Simply put, Church's thesis is not accepted internally, even though it is true externally. Last but not least, I want to thank all of you who took the time to discuss and help me to understand these fascinating issues! Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ ________________________________ Von: Paolo Giarrusso Gesendet: Montag, 16. Oktober 2017 11:28 An: Types list Cc: Bruno Bentzen Betreff: Re: [TYPES] Meaning explanations and the invalidity of the law of excluded middle On 14 October 2017 at 15:38, Jon Sterling wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi Paolo and Bruno, > > I just want to clarify that Nuprl is based on a very different and much > more complex 'meaning explanation' than Martin-L?f's; while Nuprl's > semantics validate the negation of the the principle of excluded middle > for types, it is compatible with classical reasoning at the > proof-irrelevant level (Constable calls this "virtual evidence > semantics"). > > On the other hand, my impression is that the MLTT meaning explanation > does not validate either the excluded middle for types, nor its > negation. The argument given by Andrej explains why... > > Relatedly, both MLTT and Nuprl's meaning explanations refute Church's > Thesis if formulated internally (not only does it fail to hold, it is > false). Thanks to Jon for his clarification (also elsewhere)! For those interested in more details, the same argument was laid out by Thierry Coquand. This thread (linked from nLab) clarifies why it does not apply to meaning explanations: http://uf-ias-2012.wikispaces.com/file/view/IAS+-+MEANING+EXPLANATION+DISCUSSION/390300226/IAS%20-%20MEANING%20EXPLANATION%20DISCUSSION Thierry Coquand writes A = forall n. exists m T(n,n,m) \/ not (exists m T(n,n,m)) T Kleene predicate (*almost* the same as the above U = ?(e : nat) (? (i, x : nat) T(e,i,x)) + ?(? (i, x : nat) T(e,i,x))), and gives a similar argument. IIUC, the discussion explains in more detail why the argument works in a realizability PER-model but not in the meaning explanations. These quotes appear to me most relevant (though I recommend the rest, especially on 'pre-mathematics' and the underlying philosophical considerations): > [Bob Constable:] The type A that Thierry is reasoning about is only known to be unrealizable if we accept Church's Thesis (CT). We don't accept that in CTT. If the reasoning is in the meta theory, using Church's Rule, then we might say that A is unrealizable based on an external analysis, but this is not expressible inside the theory and \x.0 is not a realizer inside for ~A. > [Bob Harper:] it is a delicate point about the nature of the meaning semantics and the concept of "pre-mathematics" that peter has been defending. the formula that thierry gave is indeed independent of HA viewed as a formal system, and if the meaning of the negation were given by provability in that formal system, then we would be in a situation where every unrealizable statement would be positively false. but that is not the case. the fact that thierry's A is unrealizable requires church's thesis, which we do not accept in the pre-mathematics (nor should we) in which the semantics is given. > [Peter Dybjer:] I agree with the conclusion of this discussion that if you consider the "meaning explanations" as being about a fixed language of computable realizers, then we can justify anti-classical principles. Relating this to my talk, I see this as one of the "global" conditions that we do not want to assume in the "meaning explanations". The meaning of a judgement should only depend on its constituent terms, not on properties of the language in which it is embedded. On Church's thesis in NuPRL, I also found https://existentialtype.wordpress.com/2012/08/09/churchs-law/ helpful. Cheers, -- Paolo G. Giarrusso - Ph.D. Student, T?bingen University http://ps.informatik.uni-tuebingen.de/team/giarrusso/ From andrej.bauer at andrej.com Tue Oct 17 04:00:52 2017 From: andrej.bauer at andrej.com (Andrej Bauer) Date: Tue, 17 Oct 2017 10:00:52 +0200 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> Message-ID: > Relatedly, both MLTT and Nuprl's meaning explanations refute Church's > Thesis if formulated internally (not only does it fail to hold, it is > false). Really? How does (pure!) MLTT refute Church's Thesis? Oh, you're interpreting it like this: ? (f : N ? N) ? (e : N) ? (n m : N) (Id(f n, m) ? ? (k : N) T(e, n, k) ? Id (U k, m) ? This says: "For every function f there is a machine e, such that f(n) = m is equivalent to there existing a run k of e on input n which results in output m." Cruicially, because we're using pies and sigmas, e depends on f in an extensional way, i.e., we can extract a map godel : (N ? N) ? N which calculates such an e, given f. But that's not a contradiction yet. How do you get a contradiction? With kind regards, Andrej From jon at jonmsterling.com Tue Oct 17 08:26:23 2017 From: jon at jonmsterling.com (Jon Sterling) Date: Tue, 17 Oct 2017 05:26:23 -0700 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: <20171017100526.GA17688@mathematik.tu-darmstadt.de> References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> <20171017100526.GA17688@mathematik.tu-darmstadt.de> Message-ID: <1508243183.1211717.1141552288.4CD824BA@webmail.messagingengine.com> Dear Andrej and Thomas, I was referring to extensional MLTT (MLTT 1979), not intensional MLTT (for which the question is still open, I believe); I believe the result is from Troelstra, but I can try and dig up the details. Best, Jon On Tue, Oct 17, 2017, at 03:05 AM, Thomas Streicher wrote: > Of course, for various reasons CT is not derivable in MLTT. It's > rather the opposite which is an open question, namely whether > intensional MLTT is consistent with CT formulated via a \Sigma-type. > > This question has been brought up quite some time ago by Milly Maietti > and is still open. > > Thomas From streicher at mathematik.tu-darmstadt.de Tue Oct 17 06:05:27 2017 From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher) Date: Tue, 17 Oct 2017 12:05:27 +0200 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> Message-ID: <20171017100526.GA17688@mathematik.tu-darmstadt.de> Of course, for various reasons CT is not derivable in MLTT. It's rather the opposite which is an open question, namely whether intensional MLTT is consistent with CT formulated via a \Sigma-type. This question has been brought up quite some time ago by Milly Maietti and is still open. Thomas From streicher at mathematik.tu-darmstadt.de Tue Oct 17 09:11:03 2017 From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher) Date: Tue, 17 Oct 2017 15:11:03 +0200 Subject: [TYPES] Meaning explanations and the invalidity of the law of excluded middle In-Reply-To: <1508243183.1211717.1141552288.4CD824BA@webmail.messagingengine.com> References: <571D7764-836C-488A-B118-4D7F6F0A371C@itu.dk> <1507988307.350040.1138661480.42D828C1@webmail.messagingengine.com> <20171017100526.GA17688@mathematik.tu-darmstadt.de> <1508243183.1211717.1141552288.4CD824BA@webmail.messagingengine.com> Message-ID: <20171017131102.GB17688@mathematik.tu-darmstadt.de> On Tue, Oct 17, 2017 at 05:26:23AM -0700, Jon Sterling wrote: > Dear Andrej and Thomas, > > I was referring to extensional MLTT (MLTT 1979), not intensional MLTT > (for which the question is still open, I believe); I believe the result > is from Troelstra, but I can try and dig up the details. Sure, one knows that relative to HA_omega the combination of extensionality, choice and continuity is inconistent simply because you can't tell a program from an initial segment of the function it computes. Thomas From aaronngray.lists at gmail.com Wed Oct 18 15:22:44 2017 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Wed, 18 Oct 2017 20:22:44 +0100 Subject: [TYPES] Book on Category Theory Message-ID: I am looking for a book on Category Theory that is ideally either aimed at Type Theory or has the relevant topics to support the area. I have bought three books on the topic so far, one 'Categories for Typesw' by Crole did not even cover covariance and contravariance.I would also like coverage of monoid and monads, and morphisms like anamorphisms and catamorphisms. I am also interested in papers applying category theory to areas of type theory. Suggestions of either online or printed material would be appreciated. Many tahnks in advance, -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From gabriel.scherer at gmail.com Thu Oct 19 04:33:33 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Thu, 19 Oct 2017 10:33:33 +0200 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: You could have a look at Barr and Wells' "Category Theory for Computing Science", 1998, which is available online: http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf I think it strikes a reasonable balance for computer science students: the mathematical examples that it uses are not too advanced, and it also uses examples from programming language to draw intuition. Note that it was written before some of the recent popularization of category theory for programming languages, so some of the vocabulary is different. Monads are called Triples, and their application to modeling effects is not discussed. On Wed, Oct 18, 2017 at 9:22 PM, Aaron Gray wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I am looking for a book on Category Theory that is ideally either aimed at > Type Theory or has the relevant topics to support the area. > > I have bought three books on the topic so far, one 'Categories for Typesw' > by Crole did not even cover covariance and contravariance.I would also like > coverage of monoid and monads, and morphisms like anamorphisms and > catamorphisms. > > I am also interested in papers applying category theory to areas of type > theory. > > Suggestions of either online or printed material would be appreciated. > > Many tahnks in advance, > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language Researcher, > Information Theorist, and amateur computer scientist. > From gc at pps.univ-paris-diderot.fr Thu Oct 19 04:47:38 2017 From: gc at pps.univ-paris-diderot.fr (Giuseppe Castagna) Date: Thu, 19 Oct 2017 10:47:38 +0200 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: My references are a little bit outdated but you can check: Basic category theory for computer scientists by Benjamin C. Pierce Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist by Andrea Asperti and Giuseppe Longo Cheers Beppe On 18/10/17 21:22, Aaron Gray wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I am looking for a book on Category Theory that is ideally either aimed at > Type Theory or has the relevant topics to support the area. > > I have bought three books on the topic so far, one 'Categories for Typesw' > by Crole did not even cover covariance and contravariance.I would also like > coverage of monoid and monads, and morphisms like anamorphisms and > catamorphisms. > > I am also interested in papers applying category theory to areas of type > theory. > > Suggestions of either online or printed material would be appreciated. > > Many tahnks in advance, From moez at cs.rice.edu Thu Oct 19 05:50:38 2017 From: moez at cs.rice.edu (Moez A. AbdelGawad) Date: Thu, 19 Oct 2017 11:50:38 +0200 Subject: [TYPES] Book on Category Theory Message-ID: In addition to Pierce's book, which was earlier mentioned, I strongly recommend Spivak's Category Theory for The Sciences and Lawvere & Schanuel's Conceptual Mathematics. Even though neither book is specifically for computer scientists, but both books are more modern, very accessible, and frequently discuss CS applications. -Moez -------- Original message -------- From: Aaron Gray Date: 18/10/2017 21:22 (GMT+02:00) To: The TYPES forum Subject: [TYPES] Book on Category Theory [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] I am looking for a book on Category Theory that is ideally either aimed at Type Theory or has the relevant topics to support the area. I have bought three books on the topic so far, one 'Categories for Typesw' by Crole did not even cover covariance and contravariance.I would also like coverage of monoid and monads, and morphisms like anamorphisms and catamorphisms. I am also interested in papers applying category theory to areas of type theory. Suggestions of either online or printed material would be appreciated. Many tahnks in advance, -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From franth2 at gmail.com Thu Oct 19 08:48:08 2017 From: franth2 at gmail.com (=?UTF-8?B?RnJhbsOnb2lzIFRoaXLDqQ==?=) Date: Thu, 19 Oct 2017 14:48:08 +0200 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: Bartosz Milewski also published sone articles on his blog about "Category Theory for Programmers" : https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ . The examples come from Haskell (and sometimes C++). Since a few weeks, the book also exists in a PDF version: https://github.com/hmemcpy/milewski-ctfp-pdf Since the book is intended for programmers, it is less formal than the books mentioned earlier. But Haskell examples help to get some intuition about some definitions. 2017-10-19 11:50 GMT+02:00 Moez A. AbdelGawad : > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > In addition to Pierce's book, which was earlier mentioned, I strongly > recommend Spivak's Category Theory for The Sciences and Lawvere & > Schanuel's Conceptual Mathematics. Even though neither book is specifically > for computer scientists, but both books are more modern, very accessible, > and frequently discuss CS applications. > > -Moez > > -------- Original message -------- > From: Aaron Gray > Date: 18/10/2017 21:22 (GMT+02:00) > To: The TYPES forum > Subject: [TYPES] Book on Category Theory > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I am looking for a book on Category Theory that is ideally either aimed at > Type Theory or has the relevant topics to support the area. > > I have bought three books on the topic so far, one 'Categories for Typesw' > by Crole did not even cover covariance and contravariance.I would also like > coverage of monoid and monads, and morphisms like anamorphisms and > catamorphisms. > > I am also interested in papers applying category theory to areas of type > theory. > > Suggestions of either online or printed material would be appreciated. > > Many tahnks in advance, > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language Researcher, > Information Theorist, and amateur computer scientist. > From alan.schmitt at polytechnique.org Thu Oct 19 09:44:45 2017 From: alan.schmitt at polytechnique.org (Alan Schmitt) Date: Thu, 19 Oct 2017 15:44:45 +0200 Subject: [TYPES] Book on Category Theory In-Reply-To: (Aaron Gray's message of "Wed, 18 Oct 2017 20:22:44 +0100") References: Message-ID: On 2017-10-18 20:22, Aaron Gray writes: > I am looking for a book on Category Theory that is ideally either aimed at > Type Theory or has the relevant topics to support the area. > > I have bought three books on the topic so far, one 'Categories for Typesw' > by Crole did not even cover covariance and contravariance.I would also like > coverage of monoid and monads, and morphisms like anamorphisms and > catamorphisms. I strongly recommend ?Category Theory for Programmers? by Bartosz Milewski. It's available online as a series of article, or as a pdf. New content is regularly added. https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ Best, Alan -- OpenPGP Key ID : 040D0A3B4ED2E5C7 Monthly Athmospheric CO?, Mauna Loa Obs. 2017-09: 403.38, 2016-09: 401.03 From u.s.reddy at cs.bham.ac.uk Thu Oct 19 11:40:52 2017 From: u.s.reddy at cs.bham.ac.uk (Uday S Reddy) Date: Thu, 19 Oct 2017 16:40:52 +0100 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: <23016.51076.597000.873109@gargle.gargle.HOWL> In addition to all the excellent books that have been recommended already, I can recommend my "Lecture notes on Categories and Functors" written for the Midlands Graduate School in the UK. It is written specifically with the view point that category theory is a "type theory". It is available via my home page. Unfortunately, the chapter on Monads is unfinished. Cheers, Uday -- Prof. Uday Reddy Tel: +44 121 414 2740 Professor of Computer Science Fax: +44 121 414 4281 School of Computer Science Email: U.S.Reddy at cs.bham.ac.uk University of Birmingham Edgbaston Birmingham B15 2TT Web: http://www.cs.bham.ac.uk/~udr From leo at halfaya.org Thu Oct 19 11:59:47 2017 From: leo at halfaya.org (John Leo) Date: Thu, 19 Oct 2017 08:59:47 -0700 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: I agree Pierce's book is great, and my favorite overall reference Awodey also has some material on applications to type theory. For specific connections, the best sources are probably lecture notes for various summer school courses. My three favorites are those in the "Category Theory and Functional Programming" section of this page: https://github.com/halfaya/BayHac/blob/master/references.md John On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > In addition to Pierce's book, which was earlier mentioned, I strongly > recommend Spivak's Category Theory for The Sciences and Lawvere & > Schanuel's Conceptual Mathematics. Even though neither book is specifically > for computer scientists, but both books are more modern, very accessible, > and frequently discuss CS applications. > > -Moez > > -------- Original message -------- > From: Aaron Gray > Date: 18/10/2017 21:22 (GMT+02:00) > To: The TYPES forum > Subject: [TYPES] Book on Category Theory > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I am looking for a book on Category Theory that is ideally either aimed at > Type Theory or has the relevant topics to support the area. > > I have bought three books on the topic so far, one 'Categories for Typesw' > by Crole did not even cover covariance and contravariance.I would also like > coverage of monoid and monads, and morphisms like anamorphisms and > catamorphisms. > > I am also interested in papers applying category theory to areas of type > theory. > > Suggestions of either online or printed material would be appreciated. > > Many tahnks in advance, > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language Researcher, > Information Theorist, and amateur computer scientist. > From dezani at di.unito.it Mon Oct 23 05:21:55 2017 From: dezani at di.unito.it (Mariangiola Dezani) Date: Mon, 23 Oct 2017 11:21:55 +0200 Subject: [TYPES] =?utf-8?q?Passing_of_Corrado_B=C3=B6hm?= Message-ID: <9C280C71-41E9-4458-A81B-C587832C87A9@di.unito.it> Unfortunately, I have to inform you that one of the most outstanding computer scientist, Corrado B?hm, died. Mariangiola Dezani @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Mariangiola Dezani-Ciancaglini Dipartimento di Informatica Universita' di Torino c.Svizzera 185, 10149 Torino (Italy) e-mail : dezani at di.unito.it phone: 39-011-6706850 fax : 39-011-751603 mobile: 39-320-4359903 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 ********************************************************************** http://processalgebra.blogspot.it/2016/12/mariangiola-dezani-ciancaglini-70-but.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 aaronngray.lists at gmail.com Mon Oct 23 10:56:38 2017 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Mon, 23 Oct 2017 15:56:38 +0100 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: Thanks everyone, but as far as I can tell none of these books give me any real stuff on covariance, contravariance, anamophisms and catamophisms. On 19 October 2017 at 16:59, John Leo wrote: > I agree Pierce's book is great, and my favorite overall reference Awodey > also has some material on applications to type theory. > > For specific connections, the best sources are probably lecture notes for > various summer school courses. My three favorites are those in the > "Category Theory and Functional Programming" section of this page: > https://github.com/halfaya/BayHac/blob/master/references.md > > John > > > > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad > wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> ilman/listinfo/types-list ] >> >> In addition to Pierce's book, which was earlier mentioned, I strongly >> recommend Spivak's Category Theory for The Sciences and Lawvere & >> Schanuel's Conceptual Mathematics. Even though neither book is specifically >> for computer scientists, but both books are more modern, very accessible, >> and frequently discuss CS applications. >> >> -Moez >> >> -------- Original message -------- >> From: Aaron Gray >> Date: 18/10/2017 21:22 (GMT+02:00) >> To: The TYPES forum >> Subject: [TYPES] Book on Category Theory >> >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> ilman/listinfo/types-list ] >> >> I am looking for a book on Category Theory that is ideally either aimed at >> Type Theory or has the relevant topics to support the area. >> >> I have bought three books on the topic so far, one 'Categories for Typesw' >> by Crole did not even cover covariance and contravariance.I would also >> like >> coverage of monoid and monads, and morphisms like anamorphisms and >> catamorphisms. >> >> I am also interested in papers applying category theory to areas of type >> theory. >> >> Suggestions of either online or printed material would be appreciated. >> >> Many tahnks in advance, >> -- >> Aaron Gray >> >> Independent Open Source Software Engineer, Computer Language Researcher, >> Information Theorist, and amateur computer scientist. >> > > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From burak.emir at gmail.com Mon Oct 23 17:58:41 2017 From: burak.emir at gmail.com (Burak Emir) Date: Mon, 23 Oct 2017 23:58:41 +0200 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: Hey there. I also prefer Steve Awodey's "Category Theory" to many of the other references. Contravariant functors happen to be mentioned there as well (p. 107 in 2nd edition - just a functor from C^op -> D : ) ), and it has an example how slice categories relate to indexed families, if dependent types is what you are pursuing. I believe the catamorphism jargon for the arrow from an initial algebra was introduced in Meijer, Fokkinga, Paterson's "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire". Certainly, knowing the categorical treatment of algebras (described succinctly in Pierce's book) will help with the understanding of that paper - and many others. Popular as that jargon seems to be, I believe it is unlikely to come across those terms in category theory books (but I might be wrong). Crole's "Categories for Types" looks like a valuable reference, the way it draws an arc from algebraic type theory over simply typed lambda calculus to system F and F-omega. It does not seem to make as good an introduction though. When looking for another, inspiring introduction that connects category theory and type theory, Lambek and Scott's "Introduction to Higher-Order Categorical Logic" is still an outstanding book, though note the "higher order" refers to lambdas in the same way simply typed lambda calculus was called higher order logic by Church. If you want to take a break from the categories : ) and consider approaching the topic via logic, another reference treating type theory as in "higher order logic" is Andrews "To truth through proof". It focuses on classical logic. To close the circle, for categorical models of dependent types, there are also plenty of references on https://ncatlab.org/nlab/show/categorical+model+of+dependent+types sincerely hope this helps! Burak On Oct 23, 2017 9:48 PM, "Aaron Gray" wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Thanks everyone, but as far as I can tell none of these books give me any real stuff on covariance, contravariance, anamophisms and catamophisms. On 19 October 2017 at 16:59, John Leo wrote: > I agree Pierce's book is great, and my favorite overall reference Awodey > also has some material on applications to type theory. > > For specific connections, the best sources are probably lecture notes for > various summer school courses. My three favorites are those in the > "Category Theory and Functional Programming" section of this page: > https://github.com/halfaya/BayHac/blob/master/references.md > > John > > > > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad > wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> ilman/listinfo/types-list ] >> >> In addition to Pierce's book, which was earlier mentioned, I strongly >> recommend Spivak's Category Theory for The Sciences and Lawvere & >> Schanuel's Conceptual Mathematics. Even though neither book is specifically >> for computer scientists, but both books are more modern, very accessible, >> and frequently discuss CS applications. >> >> -Moez >> >> -------- Original message -------- >> From: Aaron Gray >> Date: 18/10/2017 21:22 (GMT+02:00) >> To: The TYPES forum >> Subject: [TYPES] Book on Category Theory >> >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> ilman/listinfo/types-list ] >> >> I am looking for a book on Category Theory that is ideally either aimed at >> Type Theory or has the relevant topics to support the area. >> >> I have bought three books on the topic so far, one 'Categories for Typesw' >> by Crole did not even cover covariance and contravariance.I would also >> like >> coverage of monoid and monads, and morphisms like anamorphisms and >> catamorphisms. >> >> I am also interested in papers applying category theory to areas of type >> theory. >> >> Suggestions of either online or printed material would be appreciated. >> >> Many tahnks in advance, >> -- >> Aaron Gray >> >> Independent Open Source Software Engineer, Computer Language Researcher, >> Information Theorist, and amateur computer scientist. >> > > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From dan.doel at gmail.com Mon Oct 23 20:19:51 2017 From: dan.doel at gmail.com (Dan Doel) Date: Mon, 23 Oct 2017 20:19:51 -0400 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: I'm not sure which books go into much detail about covariance and contravariance. I think typically it might be mentioned in connection with functors and opposite categories, and then it's probably assumed it's rather 'obvious' from there. You should know, though, that "anamorphism" and "catamorphism," aren't terms that originate from category theory, though. They were coined (as far as I know) in the paper, "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire." That paper applies some category theory to programming, but the terminology like, "catamorphism," is not part of what's borrowed. And I wouldn't be surprised if most mathematicians had never heard those terms. The most directly related book to that stuff that I've read is Pierce's book, which works up to initial algebras of functors and Lambek's lemma. But I don't think you'll find "catamorphism" there, either, even though it's written by and for the sort of person who might actually encounter the Banana paper. -- Dan On Mon, Oct 23, 2017 at 10:56 AM, Aaron Gray wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Thanks everyone, but as far as I can tell none of these books give me any > real stuff on covariance, contravariance, anamophisms and catamophisms. > > On 19 October 2017 at 16:59, John Leo wrote: > > > I agree Pierce's book is great, and my favorite overall reference Awodey > > also has some material on applications to type theory. > > > > For specific connections, the best sources are probably lecture notes for > > various summer school courses. My three favorites are those in the > > "Category Theory and Functional Programming" section of this page: > > https://github.com/halfaya/BayHac/blob/master/references.md > > > > John > > > > > > > > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad > > wrote: > > > >> [ The Types Forum, http://lists.seas.upenn.edu/ma > >> ilman/listinfo/types-list ] > >> > >> In addition to Pierce's book, which was earlier mentioned, I strongly > >> recommend Spivak's Category Theory for The Sciences and Lawvere & > >> Schanuel's Conceptual Mathematics. Even though neither book is > specifically > >> for computer scientists, but both books are more modern, very > accessible, > >> and frequently discuss CS applications. > >> > >> -Moez > >> > >> -------- Original message -------- > >> From: Aaron Gray > >> Date: 18/10/2017 21:22 (GMT+02:00) > >> To: The TYPES forum > >> Subject: [TYPES] Book on Category Theory > >> > >> [ The Types Forum, http://lists.seas.upenn.edu/ma > >> ilman/listinfo/types-list ] > >> > >> I am looking for a book on Category Theory that is ideally either aimed > at > >> Type Theory or has the relevant topics to support the area. > >> > >> I have bought three books on the topic so far, one 'Categories for > Typesw' > >> by Crole did not even cover covariance and contravariance.I would also > >> like > >> coverage of monoid and monads, and morphisms like anamorphisms and > >> catamorphisms. > >> > >> I am also interested in papers applying category theory to areas of type > >> theory. > >> > >> Suggestions of either online or printed material would be appreciated. > >> > >> Many tahnks in advance, > >> -- > >> Aaron Gray > >> > >> Independent Open Source Software Engineer, Computer Language Researcher, > >> Information Theorist, and amateur computer scientist. > >> > > > > > > > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language Researcher, > Information Theorist, and amateur computer scientist. > From sean.leather at gmail.com Tue Oct 24 02:25:35 2017 From: sean.leather at gmail.com (Sean Leather) Date: Tue, 24 Oct 2017 08:25:35 +0200 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: Hi Aaron, On Mon, Oct 23, 2017 at 4:56 PM, Aaron Gray wrote: > > Thanks everyone, but as far as I can tell none of these books give me any > real stuff on covariance, contravariance, anamophisms and catamophisms. Perhaps ?Category Theory for Program Construction by Calculation? (1995) by Lambert Meertens? https://www.kestrel.edu/home/people/meertens/diverse/ct4pc.pdf >From the Introduction: Category theory is the theory of structure-preserving transformations. This theory provides us with a language for describing complex problems in an elegant way, and tools to give elegant, and above all simple, proofs. The language of category theory allows us to consider the essence of some problem, without the burden of?often numerous and complicated?non-essential aspects. The constructive and universal character of category theory is an aid in finding these proofs. In these lecture notes we emphasise a calculational proof style, to which category theory lends itself well. Examples are drawn from functional programming?and to a lesser extent from lattice theory?and in fact the applicability to calculational program construction has influenced the choice of topics covered. Regards, Sean From gabriel.scherer at gmail.com Tue Oct 24 03:22:39 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Tue, 24 Oct 2017 09:22:39 +0200 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: Hi Aaron, I think you may misunderstand what "category theory for type theory" is about and its focus area. It is perfectly natural for an outsider to be a bit confused about the topic you want to learn about (that's the point of learning), but my impression is that you have some work to do find out what you actually want before you can usefully tap types-list as a direct citation source. Maybe some people around here can help you do this unraveling work (Sean Leather's last reference seems to go in the same direction), but otherwise there are other places where people may be more knowledgeable about orienting people living in the gap between "category theory keywords I hear when I hang around Haskellers" and "category theory books", for example https://www.reddit.com/r/haskell/ . (Reverse engineering what you say, it also sounds like Bartosz Milewski's book mentioned by Fran?ois Thir? above may be one of the closer to what you are looking for.) On Mon, Oct 23, 2017 at 4:56 PM, Aaron Gray wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Thanks everyone, but as far as I can tell none of these books give me any > real stuff on covariance, contravariance, anamophisms and catamophisms. > > On 19 October 2017 at 16:59, John Leo wrote: > > > I agree Pierce's book is great, and my favorite overall reference Awodey > > also has some material on applications to type theory. > > > > For specific connections, the best sources are probably lecture notes for > > various summer school courses. My three favorites are those in the > > "Category Theory and Functional Programming" section of this page: > > https://github.com/halfaya/BayHac/blob/master/references.md > > > > John > > > > > > > > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad > > wrote: > > > >> [ The Types Forum, http://lists.seas.upenn.edu/ma > >> ilman/listinfo/types-list ] > >> > >> In addition to Pierce's book, which was earlier mentioned, I strongly > >> recommend Spivak's Category Theory for The Sciences and Lawvere & > >> Schanuel's Conceptual Mathematics. Even though neither book is > specifically > >> for computer scientists, but both books are more modern, very > accessible, > >> and frequently discuss CS applications. > >> > >> -Moez > >> > >> -------- Original message -------- > >> From: Aaron Gray > >> Date: 18/10/2017 21:22 (GMT+02:00) > >> To: The TYPES forum > >> Subject: [TYPES] Book on Category Theory > >> > >> [ The Types Forum, http://lists.seas.upenn.edu/ma > >> ilman/listinfo/types-list ] > >> > >> I am looking for a book on Category Theory that is ideally either aimed > at > >> Type Theory or has the relevant topics to support the area. > >> > >> I have bought three books on the topic so far, one 'Categories for > Typesw' > >> by Crole did not even cover covariance and contravariance.I would also > >> like > >> coverage of monoid and monads, and morphisms like anamorphisms and > >> catamorphisms. > >> > >> I am also interested in papers applying category theory to areas of type > >> theory. > >> > >> Suggestions of either online or printed material would be appreciated. > >> > >> Many tahnks in advance, > >> -- > >> Aaron Gray > >> > >> Independent Open Source Software Engineer, Computer Language Researcher, > >> Information Theorist, and amateur computer scientist. > >> > > > > > > > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language Researcher, > Information Theorist, and amateur computer scientist. > From buday.gergely at uni-eszterhazy.hu Tue Oct 24 07:26:38 2017 From: buday.gergely at uni-eszterhazy.hu (Gergely Buday) Date: Tue, 24 Oct 2017 13:26:38 +0200 Subject: [TYPES] Book on Category Theory Message-ID: <002001d34cba$fa37b820$eea72860$@uni-eszterhazy.hu> Aaron, https://wiki.haskell.org/Catamorphisms writes: The name catamorphism appears to have been chosen by Lambert Meertens [1]. The category theoretic machinery behind these was resolved by Grant Malcolm [2][3], and they were popularized by Meijer, Fokkinga and Paterson[4][5]. The name comes from the Greek '????-' meaning "downward or according to". A useful mnemonic is to think of a catastrophe destroying something. 1. L. Meertens. First Steps towards the theory of Rose Trees. Draft Report, CWI, Amsterdam, 1987. 2. G. Malcolm. PhD. Thesis. University of Gronigen, 1990. 3. G. Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255--279, 1990. 4. E. Meijer. Calculating Compilers, Ph.D Thesis, Utrecht State University, 1992. 5. E. Meijer, M. Fokkinga, R. Paterson, Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, 5th ACM Conference on Functional Programming Languages and Computer Architecture. 6. T. Uustalu, V. Vene. Coding Recursion a la Mendler. Proceedings 2nd Workshop on Generic Programming, WGP'2000, Ponte de Lima, Portugal, 6 July 2000 7. T. Uustalu, V. Vene, A. Pardo. Recursion schemes from Comonads. Nordic Journal of Computing. Volume 8 , Issue 3 (Fall 2001). 366--390, 2001 ISSN:1236-6064 8. E. Kmett. Catamorphism. The Comonad.Reader, 2008. I hope this helps. - Gergely From aaronngray.lists at gmail.com Tue Oct 24 09:23:53 2017 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Tue, 24 Oct 2017 14:23:53 +0100 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: Sorry I really dont get on with Bartosz Milewski's stuff its not formal enough and a bit airy fairy even for a programmer. On 24 October 2017 at 08:22, Gabriel Scherer wrote: > Hi Aaron, > > I think you may misunderstand what "category theory for type theory" is > about and its focus area. It is perfectly natural for an outsider to be a > bit confused about the topic you want to learn about (that's the point of > learning), but my impression is that you have some work to do find out what > you actually want before you can usefully tap types-list as a direct > citation source. Maybe some people around here can help you do this > unraveling work (Sean Leather's last reference seems to go in the same > direction), but otherwise there are other places where people may be more > knowledgeable about orienting people living in the gap between "category > theory keywords I hear when I hang around Haskellers" and "category theory > books", for example https://www.reddit.com/r/haskell/ . > > (Reverse engineering what you say, it also sounds like Bartosz Milewski's > book mentioned by Fran?ois Thir? above may be one of the closer to what you > are looking for.) > > On Mon, Oct 23, 2017 at 4:56 PM, Aaron Gray > wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> ilman/listinfo/types-list ] >> >> Thanks everyone, but as far as I can tell none of these books give me any >> real stuff on covariance, contravariance, anamophisms and catamophisms. >> >> On 19 October 2017 at 16:59, John Leo wrote: >> >> > I agree Pierce's book is great, and my favorite overall reference Awodey >> > also has some material on applications to type theory. >> > >> > For specific connections, the best sources are probably lecture notes >> for >> > various summer school courses. My three favorites are those in the >> > "Category Theory and Functional Programming" section of this page: >> > https://github.com/halfaya/BayHac/blob/master/references.md >> > >> > John >> > >> > >> > >> > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad >> > wrote: >> > >> >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> >> ilman/listinfo/types-list ] >> >> >> >> In addition to Pierce's book, which was earlier mentioned, I strongly >> >> recommend Spivak's Category Theory for The Sciences and Lawvere & >> >> Schanuel's Conceptual Mathematics. Even though neither book is >> specifically >> >> for computer scientists, but both books are more modern, very >> accessible, >> >> and frequently discuss CS applications. >> >> >> >> -Moez >> >> >> >> -------- Original message -------- >> >> From: Aaron Gray >> >> Date: 18/10/2017 21:22 (GMT+02:00) >> >> To: The TYPES forum >> >> Subject: [TYPES] Book on Category Theory >> >> >> >> [ The Types Forum, http://lists.seas.upenn.edu/ma >> >> ilman/listinfo/types-list ] >> >> >> >> I am looking for a book on Category Theory that is ideally either >> aimed at >> >> Type Theory or has the relevant topics to support the area. >> >> >> >> I have bought three books on the topic so far, one 'Categories for >> Typesw' >> >> by Crole did not even cover covariance and contravariance.I would also >> >> like >> >> coverage of monoid and monads, and morphisms like anamorphisms and >> >> catamorphisms. >> >> >> >> I am also interested in papers applying category theory to areas of >> type >> >> theory. >> >> >> >> Suggestions of either online or printed material would be appreciated. >> >> >> >> Many tahnks in advance, >> >> -- >> >> Aaron Gray >> >> >> >> Independent Open Source Software Engineer, Computer Language >> Researcher, >> >> Information Theorist, and amateur computer scientist. >> >> >> > >> > >> >> >> -- >> Aaron Gray >> >> Independent Open Source Software Engineer, Computer Language Researcher, >> Information Theorist, and amateur computer scientist. >> > > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From dimitris at microsoft.com Wed Oct 25 16:41:31 2017 From: dimitris at microsoft.com (Dimitrios Vytiniotis) Date: Wed, 25 Oct 2017 20:41:31 +0000 Subject: [TYPES] FW: Book on Category Theory In-Reply-To: References: <002001d34cba$fa37b820$eea72860$@uni-eszterhazy.hu> Message-ID: [FWD from Simon Dobson below] -----Original Message----- From: Simon Dobson [mailto:simoninireland at gmail.com] Sent: 25 October 2017 09:34 To: types-list at LISTS.SEAS.UPENN.EDU Subject: Re: [TYPES] Book on Category Theory On 24/10/2017 12:26, Gergely Buday wrote: > The name catamorphism appears to have been chosen by Lambert Meertens [1]. > The category theoretic machinery behind these was resolved by Grant > Malcolm [2][3], and they were popularized by Meijer, Fokkinga and Paterson[4][5]. > The name comes from the Greek '????-' meaning "downward or according > to". A useful mnemonic is to think of a catastrophe destroying something. It's also worth noting that catamorphisms are closely related to the notion of map/reduce in high-performance computing. Although associated with Google, the idea first appears (as far as I'm aware) in the work of David Skillicorn: David Skillicorn. Models for practical parallel computation. International Journal of Parallel Programming" 20(2), pp. 133--158. 1991. David Skillicorn. Architecture-independent parallel computation. IEEE Computer 23(12), pp. 38--50. January 1990. There's also work by Bird and de Moor, building on that of Meertens. See in particular: Richard Bird and Oege de Moor. Algebra of programming. Prentice Hall. 1997. Cheers, -- -- Simon From bcpierce at cis.upenn.edu Mon Oct 30 08:45:16 2017 From: bcpierce at cis.upenn.edu (Benjamin C. Pierce) Date: Mon, 30 Oct 2017 08:45:16 -0400 Subject: [TYPES] [TYPES/announce] new moderator: Gabriel Scherer In-Reply-To: References: Message-ID: <3453BB76-ECBE-477F-B7F3-98CE5570EB5F@cis.upenn.edu> Many thanks, Dimitrios, for the great job you?ve done over the past three years! The Types list is an important resource for the community, and your stewardship has been much appreciated. And thanks to Gabriel for stepping up to take over this job! - Benjamin > On Oct 30, 2017, at 7:02 AM, Dimitrios Vytiniotis > wrote: > > [ The Types Forum (announcements only), > http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] > > > Dear all, > > It has been my great pleasure to act as the moderator of the TYPES forum and the TYPES/announce mailing list over the past 3.5 years but I feel it is now a good time for a successor. Going forward, I am very happy to announce that Gabriel Scherer (from INRIA) has kindly agreed to take up the job and serve as the next moderator ? I am sure he will do a great job! > > Kind regards, > Dimitrios Vytiniotis From dimitris at microsoft.com Mon Oct 30 07:02:42 2017 From: dimitris at microsoft.com (Dimitrios Vytiniotis) Date: Mon, 30 Oct 2017 11:02:42 +0000 Subject: [TYPES] new moderator: Gabriel Scherer Message-ID: Dear all, It has been my great pleasure to act as the moderator of the TYPES forum and the TYPES/announce mailing list over the past 3.5 years but I feel it is now a good time for a successor. Going forward, I am very happy to announce that Gabriel Scherer (from INRIA) has kindly agreed to take up the job and serve as the next moderator - I am sure he will do a great job! Kind regards, Dimitrios Vytiniotis From nikhil at acm.org Mon Oct 30 09:43:22 2017 From: nikhil at acm.org (Rishiyur Nikhil) Date: Mon, 30 Oct 2017 09:43:22 -0400 Subject: [TYPES] [TYPES/announce] new moderator: Gabriel Scherer In-Reply-To: <3453BB76-ECBE-477F-B7F3-98CE5570EB5F@cis.upenn.edu> References: <3453BB76-ECBE-477F-B7F3-98CE5570EB5F@cis.upenn.edu> Message-ID: Many thanks for undertaking this task, Dimitrios and Gabriel. Nikhil On Mon, Oct 30, 2017 at 8:45 AM, Benjamin C. Pierce wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Many thanks, Dimitrios, for the great job you?ve done over the past three > years! The Types list is an important resource for the community, and your > stewardship has been much appreciated. > > And thanks to Gabriel for stepping up to take over this job! > > - Benjamin > > > On Oct 30, 2017, at 7:02 AM, Dimitrios Vytiniotis < > dimitris at microsoft.com > wrote: > > > > [ The Types Forum (announcements only), > > http://lists.seas.upenn.edu/mailman/listinfo/types-announce < > http://lists.seas.upenn.edu/mailman/listinfo/types-announce> ] > > > > > > Dear all, > > > > It has been my great pleasure to act as the moderator of the TYPES forum > and the TYPES/announce mailing list over the past 3.5 years but I feel it > is now a good time for a successor. Going forward, I am very happy to > announce that Gabriel Scherer (from INRIA) has kindly agreed to take up the > job and serve as the next moderator ? I am sure he will do a great job! > > > > Kind regards, > > Dimitrios Vytiniotis > > From gabriel.scherer at gmail.com Tue Oct 31 10:38:29 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Tue, 31 Oct 2017 14:38:29 +0000 Subject: [TYPES] new moderator: Gabriel Scherer In-Reply-To: References: Message-ID: I'll join in thanking Dimitrios for the nice moderation work -- I'm impressed with the level of dedication and care he put in maintaining this forum -- as well as previous moderators, listed in the "Types-list History" section at the bottom of https://lists.seas.upenn.edu/mailman/listinfo/types-list . I received, from Dimitrios and others, advice and encouragement to be firm in the moderation of both lists. In particular, people want types-announce to send as few announcements as possible, strictly limited to topics relevant to the types and PL community. I will be following this model, but of course people may have different opinions about what is "relevant enough". If you receive a types-announce email that you think does not belong on types-announce, it would be very helpful if you sent me a private email to let me know -- feel free to just say "I would not have accepted this email.", I wouldn't mind. Receiving this sort of feedback will help me tune my filter, and also help me justify my decisions to senders of similar announces in the future. Happy typing On Mon, Oct 30, 2017 at 11:02 AM, Dimitrios Vytiniotis < dimitris at microsoft.com> wrote: > > > Dear all, > > > > It has been my great pleasure to act as the moderator of the TYPES forum > and the TYPES/announce mailing list over the past 3.5 years but I feel it > is now a good time for a successor. Going forward, I am very happy to > announce that Gabriel Scherer (from INRIA) has kindly agreed to take up the > job and serve as the next moderator ? I am sure he will do a great job! > > > > Kind regards, > > Dimitrios Vytiniotis > From aaronngray.lists at gmail.com Wed Nov 1 10:37:53 2017 From: aaronngray.lists at gmail.com (Aaron Gray) Date: Wed, 1 Nov 2017 14:37:53 +0000 Subject: [TYPES] Book on Category Theory In-Reply-To: References: Message-ID: Thank you for all the suggestions I have ordered yet another book on category theory Lavere's - Conceptual Mathematics: A First Introduction to Categories , and am going to follow Steve Awodey's Category Theory Foundations, Lectures on YouTube :- https://www.youtube.com/user/p473r/search?query=Category+Theory I have found what I was looking for now regarding the different types of morphisms so am posting links to the two papers here so other following the thread and are interested can have the references. Graham Hutton's - Bananas in space: extending fold and unfold to exponential types :- http://www.cs.nott.ac.uk/~pszgmh/bib.html#bananas Revisiting Catamorphisms over Datatypes with Embedded Functions :- https://lambda.uta.edu/popl96.pdf These give good extended material to understand applications for algebraic data types, recursive datatypes and datatypes containing functionality. For those who don't know what I am working on and the strange angle I came from I am outside of acedemia I came across the need to understand type theory in order to specify and implement my own object oriented language SOOL which is hopefully going to be a staticly typed feature complete orthoganally complete Object Oriented Language, with meta and grammatical extensions (hence the interest in cata and ana morphisms). Kind regards, Aaron On 1 November 2017 at 02:11, Aaron Gray wrote: > Hi Gabrel, > > Congratulations on becoming moderator I have had a look at your homepage > and your work looks very interesting. I need to read your GADT's and > subtyping paper as this is an area I have avoided looking at due to their > inter-complexity. > > Sorry I have not really responded properly on the list it takes me a long > time to digest things and am currently still learning what is very complex > ground. I do find I understand things when they are very well formulated > this is often in founding papers or in disseminations of them. > > Thank you for all the suggestions I have ordered yet another book on > category theory Lavere's - Conceptual Mathematics: A First Introduction > to Categories > > , and am going to follow Steve Awodey's Category Theory Foundations, > Lectures on YouTube :- > > https://www.youtube.com/user/p473r/search?query=Category+Theory > > I have found what I was looking for now regarding the different types of > morphisms so am posting links to the two papers here so other following the > thread and are interested can have the references. > > Graham Hutton's - Bananas in space: extending fold and unfold to > exponential types :- > > http://www.cs.nott.ac.uk/~pszgmh/bib.html#bananas > > Revisiting Catamorphisms over Datatypes with Embedded Functions :- > > https://lambda.uta.edu/popl96.pdf > > These give good extended matterial to understand the area for recursive > datatypes and datatypes containing functionality. > > For those who don't know what I am working on and the strange angle I came > from I am outside of acedemia I came across the need to understand type > theory in order to specify and implement my own object oriented language > SOOL which is hopefully going to be a staticly typed feature complete > orthoganally complete Object Oriented Language, with meta and grammatical > extensions (hence the interest in cata and ana morphisms). > > Kind regards, > > Aaron > > > On 24 October 2017 at 08:22, Gabriel Scherer > wrote: > >> Hi Aaron, >> >> I think you may misunderstand what "category theory for type theory" is >> about and its focus area. It is perfectly natural for an outsider to be a >> bit confused about the topic you want to learn about (that's the point of >> learning), but my impression is that you have some work to do find out what >> you actually want before you can usefully tap types-list as a direct >> citation source. Maybe some people around here can help you do this >> unraveling work (Sean Leather's last reference seems to go in the same >> direction), but otherwise there are other places where people may be more >> knowledgeable about orienting people living in the gap between "category >> theory keywords I hear when I hang around Haskellers" and "category theory >> books", for example https://www.reddit.com/r/haskell/ . >> >> (Reverse engineering what you say, it also sounds like Bartosz Milewski's >> book mentioned by Fran?ois Thir? above may be one of the closer to what you >> are looking for.) >> >> On Mon, Oct 23, 2017 at 4:56 PM, Aaron Gray >> wrote: >> >>> [ The Types Forum, http://lists.seas.upenn.edu/ma >>> ilman/listinfo/types-list ] >>> >>> Thanks everyone, but as far as I can tell none of these books give me any >>> real stuff on covariance, contravariance, anamophisms and catamophisms. >>> >>> On 19 October 2017 at 16:59, John Leo wrote: >>> >>> > I agree Pierce's book is great, and my favorite overall reference >>> Awodey >>> > also has some material on applications to type theory. >>> > >>> > For specific connections, the best sources are probably lecture notes >>> for >>> > various summer school courses. My three favorites are those in the >>> > "Category Theory and Functional Programming" section of this page: >>> > https://github.com/halfaya/BayHac/blob/master/references.md >>> > >>> > John >>> > >>> > >>> > >>> > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad >>> > wrote: >>> > >>> >> [ The Types Forum, http://lists.seas.upenn.edu/ma >>> >> ilman/listinfo/types-list ] >>> >> >>> >> In addition to Pierce's book, which was earlier mentioned, I strongly >>> >> recommend Spivak's Category Theory for The Sciences and Lawvere & >>> >> Schanuel's Conceptual Mathematics. Even though neither book is >>> specifically >>> >> for computer scientists, but both books are more modern, very >>> accessible, >>> >> and frequently discuss CS applications. >>> >> >>> >> -Moez >>> >> >>> >> -------- Original message -------- >>> >> From: Aaron Gray >>> >> Date: 18/10/2017 21:22 (GMT+02:00) >>> >> To: The TYPES forum >>> >> Subject: [TYPES] Book on Category Theory >>> >> >>> >> [ The Types Forum, http://lists.seas.upenn.edu/ma >>> >> ilman/listinfo/types-list ] >>> >> >>> >> I am looking for a book on Category Theory that is ideally either >>> aimed at >>> >> Type Theory or has the relevant topics to support the area. >>> >> >>> >> I have bought three books on the topic so far, one 'Categories for >>> Typesw' >>> >> by Crole did not even cover covariance and contravariance.I would also >>> >> like >>> >> coverage of monoid and monads, and morphisms like anamorphisms and >>> >> catamorphisms. >>> >> >>> >> I am also interested in papers applying category theory to areas of >>> type >>> >> theory. >>> >> >>> >> Suggestions of either online or printed material would be appreciated. >>> >> >>> >> Many tahnks in advance, >>> >> -- >>> >> Aaron Gray >>> >> >>> >> Independent Open Source Software Engineer, Computer Language >>> Researcher, >>> >> Information Theorist, and amateur computer scientist. >>> >> >>> > >>> > >>> >>> >>> -- >>> Aaron Gray >>> >>> Independent Open Source Software Engineer, Computer Language Researcher, >>> Information Theorist, and amateur computer scientist. >>> >> >> > > > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language Researcher, > Information Theorist, and amateur computer scientist. > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist. From dspivak at gmail.com Wed Nov 8 14:14:56 2017 From: dspivak at gmail.com (David Spivak) Date: Wed, 8 Nov 2017 11:14:56 -0800 Subject: [TYPES] temporal type theory book Message-ID: Dear all, A colleague and I have recently finished a book called "Temporal Type Theory: A topos-theoretic approach to systems and behavior". It can be found on the arXiv here: https://arxiv.org/abs/1710.10258. We would be grateful for any feedback, including comments and questions, pointers to relevant literature, etc. Thanks, David From gabriel.scherer at gmail.com Wed Dec 6 04:57:37 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Wed, 6 Dec 2017 10:57:37 +0100 Subject: [TYPES] [TYPES/announce] subject reduction In-Reply-To: <20171205202623.C5E298C0175@chase.mathstat.dal.ca> References: <20171205202623.C5E298C0175@chase.mathstat.dal.ca> Message-ID: Dear types-announce and types-list, As a moderator of both list, I mistakenly accepted this "Subject reductoin" email on the types-announce list, which is only for announces. Apologies for the noise. If you wish to reply to Peter, please use types-list instead. Below is a collection of the excellent responses already received: From: Simone Martini > > Types, for H.B. Curry, are properties, which are asserted on a subject. > Hence: M:T may be read as ?the subject M has the property T?. > > I am sure others on this list may be more philologically precise. From: Tarmo Uustalu > > Hi Peter, > > It's about 'subject' vs 'predicate' where the subject is the term and > the predicate is the type in a typing judgement s : P. > > Best wishes, > > Tarmo U From: Sophia Drossopoulou > > I do not know why ?subject?. But I think that the first use of the technique in CS as > Mitchell & Plotkin: Abstract types has existential type, POPL 1985 > > And they attributed the technique to > Curry & Feys, Combinatory Logic I, North Holland, 1958 Cheers On Tue, Dec 5, 2017 at 9:26 PM, Peter Selinger wrote: > [ The Types Forum (announcements only), > http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] > > Dear type theorists, > > what is the origin of the term "subject reduction"? I am of course > referring to the property that if M:A and M -> N, then N:A, also > known as type preservation. > > I can sort of see where "reduction" comes into it, but why "subject"? > > Thanks, -- Peter From herman at cs.ru.nl Wed Dec 6 10:18:11 2017 From: herman at cs.ru.nl (Herman Geuvers) Date: Wed, 6 Dec 2017 16:18:11 +0100 Subject: [TYPES] subject reduction In-Reply-To: References: Message-ID: <407de521-ff3d-92b5-bece-5405786d5b37@cs.ru.nl> Dear all, I think the terminology comes from the research on Illative Combinatory Logic (ILC). The notions "subject" and "predicate", respectively for the term M and the type A in a judgment M:A are explained in the publication [Seldin 1919], see below. (I am not sure it is the original source though, Seldin refers to [Curry, Hindley, Seldin, 1972] when talking about subject-reduction, in Section 2.2.2) In ILC, one writes AM for the typing M:A, where A and M are both lambda-terms and A is interpreted as the type (predicate) and M as the term (subject) we want to give a type to. Hindley and Seldin also use the terminology in their 1986 classic book. Best Herman [Seldin 1979] J. P. Seldin. Progress report on generalized functionality. Annals of Mathematical Logic, 17:29?59, 1979. Condensed from manuscript Theory of Generalized functionality informally circulated 1975. Journal now called "Annals of Pure and Applied Logic". see https://www.sciencedirect.com/science/article/pii/0003484379900202 [Hindley and Seldin, 1986] J. R. Hindley and J. P. Seldin. Introduction to Combinators and ?-calculus. Cambridge Univ. Press, England, 1986. [Curry, Hindley, Seldin, 1972] Curry, Haskell B., Hindley, Roger, and Seldin, Jonathan P. Combinatory Logic, vol. II. (North-Holland, Amsterdam, 1972). From halleyy at seas.upenn.edu Wed Dec 6 14:40:22 2017 From: halleyy at seas.upenn.edu (Halley Young) Date: Wed, 6 Dec 2017 14:40:22 -0500 Subject: [TYPES] Formal models of python-like languages Message-ID: Hi all, I have had trouble finding formal research regarding languages with all or most of the properties of core python. Python has the following properties: 1. It is often used in a purely imperative style, and has side effects and pointers. 2. Functions are first class variables, and can be higher-order or anonymous. 3. One can define objects with subclasses and inheritance, but not everything is wrapped in a class. 4. There is dynamic "duck typing," and branches based on runtime checks of types. Even though obviously research on any one of these properties exist, research on languages combining them all, or even just programming with side-effects/pointers and higher order functions, seem to be much rarer. Do you know of any work that has been done formalizing languages with all or most of these features? Thank you, Halley Young From alan.schmitt at polytechnique.org Thu Dec 7 03:37:41 2017 From: alan.schmitt at polytechnique.org (Alan Schmitt) Date: Thu, 07 Dec 2017 09:37:41 +0100 Subject: [TYPES] Formal models of python-like languages In-Reply-To: (Halley Young's message of "Wed, 6 Dec 2017 14:40:22 -0500") References: Message-ID: On 2017-12-06 14:40, Halley Young writes: > I have had trouble finding formal research regarding languages with all or > most of the properties of core python. Python has the following properties: > > 1. It is often used in a purely imperative style, and has side effects and > pointers. > 2. Functions are first class variables, and can be higher-order or > anonymous. > 3. One can define objects with subclasses and inheritance, but not > everything is wrapped in a class. > 4. There is dynamic "duck typing," and branches based on runtime checks of > types. > > Even though obviously research on any one of these properties exist, > research on languages combining them all, or even just programming with > side-effects/pointers and higher order functions, seem to be much rarer. > Do you know of any work that has been done formalizing languages with all > or most of these features? Would JavaScript count (it seems to only be missing pointers)? If so, there are several formalizations of it. http://cs.brown.edu/research/plt/dl/s5/ http://fsl.cs.illinois.edu/index.php/KJS:_A_Complete_Formal_Semantics_of_JavaScript http://jscert.org/ Best, Alan -- OpenPGP Key ID : 040D0A3B4ED2E5C7 Monthly Athmospheric CO?, Mauna Loa Obs. 2017-11: 405.14, 2016-11: 403.53 From james.cheney at gmail.com Thu Dec 7 03:37:07 2017 From: james.cheney at gmail.com (James Cheney) Date: Thu, 7 Dec 2017 08:37:07 +0000 Subject: [TYPES] Formal models of python-like languages In-Reply-To: References: Message-ID: Probably the best place to start would be this: Joe Gibbs Politz, Alejandro Martinez, Matthew Milano, Sumner Warren, Daniel Patterson, Junsong Li, Anand Chitipothu, and Shriram Krishnamurthi. 2013. Python: the full monty. In *Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications* (OOPSLA '13). ACM, New York, NY, USA, 217-232. DOI= http://dx.doi.org/10.1145/2509136.2509536 I am not sure how many of the features you mentioned are covered, but probably some of the authors are on this list and can say more. --James On Dec 7, 2017 5:44 AM, "Halley Young" wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hi all, I have had trouble finding formal research regarding languages with all or most of the properties of core python. Python has the following properties: 1. It is often used in a purely imperative style, and has side effects and pointers. 2. Functions are first class variables, and can be higher-order or anonymous. 3. One can define objects with subclasses and inheritance, but not everything is wrapped in a class. 4. There is dynamic "duck typing," and branches based on runtime checks of types. Even though obviously research on any one of these properties exist, research on languages combining them all, or even just programming with side-effects/pointers and higher order functions, seem to be much rarer. Do you know of any work that has been done formalizing languages with all or most of these features? Thank you, Halley Young From anstenklev at gmail.com Thu Dec 7 04:37:35 2017 From: anstenklev at gmail.com (=?UTF-8?Q?Ansten_M=C3=B8rch_Klev?=) Date: Thu, 7 Dec 2017 10:37:35 +0100 Subject: [TYPES] Subject reduction Message-ID: Dear types-list, Here is some more information regarding the interesting question raised by Peter Selinger. This use of ?subject? and ?predicate? appears indeed already in the first volume (1958) of Curry & Feys, page 272. I could not find it in Curry?s ?Functionality in combinatory logic? (1934). The reason why this terminology was chosen may have been the following. We all know the terms ?subject? and ?predicate? from school grammar. These terms go back to Aristotle?s ?hypokeimenon? and ?kategoroumenon? and are a staple of traditional logic. One of Frege?s main inventions in his *Begriffsschrift* (1879) was to replace these terms with the mathematical terms ?function? and ?argument?. The analysis of propositions into function and argument(s) naturally leads to the idea of a type hierarchy, as first hinted at in Frege?s *Grundgesetze* (1893), and, concomitantly, to the idea that any component of a proposition belongs to a type in such a hierarchy. In a typing judgement, a : A, we are saying that a is an object of type A. Is this judgement itself (or its content) to be analyzed as: function applied to argument(s)? That does not seem quite right, certainly not in Curry?s context, where a is always a function. The traditional terminology therefore presents itself as a natural alternative: a : A is to be analyzed as subject?copula?predicate. The philologically inclined may be interested in ch. 2 of Jonathan Barnes's *Truth, etc.* (Oxford, 2007). The philosophically inclined may perhaps see that the question of the logical form of typing judgements is closely related to the so-called 'concept horse problem' first raised by Frege. Best wishes, Ansten From hindley at waitrose.com Thu Dec 7 05:39:40 2017 From: hindley at waitrose.com (J. R. Hindley) Date: Thu, 7 Dec 2017 10:39:40 +0000 Subject: [TYPES] subject reduction Message-ID: Dear All, Simone and Tarmo and Herman are right. A typing judgment M:A can be thought of as an analogy to the English sentence "John is happy", where "John" is the subject and "happy" is the predicate. (Or perhaps better, John is the subject and happiness is the predicate.) The subject/predicate notation is introduced in Curry and Feys "Combinatory Logic Volume 1" (1958) pp. 272--3 (Section 8E5), followed by a discussion on pp.274--5 (Section 8S2) of the analogy between type-theory (which Curry calls "functionality") and traditional grammar. Happy Christmas, Roger Hindley ----------------------- [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear types-announce and types-list, As a moderator of both list, I mistakenly accepted this "Subject reductoin" email on the types-announce list, which is only for announces. Apologies for the noise. If you wish to reply to Peter, please use types-list instead. Below is a collection of the excellent responses already received: From: Simone Martini > > Types, for H.B. Curry, are properties, which are asserted on a subject. > Hence: M:T may be read as ?the subject M has the property T?. > > I am sure others on this list may be more philologically precise. From: Tarmo Uustalu > > Hi Peter, > > It's about 'subject' vs 'predicate' where the subject is the term and > the predicate is the type in a typing judgement s : P. > > Best wishes, > > Tarmo U From: Sophia Drossopoulou > > I do not know why ?subject?. But I think that the first use of the technique in CS as > Mitchell & Plotkin: Abstract types has existential type, POPL 1985 > > And they attributed the technique to > Curry & Feys, Combinatory Logic I, North Holland, 1958 Cheers On Tue, Dec 5, 2017 at 9:26 PM, Peter Selinger wrote: > [ The Types Forum (announcements only), > http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] > > Dear type theorists, > > what is the origin of the term "subject reduction"? I am of course > referring to the property that if M:A and M -> N, then N:A, also > known as type preservation. > > I can sort of see where "reduction" comes into it, but why "subject"? > > Thanks, -- Peter From giacomo.bergami2 at unibo.it Tue Dec 12 04:57:03 2017 From: giacomo.bergami2 at unibo.it (Giacomo Bergami) Date: Tue, 12 Dec 2017 09:57:03 +0000 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: <1513039984858.1262@unibo.it> References: <1513026197176.80192@unibo.it>,<1513039984858.1262@unibo.it> Message-ID: <1513072620335.94931@unibo.it> Hello Everyone, I am trying to check if it is possible to do reflection (as in Java) using "type safe" languages and, therefore, I am wondering if there is a language having dependent types with subtyping (in particular, I'm not talking of subtyping as in types' universes, but as in record subtyping). All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since then, it seems that whether the type system is consistent or not is still an open problem ( http://lucacardelli.name/Papers/Dependent%20Typechecking.US.pdf ). Therefore, I'm wondering if there are any advances on this regard: moreover, it seems to be that no proof assistant supports this technology. Thanks in advance for any reply, Giacomo Bergami Ph.D Student University of Bologna https://jackbergus.github.io/ From gabriel.scherer at gmail.com Tue Dec 12 05:45:28 2017 From: gabriel.scherer at gmail.com (Gabriel Scherer) Date: Tue, 12 Dec 2017 11:45:28 +0100 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: <1513072620335.94931@unibo.it> References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> Message-ID: There is a language with dependent types and subtyping (including contravariant functions) in: Normalization by Evaluation for Sized Dependent Types Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017) http://www.cse.chalmers.se/~abela/icfp17-long.pdf However, subtyping there is not "higher-order" in the sense of having type-indexed parameters themselves indicate a variance (you cannot abstract over all covariant parametrized types) -- pi-types only track relevant and irrelevant abstraction. In contrast, see the "higher-order subtyping" for F-omega-sub in Polarized Subtyping for Sized Types Andreas Abel, 2008 http://www.cse.chalmers.se/~abela/mscs06.pdf For higher-order subtyping in dependent systems, the two references I know of happen to be also mentioned on the nLab wiki: https://ncatlab.org/nlab/show/directed+homotopy+type+theory they are the work by Harper and Licata on directed type theory (and Dan Licata's PhD thesis), and Andreas Nuyts' master thesis. 2-Dimensional directed dependent type theory Robert Harper, Dan Licata, 2011 http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf Dependently Typed Programming with Domain-Specific Logics Dan Licata, 2011 http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance Andreas Nuyts, 2015 http://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hello Everyone, > > I am trying to check if it is possible to do reflection (as in > Java) using "type safe" languages and, therefore, I am wondering if there > is a language having dependent types with subtyping (in particular, I'm not > talking of subtyping as in types' universes, but as in record subtyping). > All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since > then, it seems that whether the type system is consistent or not is still > an open problem ( http://lucacardelli.name/Papers/Dependent% > 20Typechecking.US.pdf ). > Therefore, I'm wondering if there are any advances on this > regard: moreover, it seems to be that no proof assistant supports this > technology. > Thanks in advance for any reply, > > Giacomo Bergami > Ph.D Student > University of Bologna > https://jackbergus.github.io/ > From sandro.stucki at epfl.ch Tue Dec 12 07:09:37 2017 From: sandro.stucki at epfl.ch (Sandro Stucki) Date: Tue, 12 Dec 2017 13:09:37 +0100 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> Message-ID: There are several instances of Pure Type Systems (PTS) combining dependent types and subtyping in the literature. For example Subtyping dependent types David Aspinall, Adriana Compagnoni. TCS, 2001 http://www.sciencedirect.com/science/article/pii/S0304397500001754 Pure Type Systems with Subtyping Jan Zwanenburg. TLCA 1999 http://dx.doi.org/10.1007/3-540-48959-2_27 Unifying Typing and Subtyping Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf The latter two feature F-omeag-sub-like higher-order subtyping, but none have polarized higher-order subtyping (in the style of Abel's 2008 paper mentioned by Gabriel). Cheers /Sandro On Tue, Dec 12, 2017 at 1:07 PM, Sandro Stucki wrote: > There are several instances of Pure Type Systems (PTS) combining > dependent types and subtyping in the literature. For example > > Subtyping dependent types > David Aspinall, Adriana Compagnoni. TCS, 2001 > http://www.sciencedirect.com/science/article/pii/S0304397500001754 > > Pure Type Systems with Subtyping > Jan Zwanenburg. TLCA 1999 > http://dx.doi.org/10.1007/3-540-48959-2_27 > > Unifying Typing and Subtyping > Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 > http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf > > The latter two feature F-omeag-sub-like higher-order (HO) subtyping, > but none have polarized higher-order subtyping (in the style of Abel's > 2008 paper mentioned by Gabriel). > > Cheers > /Sandro > > On Tue, Dec 12, 2017 at 11:45 AM, Gabriel Scherer > wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> There is a language with dependent types and subtyping (including >> contravariant functions) in: >> >> Normalization by Evaluation for Sized Dependent Types >> Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017) >> http://www.cse.chalmers.se/~abela/icfp17-long.pdf >> >> However, subtyping there is not "higher-order" in the sense of having >> type-indexed parameters themselves indicate a variance (you cannot >> abstract over all covariant parametrized types) -- pi-types only track >> relevant and irrelevant abstraction. In contrast, see the >> "higher-order subtyping" for F-omega-sub in >> >> Polarized Subtyping for Sized Types >> Andreas Abel, 2008 >> http://www.cse.chalmers.se/~abela/mscs06.pdf >> >> >> For higher-order subtyping in dependent systems, the two references >> I know of happen to be also mentioned on the nLab wiki: >> >> https://ncatlab.org/nlab/show/directed+homotopy+type+theory >> >> they are the work by Harper and Licata on directed type theory (and >> Dan Licata's PhD thesis), and Andreas Nuyts' master thesis. >> >> 2-Dimensional directed dependent type theory >> Robert Harper, Dan Licata, 2011 >> http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf >> >> Dependently Typed Programming with Domain-Specific Logics >> Dan Licata, 2011 >> http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf >> >> Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance >> Andreas Nuyts, 2015 >> http://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf >> >> >> On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami >> wrote: >> >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >>> ] >>> >>> Hello Everyone, >>> >>> I am trying to check if it is possible to do reflection (as in >>> Java) using "type safe" languages and, therefore, I am wondering if there >>> is a language having dependent types with subtyping (in particular, I'm not >>> talking of subtyping as in types' universes, but as in record subtyping). >>> All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since >>> then, it seems that whether the type system is consistent or not is still >>> an open problem ( http://lucacardelli.name/Papers/Dependent% >>> 20Typechecking.US.pdf ). >>> Therefore, I'm wondering if there are any advances on this >>> regard: moreover, it seems to be that no proof assistant supports this >>> technology. >>> Thanks in advance for any reply, >>> >>> Giacomo Bergami >>> Ph.D Student >>> University of Bologna >>> https://jackbergus.github.io/ >>> From gc at pps.univ-paris-diderot.fr Tue Dec 12 07:52:49 2017 From: gc at pps.univ-paris-diderot.fr (Giuseppe Castagna) Date: Tue, 12 Dec 2017 13:52:49 +0100 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> Message-ID: <5d206ad4-16b4-eb2e-2b68-e1b75ad6c12b@pps.univ-paris-diderot.fr> An older work in which you have a limited form of intersection types is: G. Castagna and G. Chen: Dependent types with subtyping and late-bound overloading. Information and Computation, vol.?168, n.?1, pag.?1-67, 2001. https://www.irif.fr/~gc/papers/infcomp99.pdf and you may be also interested in AC96b. D. Aspinall and A. Compagnoni. Subtyping dependent types. In Proc. 11th Annual Synposium on Logic in Computer Science, IEEE, pages 86?97, 1996 Beppe On 12/12/17 11:45, Gabriel Scherer wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > There is a language with dependent types and subtyping (including > contravariant functions) in: > > Normalization by Evaluation for Sized Dependent Types > Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017) > http://www.cse.chalmers.se/~abela/icfp17-long.pdf > > However, subtyping there is not "higher-order" in the sense of having > type-indexed parameters themselves indicate a variance (you cannot > abstract over all covariant parametrized types) -- pi-types only track > relevant and irrelevant abstraction. In contrast, see the > "higher-order subtyping" for F-omega-sub in > > Polarized Subtyping for Sized Types > Andreas Abel, 2008 > http://www.cse.chalmers.se/~abela/mscs06.pdf > > > For higher-order subtyping in dependent systems, the two references > I know of happen to be also mentioned on the nLab wiki: > > https://ncatlab.org/nlab/show/directed+homotopy+type+theory > > they are the work by Harper and Licata on directed type theory (and > Dan Licata's PhD thesis), and Andreas Nuyts' master thesis. > > 2-Dimensional directed dependent type theory > Robert Harper, Dan Licata, 2011 > http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf > > Dependently Typed Programming with Domain-Specific Logics > Dan Licata, 2011 > http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf > > Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance > Andreas Nuyts, 2015 > http://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf > > > On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami > wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> ] >> >> Hello Everyone, >> >> I am trying to check if it is possible to do reflection (as in >> Java) using "type safe" languages and, therefore, I am wondering if there >> is a language having dependent types with subtyping (in particular, I'm not >> talking of subtyping as in types' universes, but as in record subtyping). >> All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since >> then, it seems that whether the type system is consistent or not is still >> an open problem ( http://lucacardelli.name/Papers/Dependent% >> 20Typechecking.US.pdf ). >> Therefore, I'm wondering if there are any advances on this >> regard: moreover, it seems to be that no proof assistant supports this >> technology. >> Thanks in advance for any reply, >> >> Giacomo Bergami >> Ph.D Student >> University of Bologna >> https://jackbergus.github.io/ >> From Sergei.Soloviev at irit.fr Tue Dec 12 08:10:41 2017 From: Sergei.Soloviev at irit.fr (Sergei Soloviev) Date: Tue, 12 Dec 2017 14:10:41 +0100 Subject: [TYPES] =?utf-8?b?Pz09P3V0Zi04P3E/ID89PT91dGYtOD9xPyBJOiBPbiBE?= =?utf-8?q?ependent_types_and_Subtyping=27s_consistency?= In-Reply-To: Message-ID: <644d-5a2fd580-34b-27ea7d40@263724168> You may also have a look at the page of Zhaohui Luo at Royal Holloway, there are several papers on coercive subtyping, coherence problems etc for dependent types. https://www.cs.rhul.ac.uk/home/zhaohui/subtyping.html Sergei Soloviev Le Mardi 12 D?cembre 2017 13:09 CET, Sandro Stucki a ?crit: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > There are several instances of Pure Type Systems (PTS) combining > dependent types and subtyping in the literature. For example > > Subtyping dependent types > David Aspinall, Adriana Compagnoni. TCS, 2001 > http://www.sciencedirect.com/science/article/pii/S0304397500001754 > > Pure Type Systems with Subtyping > Jan Zwanenburg. TLCA 1999 > http://dx.doi.org/10.1007/3-540-48959-2_27 > > Unifying Typing and Subtyping > Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 > http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf > > The latter two feature F-omeag-sub-like higher-order subtyping, but > none have polarized higher-order subtyping (in the style of Abel's > 2008 paper mentioned by Gabriel). > > Cheers > /Sandro > > On Tue, Dec 12, 2017 at 1:07 PM, Sandro Stucki wrote: > > There are several instances of Pure Type Systems (PTS) combining > > dependent types and subtyping in the literature. For example > > > > Subtyping dependent types > > David Aspinall, Adriana Compagnoni. TCS, 2001 > > http://www.sciencedirect.com/science/article/pii/S0304397500001754 > > > > Pure Type Systems with Subtyping > > Jan Zwanenburg. TLCA 1999 > > http://dx.doi.org/10.1007/3-540-48959-2_27 > > > > Unifying Typing and Subtyping > > Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 > > http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf > > > > The latter two feature F-omeag-sub-like higher-order (HO) subtyping, > > but none have polarized higher-order subtyping (in the style of Abel's > > 2008 paper mentioned by Gabriel). > > > > Cheers > > /Sandro > > > > On Tue, Dec 12, 2017 at 11:45 AM, Gabriel Scherer > > wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > >> > >> There is a language with dependent types and subtyping (including > >> contravariant functions) in: > >> > >> Normalization by Evaluation for Sized Dependent Types > >> Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017) > >> http://www.cse.chalmers.se/~abela/icfp17-long.pdf > >> > >> However, subtyping there is not "higher-order" in the sense of having > >> type-indexed parameters themselves indicate a variance (you cannot > >> abstract over all covariant parametrized types) -- pi-types only track > >> relevant and irrelevant abstraction. In contrast, see the > >> "higher-order subtyping" for F-omega-sub in > >> > >> Polarized Subtyping for Sized Types > >> Andreas Abel, 2008 > >> http://www.cse.chalmers.se/~abela/mscs06.pdf > >> > >> > >> For higher-order subtyping in dependent systems, the two references > >> I know of happen to be also mentioned on the nLab wiki: > >> > >> https://ncatlab.org/nlab/show/directed+homotopy+type+theory > >> > >> they are the work by Harper and Licata on directed type theory (and > >> Dan Licata's PhD thesis), and Andreas Nuyts' master thesis. > >> > >> 2-Dimensional directed dependent type theory > >> Robert Harper, Dan Licata, 2011 > >> http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf > >> > >> Dependently Typed Programming with Domain-Specific Logics > >> Dan Licata, 2011 > >> http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf > >> > >> Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance > >> Andreas Nuyts, 2015 > >> http://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf > >> > >> > >> On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami >>> wrote: > >> > >>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > >>> ] > >>> > >>> Hello Everyone, > >>> > >>> I am trying to check if it is possible to do reflection (as in > >>> Java) using "type safe" languages and, therefore, I am wondering if there > >>> is a language having dependent types with subtyping (in particular, I'm not > >>> talking of subtyping as in types' universes, but as in record subtyping). > >>> All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since > >>> then, it seems that whether the type system is consistent or not is still > >>> an open problem ( http://lucacardelli.name/Papers/Dependent% > >>> 20Typechecking.US.pdf ). > >>> Therefore, I'm wondering if there are any advances on this > >>> regard: moreover, it seems to be that no proof assistant supports this > >>> technology. > >>> Thanks in advance for any reply, > >>> > >>> Giacomo Bergami > >>> Ph.D Student > >>> University of Bologna > >>> https://jackbergus.github.io/ > >>> From monnier at iro.umontreal.ca Tue Dec 12 08:45:43 2017 From: monnier at iro.umontreal.ca (Stefan Monnier) Date: Tue, 12 Dec 2017 08:45:43 -0500 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: <1513072620335.94931@unibo.it> (Giacomo Bergami's message of "Tue, 12 Dec 2017 09:57:03 +0000") References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> Message-ID: > I am trying to check if it is possible to do reflection (as in Java) > using "type safe" languages and, therefore, I am wondering if there is > a language having dependent types with subtyping (in particular, I'm > not talking of subtyping as in types' universes, but as in record > subtyping). All the infos I got was a paper by Luca Cardelli dated > 2000/2001 but, since then, it seems that whether the type system is > consistent or not is still an open problem I'm not completely sure what is your concrete goal (after all, all cases of reflection I know of are in languages which are already type-safe, such as Common-Lisp, Java, ...), but I wanted to point out that you may not need subtyping in your type system, because you can translate a type-system such as that of Java to a language without subtyping (e.g. using row-polymorphism). See for example: Precision in Practice: A Type-Preserving Java Compiler. Christopher League, Zhong Shao, and Valery Trifonov. In Proc. 12th International Conference on Compiler Construction (CC'03), Warsaw, Poland, April 2003. Where they compile Java to something similar to F?. I don't think Chris found the time to cover Java reflection, but from what I remember of discussions at the time it's not necessarily too hard to add, especially if you're willing to pay the price of a bit of runtime tests in there. Also, since they don't rely on subtyping in their target language, it's probably easier to add dependent types to it. Stefan From giacomo.bergami2 at unibo.it Tue Dec 12 09:27:01 2017 From: giacomo.bergami2 at unibo.it (Giacomo Bergami) Date: Tue, 12 Dec 2017 14:27:01 +0000 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it>, Message-ID: <1513088820986.82807@unibo.it> Actually, my goal are data manipulation using a type safe system. I'm going to provide some practical examples and some definitions (forgive the abuse of notation). a) Dependent Type language is required because I want to express operations that manipulate data at the schema level which, in type theory, corresponds to type manipulation. I would like that one of my functions within the programming language takes a type as an input, and manipulates it as an output type (maybe homotopy type theory comes here in help...?) This comes in help in the data integration scenario, where data translation are provided. The usage of dependent types in relational database scenarios has some examples in this Idris book: https://www.manning.com/books/type-driven-development-with-idris b) Subtyping is required when I know that an operation, such as an embedding, increases the schema of my relation, and hence i want to express the property: \varepsilon : S_1 -> S_2 such that S_2 <: S_1 Counterwise, the projection operator reduces the schema of my elements, and hence \pi : S_1 -> S_2 such that S_2 :> S_1 In particular, I'm referring to Java libraries like Apache Spark and jOOQ which perform the aforementioned operations in a language which doesn't have dependant types. My relational database (after a SQL query) might generate a set of tuples (then, list of terms) of a given schema at the programming level side (all the returned terms have the same type) which is "untyped" (the result provided by the Java JDBC interface has no explicit final schema, it is generally a ResultSet). The library freely assumes by using reflection that the type you provided can be matched by a given field of the database, and hence all the provided terms can be converted into a given class. On the other hand, I would like that the programming language extracts the database metadata (the schema information) and generates a new type at runtime (reflection) and then assures that all the data operations (term operations) provide some operations as expected at the database level. Then, given that some data manipulation operations, check if the typecast to the given class is possible (subtyping). Maybe I'm talking sci-fi, but that is something that I require to create a query language which is correct, and such query language requires a programming language in which to express such constraints. Reflection helps when I want to do some magic, but is not always "correct" and it is more "making educated guesses". Thanks to you all for the papers' suggestions, I'm taking my time to check all the proposed ones. Giacomo ________________________________________ Da: Stefan Monnier Inviato: marted? 12 dicembre 2017 14:45 A: Giacomo Bergami Cc: types-list at lists.seas.upenn.edu Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency > I am trying to check if it is possible to do reflection (as in Java) > using "type safe" languages and, therefore, I am wondering if there is > a language having dependent types with subtyping (in particular, I'm > not talking of subtyping as in types' universes, but as in record > subtyping). All the infos I got was a paper by Luca Cardelli dated > 2000/2001 but, since then, it seems that whether the type system is > consistent or not is still an open problem I'm not completely sure what is your concrete goal (after all, all cases of reflection I know of are in languages which are already type-safe, such as Common-Lisp, Java, ...), but I wanted to point out that you may not need subtyping in your type system, because you can translate a type-system such as that of Java to a language without subtyping (e.g. using row-polymorphism). See for example: Precision in Practice: A Type-Preserving Java Compiler. Christopher League, Zhong Shao, and Valery Trifonov. In Proc. 12th International Conference on Compiler Construction (CC'03), Warsaw, Poland, April 2003. Where they compile Java to something similar to F?. I don't think Chris found the time to cover Java reflection, but from what I remember of discussions at the time it's not necessarily too hard to add, especially if you're willing to pay the price of a bit of runtime tests in there. Also, since they don't rely on subtyping in their target language, it's probably easier to add dependent types to it. Stefan From giacomo.bergami2 at unibo.it Tue Dec 12 10:23:22 2017 From: giacomo.bergami2 at unibo.it (Giacomo Bergami) Date: Tue, 12 Dec 2017 15:23:22 +0000 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: <1513088820986.82807@unibo.it> References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it>, , <1513088820986.82807@unibo.it> Message-ID: <1513092202128.62302@unibo.it> > \varepsilon : S_1 -> S_2 such that S_2 <: S_1 p.s. If I have that the type system is consistent, then I can also provide side proofs within my "programming-language-proof-assistant" and check whether my data manipulation function \varepsilon actually does what I expect. ________________________________________ Da: Types-list per conto di Giacomo Bergami Inviato: marted? 12 dicembre 2017 15:27 A: Stefan Monnier Cc: types-list at lists.seas.upenn.edu Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Actually, my goal are data manipulation using a type safe system. I'm going to provide some practical examples and some definitions (forgive the abuse of notation). a) Dependent Type language is required because I want to express operations that manipulate data at the schema level which, in type theory, corresponds to type manipulation. I would like that one of my functions within the programming language takes a type as an input, and manipulates it as an output type (maybe homotopy type theory comes here in help...?) This comes in help in the data integration scenario, where data translation are provided. The usage of dependent types in relational database scenarios has some examples in this Idris book: https://www.manning.com/books/type-driven-development-with-idris b) Subtyping is required when I know that an operation, such as an embedding, increases the schema of my relation, and hence i want to express the property: \varepsilon : S_1 -> S_2 such that S_2 <: S_1 Counterwise, the projection operator reduces the schema of my elements, and hence \pi : S_1 -> S_2 such that S_2 :> S_1 In particular, I'm referring to Java libraries like Apache Spark and jOOQ which perform the aforementioned operations in a language which doesn't have dependant types. My relational database (after a SQL query) might generate a set of tuples (then, list of terms) of a given schema at the programming level side (all the returned terms have the same type) which is "untyped" (the result provided by the Java JDBC interface has no explicit final schema, it is generally a ResultSet). The library freely assumes by using reflection that the type you provided can be matched by a given field of the database, and hence all the provided terms can be converted into a given class. On the other hand, I would like that the programming language extracts the database metadata (the schema information) and generates a new type at runtime (reflection) and then assures that all the data operations (term operations) provide some operations as expected at the database level. Then, given that some data manipulation operations, check if the typecast to the given class is possible (subtyping). Maybe I'm talking sci-fi, but that is something that I require to create a query language which is correct, and such query language requires a programming language in which to express such constraints. Reflection helps when I want to do some magic, but is not always "correct" and it is more "making educated guesses". Thanks to you all for the papers' suggestions, I'm taking my time to check all the proposed ones. Giacomo ________________________________________ Da: Stefan Monnier Inviato: marted? 12 dicembre 2017 14:45 A: Giacomo Bergami Cc: types-list at lists.seas.upenn.edu Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency > I am trying to check if it is possible to do reflection (as in Java) > using "type safe" languages and, therefore, I am wondering if there is > a language having dependent types with subtyping (in particular, I'm > not talking of subtyping as in types' universes, but as in record > subtyping). All the infos I got was a paper by Luca Cardelli dated > 2000/2001 but, since then, it seems that whether the type system is > consistent or not is still an open problem I'm not completely sure what is your concrete goal (after all, all cases of reflection I know of are in languages which are already type-safe, such as Common-Lisp, Java, ...), but I wanted to point out that you may not need subtyping in your type system, because you can translate a type-system such as that of Java to a language without subtyping (e.g. using row-polymorphism). See for example: Precision in Practice: A Type-Preserving Java Compiler. Christopher League, Zhong Shao, and Valery Trifonov. In Proc. 12th International Conference on Compiler Construction (CC'03), Warsaw, Poland, April 2003. Where they compile Java to something similar to F?. I don't think Chris found the time to cover Java reflection, but from what I remember of discussions at the time it's not necessarily too hard to add, especially if you're willing to pay the price of a bit of runtime tests in there. Also, since they don't rely on subtyping in their target language, it's probably easier to add dependent types to it. Stefan From giacomo.bergami2 at unibo.it Thu Dec 14 08:37:12 2017 From: giacomo.bergami2 at unibo.it (Giacomo Bergami) Date: Thu, 14 Dec 2017 13:37:12 +0000 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> <1513088820986.82807@unibo.it> <1513092202128.62302@unibo.it>, Message-ID: <1513258632830.11158@unibo.it> A little clarification on the definition of reflection I have in mind (quoting from Wikipedia, https://en.wikipedia.org/wiki/Reflection_(computer_programming)): >> Discover and modify source-code constructions (such as code blocks, classes, methods, protocols, etc.) as first-class objects at runtime. In my case, I'm aware that I cannot change a definition of a type at runtime (it won't be safe at all), but sometimes I'd like to transform it into another type while I perform some data operations (and then, create a new type from a previous one). Some operations (like the ones that can be carried out in Java and in some other frameworks) are directly provided by the user, and the user might just (implicitly) define a type while performing data manipulations. So the notion of subtyping seems to be to partially solve the problem of "generating a different type from the previous one" for the relational model (SQL over Relational Database Management Systems). For the XML model, I sense that something like CDuce may be used (http://www.cduce.org/), but all these approaches strictly depend on the data model of choice (for instance, I'm currently working on graph databases...) I'm also providing a short reply to the people that previously sent some infos that I managed to check within my (little) spare time from main research (thanks by the way for your continuous suggestions). For all the remaining suggestions I'm just slowly reviewing them (My main research field are [graph] databases, and I have knowledge of type theory from my master degree studies). @Sergei Soloviev I sense that these solutions are very near to something that I'm looking for, even though they state that there is still some more work to do. In particular, I'm referring to I \lambda <= conclusions: > We already have a sound and complete algorithmic system and we **believe** it is decidable, though we do not have the proof **yet**. Hope that they'll found a proof soon :) @Matthieu Sozeau UR seems to be like a start, but it doesn't have the subtyping notion (correct me if I'm wrong. See above.). @Ryan Wisnesky I would like that group by operations would be represented (agreed, I could exted your paper work to add grouping functions, but those are not represented for the moment). Moreover, I also have Spivak's book on Category Theory, but there are no insight on nested representations (and hence, no reference on group by operations). That's why I was planning to design an ad-hoc language for data "manipulations". Giacomo Bergami Da: Matthieu Sozeau Inviato: gioved? 14 dicembre 2017 13:34 A: Giacomo Bergami Cc: Stefan Monnier; types-list at lists.seas.upenn.edu Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency ? Hi, I might be far off but it sounds close to what A. Chlipala's Ur/web language is doing, and it does have a limited form of dependent types, expressive type-level programming with records and a type-safe interface to SQL. ??http://www.impredicative.com/ur/ Best, -- Matthieu On Tue, Dec 12, 2017 at 5:45 PM Giacomo Bergami wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > \varepsilon : S_1 -> S_2 such that S_2 <: S_1 p.s. If I have that the type system is consistent, then I can also provide side proofs within my "programming-language-proof-assistant" and check whether my data manipulation function \varepsilon actually does what I expect. ________________________________________ Da: Types-list per conto di Giacomo Bergami Inviato: marted? 12 dicembre 2017 15:27 A: Stefan Monnier Cc: types-list at lists.seas.upenn.edu Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Actually, my goal are data manipulation using a type safe system. I'm going to provide some practical examples and some definitions (forgive the abuse of notation). a) Dependent Type language is required because I want to express operations that manipulate data at the schema level which, in type theory, corresponds to? type manipulation.? I would like that one of my functions within the programming language takes a type as an input, and manipulates it as an output type? (maybe homotopy type theory comes here in help...?) This comes in help in the data integration scenario, where data translation are provided. The usage of dependent types in relational database scenarios has some examples in this Idris book: https://www.manning.com/books/type-driven-development-with-idris b) Subtyping is required when I know that an operation, such as an embedding, increases the schema of my relation, and hence i want to express the property: \varepsilon : S_1 -> S_2 such that S_2 <: S_1 Counterwise, the projection operator reduces the schema of my elements, and hence \pi : S_1 -> S_2 such that S_2 :> S_1 In particular, I'm referring to Java libraries like Apache Spark and jOOQ which perform the aforementioned operations in a language which doesn't have dependant types. My relational database (after a SQL query) might generate a set of tuples (then, list of terms) of a given? schema at the programming level side (all the returned terms have the same type) which is "untyped" (the result provided by the Java? JDBC interface has no explicit final schema, it is generally a ResultSet). The library freely assumes by using reflection that the type you provided can be matched by a given field of the database, and hence all the provided terms can be converted into a given class. On the other hand, I would like that the programming language extracts the database metadata (the schema information) and generates a new type at runtime (reflection) and then assures that all the data operations (term operations) provide some operations as expected at the database level. Then, given that some data manipulation operations, check if the typecast to the given class is possible (subtyping). Maybe I'm talking sci-fi, but that is something that I require to create a query language which is correct, and such query language requires a programming language in which to express such constraints. Reflection helps when I want to do some magic, but is not always "correct" and it is more "making educated guesses". Thanks to you all for the papers' suggestions, I'm taking my time to check all the proposed ones. ? ? ?Giacomo ________________________________________ Da: Stefan Monnier Inviato: marted? 12 dicembre 2017 14:45 A: Giacomo Bergami Cc: types-list at lists.seas.upenn.edu Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency > I am trying to check if it is possible to do reflection (as in Java) > using "type safe" languages and, therefore, I am wondering if there is > a language having dependent types with subtyping (in particular, I'm > not talking of subtyping as in types' universes, but as in record > subtyping). All the infos I got was a paper by Luca Cardelli dated > 2000/2001 but, since then, it seems that whether the type system is > consistent or not is still an open problem I'm not completely sure what is your concrete goal (after all, all cases of reflection I know of are in languages which are already type-safe, such as Common-Lisp, Java, ...), but I wanted to point out that you may not need subtyping in your type system, because you can translate a type-system such as that of Java to a language without subtyping (e.g. using row-polymorphism). See for example: ? ? Precision in Practice: A Type-Preserving Java Compiler. ? ? Christopher League, Zhong Shao, and Valery Trifonov.? In Proc. 12th ? ? International Conference on Compiler Construction (CC'03), Warsaw, ? ? Poland, April 2003. Where they compile Java to something similar to F?. I don't think Chris found the time to cover Java reflection, but from what I remember of discussions at the time it's not necessarily too hard to add, especially if you're willing to pay the price of a bit of runtime tests in there. Also, since they don't rely on subtyping in their target language, it's probably easier to add dependent types to it. ? ? ? ? Stefan From marco.servetto at gmail.com Fri Dec 15 21:15:41 2017 From: marco.servetto at gmail.com (Marco Servetto) Date: Sat, 16 Dec 2017 15:15:41 +1300 Subject: [TYPES] An Expressive Type System helping for run-time verification Message-ID: We plan to leverage expressive type systems to support the correctness of run-time verification. For now we are focusing on class invariants only. We are struggling to find related works about "sound/correct" run time verification, in the context of pure object oriented languages. Please, can you suggest us some reference? Marco. p.s. For now, we are even struggling to define formally what should it means to soundly enforce a (multi object) class invariant at run time, without relying on pre-post conditions but just on the semantic of the language. From dlucanu at info.uaic.ro Sat Dec 16 10:05:12 2017 From: dlucanu at info.uaic.ro (Dorel Lucanu) Date: Sat, 16 Dec 2017 17:05:12 +0200 Subject: [TYPES] An Expressive Type System helping for run-time verification In-Reply-To: References: Message-ID: <2db8c40b-b096-0f96-8e8a-7ff0dadf9283@info.uaic.ro> I think that Monitoring-oriented programming (MOP) Framework is a strong related approach, even if it is not directly based on type systems. MOP is developed by FSL research group at UIUC led by Grigore Rosu: http://fsl.cs.illinois.edu/index.php/MOP MPOP is a part of a more complex project devoted to run-time verification: http://fsl.cs.illinois.edu/index.php/Runtime_Verification Dorel On 16/12/2017 04:15, Marco Servetto wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > We plan to leverage expressive type systems to support the correctness > of run-time verification. > For now we are focusing on class invariants only. > > We are struggling to find related works about "sound/correct" run time > verification, > in the context of pure object oriented languages. > Please, can you suggest us some reference? > > Marco. > > p.s. > For now, we are even struggling to define formally what should it means to > soundly enforce a (multi object) class invariant at run time, without relying on > pre-post conditions but just on the semantic of the language. From delesley at gmail.com Fri Dec 15 13:01:22 2017 From: delesley at gmail.com (DeLesley Hutchins) Date: Fri, 15 Dec 2017 10:01:22 -0800 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> Message-ID: An additional example is: "Pure Subtype Systems", POPL 2010 https://dl.acm.org/citation.cfm?id=1706334 Which shows that you can combine subtyping and dependent typing into a single relation. The PSS theory is currently incomplete -- you need a stratified universe of types to prove strong normalization. - DeLesley On Tue, Dec 12, 2017 at 4:09 AM, Sandro Stucki wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > There are several instances of Pure Type Systems (PTS) combining > dependent types and subtyping in the literature. For example > > Subtyping dependent types > David Aspinall, Adriana Compagnoni. TCS, 2001 > http://www.sciencedirect.com/science/article/pii/S0304397500001754 > > Pure Type Systems with Subtyping > Jan Zwanenburg. TLCA 1999 > http://dx.doi.org/10.1007/3-540-48959-2_27 > > Unifying Typing and Subtyping > Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 > http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf > > The latter two feature F-omeag-sub-like higher-order subtyping, but > none have polarized higher-order subtyping (in the style of Abel's > 2008 paper mentioned by Gabriel). > > Cheers > /Sandro > > On Tue, Dec 12, 2017 at 1:07 PM, Sandro Stucki > wrote: > > There are several instances of Pure Type Systems (PTS) combining > > dependent types and subtyping in the literature. For example > > > > Subtyping dependent types > > David Aspinall, Adriana Compagnoni. TCS, 2001 > > http://www.sciencedirect.com/science/article/pii/S0304397500001754 > > > > Pure Type Systems with Subtyping > > Jan Zwanenburg. TLCA 1999 > > http://dx.doi.org/10.1007/3-540-48959-2_27 > > > > Unifying Typing and Subtyping > > Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 > > http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf > > > > The latter two feature F-omeag-sub-like higher-order (HO) subtyping, > > but none have polarized higher-order subtyping (in the style of Abel's > > 2008 paper mentioned by Gabriel). > > > > Cheers > > /Sandro > > > > On Tue, Dec 12, 2017 at 11:45 AM, Gabriel Scherer > > wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list ] > >> > >> There is a language with dependent types and subtyping (including > >> contravariant functions) in: > >> > >> Normalization by Evaluation for Sized Dependent Types > >> Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017) > >> http://www.cse.chalmers.se/~abela/icfp17-long.pdf > >> > >> However, subtyping there is not "higher-order" in the sense of having > >> type-indexed parameters themselves indicate a variance (you cannot > >> abstract over all covariant parametrized types) -- pi-types only track > >> relevant and irrelevant abstraction. In contrast, see the > >> "higher-order subtyping" for F-omega-sub in > >> > >> Polarized Subtyping for Sized Types > >> Andreas Abel, 2008 > >> http://www.cse.chalmers.se/~abela/mscs06.pdf > >> > >> > >> For higher-order subtyping in dependent systems, the two references > >> I know of happen to be also mentioned on the nLab wiki: > >> > >> https://ncatlab.org/nlab/show/directed+homotopy+type+theory > >> > >> they are the work by Harper and Licata on directed type theory (and > >> Dan Licata's PhD thesis), and Andreas Nuyts' master thesis. > >> > >> 2-Dimensional directed dependent type theory > >> Robert Harper, Dan Licata, 2011 > >> http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf > >> > >> Dependently Typed Programming with Domain-Specific Logics > >> Dan Licata, 2011 > >> http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf > >> > >> Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance > >> Andreas Nuyts, 2015 > >> http://people.cs.kuleuven.be/~dominique.devriese/ > ThesisAndreasNuyts.pdf > >> > >> > >> On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami < > giacomo.bergami2 at unibo.it > >>> wrote: > >> > >>> [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list > >>> ] > >>> > >>> Hello Everyone, > >>> > >>> I am trying to check if it is possible to do reflection (as > in > >>> Java) using "type safe" languages and, therefore, I am wondering if > there > >>> is a language having dependent types with subtyping (in particular, > I'm not > >>> talking of subtyping as in types' universes, but as in record > subtyping). > >>> All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, > since > >>> then, it seems that whether the type system is consistent or not is > still > >>> an open problem ( http://lucacardelli.name/Papers/Dependent% > >>> 20Typechecking.US.pdf ). > >>> Therefore, I'm wondering if there are any advances on this > >>> regard: moreover, it seems to be that no proof assistant supports this > >>> technology. > >>> Thanks in advance for any reply, > >>> > >>> Giacomo Bergami > >>> Ph.D Student > >>> University of Bologna > >>> https://jackbergus.github.io/ > >>> > From fp at cs.cmu.edu Sat Dec 16 15:33:39 2017 From: fp at cs.cmu.edu (Frank Pfenning) Date: Sat, 16 Dec 2017 15:33:39 -0500 Subject: [TYPES] I: On Dependent types and Subtyping's consistency In-Reply-To: <1513072620335.94931@unibo.it> References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> Message-ID: Below are some additional references, that include not only subtyping and dependent types, but also intersection types (which, in my opinion, are important whenever subtyping is in play). There are also conference papers about each of these lines of research, but by necessity they tend to be less tutorial. Joshua Dunfield, A Unified System of Type Refinements , PhD Thesis, CMU, August 2007. William Lovas, Refinement Types for Logical Frameworks , PhD Thesis, CMU, September 2010. Joshua combines subtyping, intersection, union, and dependent types in a single language. There is also an implementation of an ML subset called Stardust (not sure about its current status). Soundness here is not at all obvious; there are some traps that must be avoided. In this regard, see also Davies & Pfenning, ICFP 2000. William combines pure dependent types and intersection types and derives from that a principled notion of subtyping appropriate for a logical framework. Here, the key is to respect the open-endedness of logical framework specifications. - Frank On Tue, Dec 12, 2017 at 4:57 AM, Giacomo Bergami wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hello Everyone, > > I am trying to check if it is possible to do reflection (as in > Java) using "type safe" languages and, therefore, I am wondering if there > is a language having dependent types with subtyping (in particular, I'm not > talking of subtyping as in types' universes, but as in record subtyping). > All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since > then, it seems that whether the type system is consistent or not is still > an open problem ( http://lucacardelli.name/Papers/Dependent% > 20Typechecking.US.pdf ). > Therefore, I'm wondering if there are any advances on this > regard: moreover, it seems to be that no proof assistant supports this > technology. > Thanks in advance for any reply, > > Giacomo Bergami > Ph.D Student > University of Bologna > https://jackbergus.github.io/ > -- Frank Pfenning, Professor and Head Department of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3891 http://www.cs.cmu.edu/~fp +1 412 268-6343 GHC 7019 From mail at kenkubota.de Sat Dec 16 17:55:10 2017 From: mail at kenkubota.de (Ken Kubota) Date: Sat, 16 Dec 2017 23:55:10 +0100 Subject: [TYPES] On Dependent types and Subtyping's consistency In-Reply-To: <1513072620335.94931@unibo.it> References: <1513026197176.80192@unibo.it> <1513039984858.1262@unibo.it> <1513072620335.94931@unibo.it> Message-ID: <0AEA0653-7692-424C-942D-A051B9DBB1DB@kenkubota.de> The software implementation described at http://www.owlofminerva.net/files/formulae.pdf has many similarities to your reference http://lucacardelli.name/Papers/Dependent%20Typechecking.US.pdf It implements the Type:Type rule (cf. p. 11), hence, provides an unstratified type system, has subtypes similar to the predicate subtypes in PVS (see: http://www.csl.sri.com/papers/cade92-pvs/cade92-pvs.pdf, p. 2), and a mechanism to preserve the type dependencies within the type symbol similar to the de Bruijn indices, but used for type variables within the type information only, such that no explicit type inference rules are required, but the type directly results from lambda conversion (or lambda application). Mathematical entities may have different types (i.e., it is a Curry-style rather than a Church-style system). Kind regards, Ken Kubota ____________________ Ken Kubota http://doi.org/10.4444/100 > Am 12.12.2017 um 10:57 schrieb Giacomo Bergami : > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello Everyone, > > I am trying to check if it is possible to do reflection (as in Java) using "type safe" languages and, therefore, I am wondering if there is a language having dependent types with subtyping (in particular, I'm not talking of subtyping as in types' universes, but as in record subtyping). All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since then, it seems that whether the type system is consistent or not is still an open problem ( http://lucacardelli.name/Papers/Dependent%20Typechecking.US.pdf ). > Therefore, I'm wondering if there are any advances on this regard: moreover, it seems to be that no proof assistant supports this technology. > Thanks in advance for any reply, > > Giacomo Bergami > Ph.D Student > University of Bologna > https://jackbergus.github.io/ From P.B.Levy at cs.bham.ac.uk Tue Dec 19 04:10:32 2017 From: P.B.Levy at cs.bham.ac.uk (Paul Blain Levy) Date: Tue, 19 Dec 2017 09:10:32 +0000 Subject: [TYPES] judgemental eta for function types Message-ID: <3dd4de62-f422-ecf5-b859-b37e3974c499@cs.bham.ac.uk> Dear all, I have a question about systems like Coq and Agda that are based on intensional type theory, and the way they treat the eta-law for dependent function? types, including types of the form A->B and A*B and 1.? I have been told that they allow this eta-law as a judgemental equality, not just propositional.? (By constrast, the eta-law for types such as A+B and 0 is allowed as only as a propositional equality, in order to keep judgements decidable, and allegedly for philosophical reasons too.) My question is, how useful is this facility (judgemental eta-law for function types) in practice?? Can you give me examples of the ways that users commonly make use of it?? To put the question differently, if the eta-law for function types were available only as a propositional equality, how inconvenient would that be for users?? Do you think that allowing it as a judgemental equality has significantly boosted the popularity of these systems? Regards, Paul From rodolphe.lepigre at inria.fr Thu Dec 21 05:34:53 2017 From: rodolphe.lepigre at inria.fr (Rodolphe Lepigre) Date: Thu, 21 Dec 2017 11:34:53 +0100 Subject: [TYPES] I: On Dependent types and Subtyping's consistency Message-ID: <20171221103453.GU24481@HPArchRod.localdomain> > Hello Everyone, > > I am trying to check if it is possible to do reflection (as in Java) using > "type safe" languages and, therefore, I am wondering if there is a language > having dependent types with subtyping (in particular, I'm not talking of > subtyping as in types' universes, but as in record subtyping). All the infos > I got was a paper by Luca Cardelli dated 2000/2001 but, since then, it seems > that whether the type system is consistent or not is still an open problem ( > http://lucacardelli.name/Papers/Dependent%20Typechecking.US.pdf ). > > Therefore, I'm wondering if there are any advances on this regard: moreover, > it seems to be that no proof assistant supports this technology. Thanks in > advance for any reply, > > Giacomo Bergami > Ph.D Student > University of Bologna > https://jackbergus.github.io/ Hi there, You might also be interested in the PML language, which was the subject of my (recently defended) thesis. Roughly, the ideas of PML are the following: - start with an ML-like programming language (polymorphism, recursion, ...), - extend the type system with a way of proving program properties, - put everything together with subtyping. The main point of subtyping in this framework is to obtain a practical way of type-checking Curry-style programs, which is difficult. Here is a (non-exhaustive) list of features: - a very general form of implicit (non-coercive) subtyping, - Curry-style quantifiers and dependent function type, - an equality type for specifying program properties, - control operators (interpreted with classical logic), - general recursion with termination checking, - inductive and coinductive types (sized types). Relevant papers and implementation: http://lepigre.fr/files/docs/lepigre2017_pml2.pdf (examples in PML) https://github.com/rlepigre/phd/blob/master/manuscript_archived.pdf (thesis) https://github.com/rlepigre/pml (implementation of PML) More stuff on subtyping (joint work with Christophe Raffalli) and the SubML language (which has subtyping, but does not have dependent types, but PML is base on the same ideas): http://lepigre.fr/files/docs/lepigre2017_subml.pdf (subtyping theory) https://github.com/rlepigre/subml (SubML language implementation) https://rlepigre.github.io/subml (SubML language, try it online) I hope this helps! Cheers, Rodolphe -- Rodolphe Lepigre Inria (Deducteam), LSV, CNRS, Universit? Paris-Saclay, FRANCE https://lepigre.fr From andreas.abel at ifi.lmu.de Thu Dec 21 12:46:38 2017 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Thu, 21 Dec 2017 18:46:38 +0100 Subject: [TYPES] judgemental eta for function types In-Reply-To: <3dd4de62-f422-ecf5-b859-b37e3974c499@cs.bham.ac.uk> References: <3dd4de62-f422-ecf5-b859-b37e3974c499@cs.bham.ac.uk> Message-ID: For the use of eta for sigma types, see Conor McBride's Outrageous but meaningful coincidences Higher-order unification modulo eta is used in a significant way there. > Do you think that > allowing it as a judgemental equality has significantly boosted the > popularity of these systems? Do you care what (A) I think or whether (B) "judgemental equality has significantly boosted the popularity of these systems?" ;-) (A) No clue. (B) Let's ask an omniscient being in our afterlive. Cheers, Andreas On 19.12.2017 10:10, Paul Blain Levy wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear all, > > I have a question about systems like Coq and Agda that are based on > intensional type theory, and the way they treat the eta-law for > dependent function? types, including types of the form A->B and A*B and > 1.? I have been told that they allow this eta-law as a judgemental > equality, not just propositional.? (By constrast, the eta-law for types > such as A+B and 0 is allowed as only as a propositional equality, in > order to keep judgements decidable, and allegedly for philosophical > reasons too.) > > My question is, how useful is this facility (judgemental eta-law for > function types) in practice?? Can you give me examples of the ways that > users commonly make use of it?? To put the question differently, if the > eta-law for function types were available only as a propositional > equality, how inconvenient would that be for users?? Do you think that > allowing it as a judgemental equality has significantly boosted the > popularity of these systems? > > Regards, > > Paul > > -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www.cse.chalmers.se/~abela/ From matthieu.sozeau at inria.fr Fri Dec 22 03:55:39 2017 From: matthieu.sozeau at inria.fr (Matthieu Sozeau) Date: Fri, 22 Dec 2017 08:55:39 +0000 Subject: [TYPES] judgemental eta for function types In-Reply-To: <3dd4de62-f422-ecf5-b859-b37e3974c499@cs.bham.ac.uk> References: <3dd4de62-f422-ecf5-b859-b37e3974c499@cs.bham.ac.uk> Message-ID: Dear Paul, On Tue, Dec 19, 2017 at 12:35 PM Paul Blain Levy wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear all, > > I have a question about systems like Coq and Agda that are based on > intensional type theory, and the way they treat the eta-law for > dependent function types, including types of the form A->B and A*B and > 1. I have been told that they allow this eta-law as a judgemental > equality, not just propositional. (By constrast, the eta-law for types > such as A+B and 0 is allowed as only as a propositional equality, in > order to keep judgements decidable, and allegedly for philosophical > reasons too.) > > My question is, how useful is this facility (judgemental eta-law for > function types) in practice? Can you give me examples of the ways that > users commonly make use of it? It might seem annecdotical, but it's quite useful in practice to have ? A (fun x : A => P x) be convertible to ? A P. It's not unusual for a user to declare a value of type ? A P and to use it to inhabit ? A (fun x : A => P x). It comes up with typeclass instances in practice for example. I also comes up in formalizations of structures based on functions where some primitives definitions eta-expand. Typically for composition of functions you will have [f ? id = (fun x => f x) = f], and it's neat to have it be definitional. The fact that function composition and identity form a monoid "strictly" or on the nose is used for example in [1] to show that the Yoneda translation of a category is a category with equations holding up-to definitional equality. ? > To put the question differently, if the > eta-law for function types were available only as a propositional > equality, how inconvenient would that be for users? Do you think that > allowing it as a judgemental equality has significantly boosted the > popularity of these systems? > > I can't judge how significant it is. Note that without a definitional equality for eta, in older Coq versions for example, users were typically adding the functional extensionality axiom to derive it. [1] The Definitional Side of the Forcing. G. Jaber et al.. https://hal.archives-ouvertes.fr/hal-01319066 Best, -- Matthieu