[HoTT] is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[HoTT] is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[xieyuheng]

[-- 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 --]

[HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[Matt Oliveri]

[-- 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 --]

[HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[xieyuheng]

[-- 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 --]

[HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[xieyuheng]

[-- 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 --]

[HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[Matt Oliveri]

[-- 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 --]

[HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[xieyuheng]

[-- 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 --]

Re: [HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[xieyuheng]

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.

[HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ?

[xieyuheng]

[-- 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 --]