From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDGPPLV76EPRB57ZULMQKGQEKU345YA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-ot0-x23a.google.com (mail-ot0-x23a.google.com [IPv6:2607:f8b0:4003:c0f::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b0e28ba5 for ; Tue, 19 Jun 2018 08:21:12 +0000 (UTC) Received: by mail-ot0-x23a.google.com with SMTP id a9-v6sf11459267otl.21 for ; Tue, 19 Jun 2018 01:21:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=DXpMT4TZAvP3djoJltPtGWWdAqJ95FpY868inxXsxew=; b=sRoAGGTS536v/ullxZ6sszPapjpewNoInWE2LPxsJCbESd52Tyc+AyCjOzsVM/9uJI uQFDnFCZEK0x1eU+7F5NzwYU+hXAECUzm4U4tNEx0klp7VqfdbR///XSfrZnPuSkvJ0X /SRCaCL1BnS7gxSweC7yuu83d0GYfsDwrEUPyApwqytcYPIIKkICLzq9YX8ADcuUOYa6 DE7qU97J/pN45dWSnFzXFFo9y3GZSSVepwf+O6JqbIrVBA2tLiRUxsOlxFrj4upFHvue lq5shT6vVC4Yg0yZmvn4GDIbZNxNvsnkcqPuqnZtuIeZvTHe/qkEWONsKaCl7bK38p5B gtHA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=DXpMT4TZAvP3djoJltPtGWWdAqJ95FpY868inxXsxew=; b=B0k0NxzXo8pI2aHddzpgWggz/di5Tl9cqq/FXOdnmGgImtTZtMjoIrsBPEfqlmSmnV O8Rs6T63gUbkiAWrLtAIXIQJ9GzEd1nNqmnQMQScfW/CIQhh6r3twgkDqKbvkGZ6mJZR L+YDjRmfcevA0yG32PhbS+dWmg6uiIsfeOKda30xeradLmKtQMjiED/DpQ6UmadqlKq+ xbCFC6BbIFq9w6jhwXcTx4SbX/KA3SPDZNTC02lyXJp9gnyWsTNFKlxUDNqsRz1FsInf /Ct5vMSDTjGkdBoYGFR6hK3izeLp8tXmuwUxoOFheM0LMDZmNtIm206xXYcVnK2HhOLz 1XGQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=DXpMT4TZAvP3djoJltPtGWWdAqJ95FpY868inxXsxew=; b=m73VOWBS+8jU/YaTxZX5FBCr1S8MZe0S0xVqPGnpgT0ns7YMY9e9iJm5kWOoYPD31f 9fLyzkRQ4W9XqA9hWz0b5zOxOsPqVdG6nZ3+JryvUfHSLPZgJgeaMxRpisxRNW6bJiBn AKPdLSwtCPBogC4yB+5SdmNDaiV8l9rPmLnO74zdKqPvL8+nYQCtgN+XVbFHZSdfBrcU 8gRq1u3HWZhRuEsm2EWOaZr1H5ZY7xCQM7stmfwvniC29VsZrICUitc2vdSpTOf+IzW2 Eg+kI52WEIlxILeuzf3U0AWKXieeV6UmskRypA/ccwKoS5pWl6J8J1qWXVzKOOpdl4DP PNYg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E1fdeuxX+USWYL1E7inQmrbvpGf356TxgfDEqZrfImvyDSfdHiI DJePnQnU97PDFbQxdkP6VYs= X-Google-Smtp-Source: ADUXVKJDHxAptkSDU0KRZT2EzsBHbSz+0QVJJTbaCT3eyp5jBLL+dtzdfm0W46JLaBP2oZcFLnnTIg== X-Received: by 2002:a9d:6218:: with SMTP id g24-v6mr688006otj.4.1529396471602; Tue, 19 Jun 2018 01:21:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5188:: with SMTP id y8-v6ls7067070otg.9.gmail; Tue, 19 Jun 2018 01:21:11 -0700 (PDT) X-Received: by 2002:a9d:4c96:: with SMTP id m22-v6mr676193otf.6.1529396470918; Tue, 19 Jun 2018 01:21:10 -0700 (PDT) Date: Tue, 19 Jun 2018 01:21:10 -0700 (PDT) From: xieyuheng To: Homotopy Type Theory Message-Id: <658855a4-084b-4cc3-a4b8-983d378106ce@googlegroups.com> In-Reply-To: <5edbc6da-6e18-45af-8ac0-e498f122a4ec@googlegroups.com> References: <5edbc6da-6e18-45af-8ac0-e498f122a4ec@googlegroups.com> Subject: [HoTT] Re: is there a categorical construction to generalize arrow composition, by allowing domain and codomain to be refined (or changed) by the composition ? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_18514_1310008926.1529396470414" X-Original-Sender: xyheme@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_18514_1310008926.1529396470414 Content-Type: multipart/alternative; boundary="----=_Part_18515_1552523577.1529396470415" ------=_Part_18515_1552523577.1529396470415 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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= =20 > 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=20 >> 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=20 > monoidal category. Based on some stuff in a blog post ( > https://golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multivar= ia.html),=20 > the cut rule is instead composition in a polycategory, and you can only c= ut=20 > 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= =20 > others. But the stack generally has additional elements, which I'll=20 > abstract away as =CE=93: > f : (=CE=93, t1, t2) -> (=CE=93, t3, t4) > > g has a similar story, but we use a different stack/context variable to= =20 > avoid accidental constraints: > g : (=CE=94, t, t3, t4) -> (=CE=94, t6, t7) > > To compose these, we need (=CE=93, t3, t4) to unify with (=CE=94, t, t3, = t4), so (=CE=93=20 > :=3D =CE=94, t), and > f;g : (=CE=94, t, t1, t2) -> (=CE=94, t6, t7) > which we shorten to (t, t1, t2) -> (t6, t7). > > So your composable operators seem to be substitutions (morphisms between= =20 > contexts) that are polymorphic in most of the context. All but a finite= =20 > chunk all the way on the right. Composition would presumably be compositi= on=20 > of substitutions, after instantiating them with the principal unifier. > > For simply-typed systems, contexts and substitutions can be modeled in a= =20 > monoidal category, which includes cartesian closed categories. For=20 > dependent type systems, other kinds of categories are used, like contextu= al=20 > categories and categories with families; hopefully what you want is still= =20 > instantiation and composition of this new kind of substitution. > > I'm not an expert on the kinds of categorical structures involved, but=20 > hopefully polymorphic substitutions is a good way of thinking about what= =20 > you're doing, which connects it with categorical models. > > Beware that with dependent types, there generally are not principal=20 > unifiers, due to binding operators appearing in types. But concatenative= =20 > people don't seem to like binders, so maybe you dodged the bullet. > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_18515_1552523577.1529396470415 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
you also mention that,
(roughly)
> binding operat= ors appearing in types hurts principal unifiers.
> concatenative peop= le 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 la= nguage :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 :)

------
xie= yuheng


On Tuesday, June 19, 2018 at 2:58:05 AM UTC+8, Matt Olive= ri wrote:
Hi, = Xieyuheng.

On Monday, June 18, 2018 at 12:32:14 PM UTC-4, xieyuheng = wrote:
is there a c= ategorical construction to generalize arrow composition,
by allowing dom= ain 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 w= ould be the following generalized composition in cartesian closed category = :
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 f=C2=A0=C2=A0 : (t1, t2) -&= gt; (t3, t4)
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 g=C2=A0=C2=A0 : = (t, t3, t4) -> (t6, t7)
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 f;= g : (t, t1, t2) -> (t6, t7)
and
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0 f=C2=A0=C2=A0 : (t1, t2) -> (t, t3, t4)
=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0 g=C2=A0=C2=A0 : (t3, t4) -> (t6, t7)
=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 f;g : (t, t1, t2) -> (t, t6, t7)this can be called `cut`
because it looks like gentzen's cut rule i= n sequent calculus,
and it can be used to provide semantic
for a stac= k based concatenative programming language.

= This looks more like a combination of composition and tensoring, in a monoi= dal category. Based on some stuff in a blog post (https:= //golem.ph.utexas.edu/category/2017/11/the_polycategory_of_multiv= aria.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 f= irst "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 aw= ay as =CE=93:
f=C2=A0 :=C2=A0 (=CE=93, t1, t2) -> (=CE=93, t3, t4)
g has a similar story, but we use a different stack/context variable t= o avoid accidental constraints:
g=C2=A0 :=C2=A0 (=CE=94, t, t3, t4) ->= ; (=CE=94, t6, t7)

To compose these, we need (=CE=93, t3, t4) to uni= fy with (=CE=94, t, t3, t4), so (=CE=93 :=3D =CE=94, t), and
f;g=C2=A0 := =C2=A0 (=CE=94, t, t1, t2) -> (=CE=94, t6, t7)
which we shorten to (t= , t1, t2) -> (t6, t7).

So your composable operators seem to be su= bstitutions (morphisms between contexts) that are polymorphic in most of th= e context. All but a finite chunk all the way on the right. Composition wou= ld presumably be composition of substitutions, after instantiating them wit= h the principal unifier.

For simply-typed systems, contexts and subs= titutions can be modeled in a monoidal category, which includes cartesian c= losed categories. For dependent type systems, other kinds of categories are= used, like contextual categories and categories with families; hopefully w= hat you want is still instantiation and composition of this new kind of sub= stitution.

I'm not an expert on the kinds of categorical structu= res involved, but hopefully polymorphic substitutions is a good way of thin= king about what you're doing, which connects it with categorical models= .

Beware that with dependent types, there generally are not principa= l unifiers, due to binding operators appearing in types. But concatenative = people don't seem to like binders, so maybe you dodged the bullet.
<= /div>

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_18515_1552523577.1529396470415-- ------=_Part_18514_1310008926.1529396470414--