[-- Attachment #1.1: Type: text/plain, Size: 1186 bytes --] is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ? this construction would be useful for forming theoretical background of dependent type system. for example, compose two functions f : (A x -> B y) g : (B n -> C z) will give us a function of type (A n -> C z) another example would be the following generalized composition in cartesian closed category : f : (t1, t2) -> (t3, t4) g : (t, t3, t4) -> (t6, t7) f;g : (t, t1, t2) -> (t6, t7) and f : (t1, t2) -> (t, t3, t4) g : (t3, t4) -> (t6, t7) f;g : (t, t1, t2) -> (t, t6, t7) this can be called `cut` because it looks like gentzen's cut rule in sequent calculus, and it can be used to provide semantic for a stack based concatenative programming language. ------ xieyuheng -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1548 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 3505 bytes --] Hi, Xieyuheng. On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng wrote: > > is there a categorical construction to generalize arrow composition, > by allowing domain and codomain to be refined (or changed) by the > composition ? > > this construction would be useful for > forming theoretical background of dependent type system. > > for example, compose two functions > f : (A x -> B y) > g : (B n -> C z) > will give us a function of type (A n -> C z) > I can't figure out what rule you're using to get that type. If n unifies with y, how did x become n also? That's what I'm guessing you're trying. > another example would be the following generalized composition in > cartesian closed category : > f : (t1, t2) -> (t3, t4) > g : (t, t3, t4) -> (t6, t7) > f;g : (t, t1, t2) -> (t6, t7) > and > f : (t1, t2) -> (t, t3, t4) > g : (t3, t4) -> (t6, t7) > f;g : (t, t1, t2) -> (t, t6, t7) > this can be called `cut` > because it looks like gentzen's cut rule in sequent calculus, > and it can be used to provide semantic > for a stack based concatenative programming language. > This looks more like a combination of composition and tensoring, in a monoidal category. Based on some stuff in a blog post (https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivaria.html), the cut rule is instead composition in a polycategory, and you can only cut out one type at a time. I'm thinking the first "generalized composition" could be explained thus: f only looks at the top two stack elements, and replaces them with three others. But the stack generally has additional elements, which I'll abstract away as Γ: f : (Γ, t1, t2) -> (Γ, t3, t4) g has a similar story, but we use a different stack/context variable to avoid accidental constraints: g : (Δ, t, t3, t4) -> (Δ, t6, t7) To compose these, we need (Γ, t3, t4) to unify with (Δ, t, t3, t4), so (Γ := Δ, t), and f;g : (Δ, t, t1, t2) -> (Δ, t6, t7) which we shorten to (t, t1, t2) -> (t6, t7). So your composable operators seem to be substitutions (morphisms between contexts) that are polymorphic in most of the context. All but a finite chunk all the way on the right. Composition would presumably be composition of substitutions, after instantiating them with the principal unifier. For simply-typed systems, contexts and substitutions can be modeled in a monoidal category, which includes cartesian closed categories. For dependent type systems, other kinds of categories are used, like contextual categories and categories with families; hopefully what you want is still instantiation and composition of this new kind of substitution. I'm not an expert on the kinds of categorical structures involved, but hopefully polymorphic substitutions is a good way of thinking about what you're doing, which connects it with categorical models. Beware that with dependent types, there generally are not principal unifiers, due to binding operators appearing in types. But concatenative people don't seem to like binders, so maybe you dodged the bullet. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4163 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 3840 bytes --] sorry, I had a typo, the first example should be : f : (A x -> B x) g : (B n -> C z) will give us a function of type (A n -> C z) On Tuesday, June 19, 2018 at 2:58:05 AM UTC+8, Matt Oliveri wrote: > > Hi, Xieyuheng. > > On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng wrote: >> >> is there a categorical construction to generalize arrow composition, >> by allowing domain and codomain to be refined (or changed) by the >> composition ? >> >> this construction would be useful for >> forming theoretical background of dependent type system. >> >> for example, compose two functions >> f : (A x -> B y) >> g : (B n -> C z) >> will give us a function of type (A n -> C z) >> > > I can't figure out what rule you're using to get that type. If n unifies > with y, how did x become n also? That's what I'm guessing you're trying. > > >> another example would be the following generalized composition in >> cartesian closed category : >> f : (t1, t2) -> (t3, t4) >> g : (t, t3, t4) -> (t6, t7) >> f;g : (t, t1, t2) -> (t6, t7) >> and >> f : (t1, t2) -> (t, t3, t4) >> g : (t3, t4) -> (t6, t7) >> f;g : (t, t1, t2) -> (t, t6, t7) >> this can be called `cut` >> because it looks like gentzen's cut rule in sequent calculus, >> and it can be used to provide semantic >> for a stack based concatenative programming language. >> > > This looks more like a combination of composition and tensoring, in a > monoidal category. Based on some stuff in a blog post ( > https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivaria.html), > the cut rule is instead composition in a polycategory, and you can only cut > out one type at a time. > > I'm thinking the first "generalized composition" could be explained thus: > f only looks at the top two stack elements, and replaces them with three > others. But the stack generally has additional elements, which I'll > abstract away as Γ: > f : (Γ, t1, t2) -> (Γ, t3, t4) > > g has a similar story, but we use a different stack/context variable to > avoid accidental constraints: > g : (Δ, t, t3, t4) -> (Δ, t6, t7) > > To compose these, we need (Γ, t3, t4) to unify with (Δ, t, t3, t4), so (Γ > := Δ, t), and > f;g : (Δ, t, t1, t2) -> (Δ, t6, t7) > which we shorten to (t, t1, t2) -> (t6, t7). > > So your composable operators seem to be substitutions (morphisms between > contexts) that are polymorphic in most of the context. All but a finite > chunk all the way on the right. Composition would presumably be composition > of substitutions, after instantiating them with the principal unifier. > > For simply-typed systems, contexts and substitutions can be modeled in a > monoidal category, which includes cartesian closed categories. For > dependent type systems, other kinds of categories are used, like contextual > categories and categories with families; hopefully what you want is still > instantiation and composition of this new kind of substitution. > > I'm not an expert on the kinds of categorical structures involved, but > hopefully polymorphic substitutions is a good way of thinking about what > you're doing, which connects it with categorical models. > > Beware that with dependent types, there generally are not principal > unifiers, due to binding operators appearing in types. But concatenative > people don't seem to like binders, so maybe you dodged the bullet. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 5172 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 4315 bytes --] thank you Matt Oliveri. the substitutions you used above explains my examples perfectly. I also found a bug in my second examples : f : (A, t1, t2) -> (A, t, t3, t4) g : (B, t3, t4) -> (B, t6, t7) (unify) B = (A, t) f : (A, t1, t2) -> (A, t, t3, t4) g : (A, t, t3, t4) -> (A, t, t6, t7) f;g : (A, t1, t2) -> (A, t, t6, t7) (shorten) f;g : (t1, t2) -> (t, t6, t7) (but I mistakenly wrote) f;g : (t, t1, t2) -> (t, t6, t7) --- I will learn more about polycategory and polymorphic, and try to use them to explain dependent type system. thank you again :) ------ xieyuheng On Tuesday, June 19, 2018 at 2:58:05 AM UTC+8, Matt Oliveri wrote: > > Hi, Xieyuheng. > > On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng wrote: >> >> is there a categorical construction to generalize arrow composition, >> by allowing domain and codomain to be refined (or changed) by the >> composition ? >> >> this construction would be useful for >> forming theoretical background of dependent type system. >> >> for example, compose two functions >> f : (A x -> B y) >> g : (B n -> C z) >> will give us a function of type (A n -> C z) >> > > I can't figure out what rule you're using to get that type. If n unifies > with y, how did x become n also? That's what I'm guessing you're trying. > > >> another example would be the following generalized composition in >> cartesian closed category : >> f : (t1, t2) -> (t3, t4) >> g : (t, t3, t4) -> (t6, t7) >> f;g : (t, t1, t2) -> (t6, t7) >> and >> f : (t1, t2) -> (t, t3, t4) >> g : (t3, t4) -> (t6, t7) >> f;g : (t, t1, t2) -> (t, t6, t7) >> this can be called `cut` >> because it looks like gentzen's cut rule in sequent calculus, >> and it can be used to provide semantic >> for a stack based concatenative programming language. >> > > This looks more like a combination of composition and tensoring, in a > monoidal category. Based on some stuff in a blog post ( > https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivaria.html), > the cut rule is instead composition in a polycategory, and you can only cut > out one type at a time. > > I'm thinking the first "generalized composition" could be explained thus: > f only looks at the top two stack elements, and replaces them with three > others. But the stack generally has additional elements, which I'll > abstract away as Γ: > f : (Γ, t1, t2) -> (Γ, t3, t4) > > g has a similar story, but we use a different stack/context variable to > avoid accidental constraints: > g : (Δ, t, t3, t4) -> (Δ, t6, t7) > > To compose these, we need (Γ, t3, t4) to unify with (Δ, t, t3, t4), so (Γ > := Δ, t), and > f;g : (Δ, t, t1, t2) -> (Δ, t6, t7) > which we shorten to (t, t1, t2) -> (t6, t7). > > So your composable operators seem to be substitutions (morphisms between > contexts) that are polymorphic in most of the context. All but a finite > chunk all the way on the right. Composition would presumably be composition > of substitutions, after instantiating them with the principal unifier. > > For simply-typed systems, contexts and substitutions can be modeled in a > monoidal category, which includes cartesian closed categories. For > dependent type systems, other kinds of categories are used, like contextual > categories and categories with families; hopefully what you want is still > instantiation and composition of this new kind of substitution. > > I'm not an expert on the kinds of categorical structures involved, but > hopefully polymorphic substitutions is a good way of thinking about what > you're doing, which connects it with categorical models. > > Beware that with dependent types, there generally are not principal > unifiers, due to binding operators appearing in types. But concatenative > people don't seem to like binders, so maybe you dodged the bullet. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 5714 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 4148 bytes --] you also mention that, (roughly) > binding operators appearing in types hurts principal unifiers. > concatenative people don't seem to like binders. I think you mean forth like language do not use loacl variables, but I do introduced local variables in my language :P I will try to fight "the bullet" a little. I am really happy to finally found the direction about how to provide categorical semantics for my language :) ------ xieyuheng On Tuesday, June 19, 2018 at 2:58:05 AM UTC+8, Matt Oliveri wrote: > > Hi, Xieyuheng. > > On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng wrote: >> >> is there a categorical construction to generalize arrow composition, >> by allowing domain and codomain to be refined (or changed) by the >> composition ? >> >> this construction would be useful for >> forming theoretical background of dependent type system. >> >> for example, compose two functions >> f : (A x -> B y) >> g : (B n -> C z) >> will give us a function of type (A n -> C z) >> > > I can't figure out what rule you're using to get that type. If n unifies > with y, how did x become n also? That's what I'm guessing you're trying. > > >> another example would be the following generalized composition in >> cartesian closed category : >> f : (t1, t2) -> (t3, t4) >> g : (t, t3, t4) -> (t6, t7) >> f;g : (t, t1, t2) -> (t6, t7) >> and >> f : (t1, t2) -> (t, t3, t4) >> g : (t3, t4) -> (t6, t7) >> f;g : (t, t1, t2) -> (t, t6, t7) >> this can be called `cut` >> because it looks like gentzen's cut rule in sequent calculus, >> and it can be used to provide semantic >> for a stack based concatenative programming language. >> > > This looks more like a combination of composition and tensoring, in a > monoidal category. Based on some stuff in a blog post ( > https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivaria.html), > the cut rule is instead composition in a polycategory, and you can only cut > out one type at a time. > > I'm thinking the first "generalized composition" could be explained thus: > f only looks at the top two stack elements, and replaces them with three > others. But the stack generally has additional elements, which I'll > abstract away as Γ: > f : (Γ, t1, t2) -> (Γ, t3, t4) > > g has a similar story, but we use a different stack/context variable to > avoid accidental constraints: > g : (Δ, t, t3, t4) -> (Δ, t6, t7) > > To compose these, we need (Γ, t3, t4) to unify with (Δ, t, t3, t4), so (Γ > := Δ, t), and > f;g : (Δ, t, t1, t2) -> (Δ, t6, t7) > which we shorten to (t, t1, t2) -> (t6, t7). > > So your composable operators seem to be substitutions (morphisms between > contexts) that are polymorphic in most of the context. All but a finite > chunk all the way on the right. Composition would presumably be composition > of substitutions, after instantiating them with the principal unifier. > > For simply-typed systems, contexts and substitutions can be modeled in a > monoidal category, which includes cartesian closed categories. For > dependent type systems, other kinds of categories are used, like contextual > categories and categories with families; hopefully what you want is still > instantiation and composition of this new kind of substitution. > > I'm not an expert on the kinds of categorical structures involved, but > hopefully polymorphic substitutions is a good way of thinking about what > you're doing, which connects it with categorical models. > > Beware that with dependent types, there generally are not principal > unifiers, due to binding operators appearing in types. But concatenative > people don't seem to like binders, so maybe you dodged the bullet. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 5518 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 1669 bytes --] On Tuesday, June 19, 2018 at 4:07:34 AM UTC-4, xieyuheng wrote: > > I will learn more about polycategory and polymorphic, > and try to use them to explain dependent type system. > > thank you again :) > So polycategories had to do with the cut rule, which is not what your examples are doing. I don't think you need to worry about polycategories. I don't think there's much connection between polycategories and polymorphism, other than the prefix "poly". The kind of polymorphism I used on your example is "row polymorphism". This was already used for typing the "Cat" concatenative language. (So I was guessing you already knew about it, otherwise I would've said so earlier.) Thinking of the underlying monomorphic (non-polymorphic) stack types as contexts, I figure the approach should generalize to dependent contexts, with the operations being polymorphic substitutions between dependent contexts. So I think the ingredients you want are some dependent generalization of row polymorphism, and some categorical approach to interpreting the underlying monomorphic contexts and substitutions, like contextual categories. There are a lot of approaches to categorical interpretations of dependent types, and I don't know very much about it. This overview page knows more than I do: https://ncatlab.org/nlab/show/categorical+model+of+dependent+types -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2084 bytes --]
[-- Attachment #1.1: Type: text/plain, Size: 2238 bytes --] Oh! I mistakenly thought a polymorphism is a morphism in a polycategory, only later realized that polymorphism is the term from programming language. if polycategory is unrelated, I can try to develop a generalized theory based on my simple idea above. I read through the page << Categorical models of dependent types >> on nLab. it seems unsorted. and the categorical model for dependent type system is a unsolved problem. ------ xieyuheng On Wednesday, June 20, 2018 at 2:59:38 AM UTC+8, Matt Oliveri wrote: > > On Tuesday, June 19, 2018 at 4:07:34 AM UTC-4, xieyuheng wrote: >> >> I will learn more about polycategory and polymorphic, >> and try to use them to explain dependent type system. >> >> thank you again :) >> > > So polycategories had to do with the cut rule, which is not what your > examples are doing. I don't think you need to worry about polycategories. I > don't think there's much connection between polycategories and > polymorphism, other than the prefix "poly". > > The kind of polymorphism I used on your example is "row polymorphism". > This was already used for typing the "Cat" concatenative language. (So I > was guessing you already knew about it, otherwise I would've said so > earlier.) Thinking of the underlying monomorphic (non-polymorphic) stack > types as contexts, I figure the approach should generalize to dependent > contexts, with the operations being polymorphic substitutions between > dependent contexts. > > So I think the ingredients you want are some dependent generalization of > row polymorphism, and some categorical approach to interpreting the > underlying monomorphic contexts and substitutions, like contextual > categories. > > There are a lot of approaches to categorical interpretations of dependent > types, and I don't know very much about it. This overview page knows more > than I do: > https://ncatlab.org/nlab/show/categorical+model+of+dependent+types > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3385 bytes --]
I just wrote something on this tpoic :: https://xieyuheng.github.io/output/dependent-category.html (if you use github) welcome to leave message by open new issue on the repo :: https://github.com/xieyuheng/xieyuheng.github.io/issues ------ xieyuheng 2018-06-20 14:02 GMT+08:00, xieyuheng <xyheme@gmail.com>: > Oh! I mistakenly thought a polymorphism is a morphism in a polycategory, > only later realized that polymorphism is the term from programming > language. > > if polycategory is unrelated, > I can try to develop a generalized theory based on my simple idea above. > > I read through the page << Categorical models of dependent types >> on > nLab. > it seems unsorted. > and the categorical model for dependent type system is a unsolved problem. > > ------ > xieyuheng > > > On Wednesday, June 20, 2018 at 2:59:38 AM UTC+8, Matt Oliveri wrote: >> >> On Tuesday, June 19, 2018 at 4:07:34 AM UTC-4, xieyuheng wrote: >>> >>> I will learn more about polycategory and polymorphic, >>> and try to use them to explain dependent type system. >>> >>> thank you again :) >>> >> >> So polycategories had to do with the cut rule, which is not what your >> examples are doing. I don't think you need to worry about polycategories. >> I >> don't think there's much connection between polycategories and >> polymorphism, other than the prefix "poly". >> >> The kind of polymorphism I used on your example is "row polymorphism". >> This was already used for typing the "Cat" concatenative language. (So I >> was guessing you already knew about it, otherwise I would've said so >> earlier.) Thinking of the underlying monomorphic (non-polymorphic) stack >> types as contexts, I figure the approach should generalize to dependent >> contexts, with the operations being polymorphic substitutions between >> dependent contexts. >> >> So I think the ingredients you want are some dependent generalization of >> row polymorphism, and some categorical approach to interpreting the >> underlying monomorphic contexts and substitutions, like contextual >> categories. >> >> There are a lot of approaches to categorical interpretations of dependent >> >> types, and I don't know very much about it. This overview page knows more >> >> than I do: >> https://ncatlab.org/nlab/show/categorical+model+of+dependent+types >> > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.