From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 16 Oct 2017 06:45:44 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> <20171015074530.GA29437@mathematik.tu-darmstadt.de> <20171015135740.GA7845@mathematik.tu-darmstadt.de> <37664950-3045-4570-af39-5f44bfc13a1b@googlegroups.com> Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_24592_611497920.1508161544764" ------=_Part_24592_611497920.1508161544764 Content-Type: multipart/alternative; boundary="----=_Part_24593_1462759714.1508161544764" ------=_Part_24593_1462759714.1508161544764 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On Monday, October 16, 2017 at 1:10:20 AM UTC-4, Michael Shulman wrote: > > What you call "intrinsically typed syntax" is what I favor. I want > initiality theorems that are proven by a straightforward structural > induction over something that is inductively generated, and > derivations are the basic inductively generated object of a deductive > system. I want to set up some terminology, which we should try to use consistently for this thread. (I mean Mike and me, but others could follow along too. It might be helpful.) In the extrinsic style of syntax, which is the usual one, there are "preterms" and "derivations". To notate types, there are either separate "pretypes", or else pretypes are a subset of the preterms. The thing to the left of the turnstile is a "precontext". In the intrinsic style of syntax, there are contexts, types, and terms. (In principle, you should be able to make types a subset of terms, but I haven't seen that, and it doesn't seem appropriate for categorical semantics.) There may also be other things defined mutually. In the intrinsic style, there are no derivations. One could have opinions on whether intrinsic terms are more like preterms or typing derivations, but they aren't actually either of those. Techniques like bidirectional type checking don't seem to apply to intrinsic syntax. You don't type check intrinsic syntax; it's intrinsically well-typed. I'm not sure there's even any analogue of bidirectional judgments for intrinsic syntax. Maybe you know one. I bring this up because you were talking about interpreting derivations of bidirectional typing. That sounds interesting, but it's totally not interpreting intrinsic syntax. So you're saying you like intrinsic syntax, and how it lets you interpret with one structural induction. That makes sense. But that's not interpreting derivations. If you interpret derivations, then you also have preterms to worry about, since they are what appear in judgments. It seems most natural to me to introduce terms as a > convenient 1-dimensional notation for derivations, and departing from > that is what causes all the problems. > What's a 1-dimensional notation? > On Sun, Oct 15, 2017 at 2:00 PM, Matt Oliveri > wrote: > > In order to assign meanings to derivations, one would have to define > > derivations. Technically, to assign meanings to derivable terms, one > would > > only need to define derivability. All information needed to pick the > right > > meaning would then need to be included in the terms. This might explain > the > > disagreement over whether unique typing is necessary. In the middle, you > > could assign meanings to derivable judgments... > > > > Given the usual raw-terms-then-derivations approach, interpreting > > derivations is the most flexible. Gabirel Scherer brought up functor > > semantics of refinement type systems, which seems to be studying the > general > > situation, with a category of derivation meanings and a category of term > > meanings, and a functor from the former to the latter. > > > > With intrinsically typed syntax--what Thorsten is talking about--there > is no > > separation between terms and derivations in the first place. This is a > style > > of syntax for type systems where--as a design constraint--all "relevant" > > information is included in the terms. > > > > Mike, I'm surprised that you favor interpreting derivations. For a > > categorical semantics, there is only one "level" of meaning. (Not two, > like > > with a functor.) So I figured you would find it more elegant to stick to > > systems where the meaning can be assigned to derivable terms. Even when > this > > sort of system is not directly amenable to implementation, it provides > an > > interface to separate syntactic and semantic concerns. > > > > On Sunday, October 15, 2017 at 12:00:36 PM UTC-4, Michael Shulman wrote: > >> > >> I mean, it seems to me kind of like the difference between proving a > >> type A is contractible by > >> > >> Sigma(a:A) Pi(x:A) (x=a) > >> > >> and by > >> > >> A x Pi(x y:A) (x=y) > >> > >> i.e. not much. But maybe I am missing something? > >> > >> On Sun, Oct 15, 2017 at 7:53 AM, Michael Shulman > >> wrote: > >> > I'm not saying to do anything different mathematically, just to > >> > *think* about "using a partial interpretation function on > prejudgments > >> > and showing that all derivable judgments get a meaning" as *being a > >> > way of* "assigning meanings to derivations and showing that distinct > >> > derivations of the same judgment get the same meaning". > >> > > >> > On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streicher > >> > wrote: > >> >>> > When writing my thesis in the second half of the 80s I found this > >> >>> > too > >> >>> > difficult and instead used an a priori partial interpretation > >> >>> > function assigning meaning to prejudgements. It was then part of > the > >> >>> > correctness theorem that all derivable judgements get assigned a > >> >>> > meaning. > >> >>> > >> >>> Couldn't one consider the latter to be a way of doing the former? > >> >> > >> >> In principle yes but it is very laborious. First of all you have to > >> >> formalize derivations and do a double induction on them which I > don't > >> >> know how to to perform. > >> >> > >> >> Thomas > ------=_Part_24593_1462759714.1508161544764 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Monday, October 16, 2017 at 1:10:20 AM UTC-4, Michael S= hulman wrote:
What you call &qu= ot;intrinsically typed syntax" is what I favor. =C2=A0I want
initiality theorems that are proven by a straightforward structural
induction over something that is inductively generated, and
derivations are the basic inductively generated object of a deductive
system.

I want to set up some terminology, which w= e should try to use consistently for this thread. (I mean Mike and me, but = others could follow along too. It might be helpful.)

In the extrinsi= c style of syntax, which is the usual one, there are "preterms" a= nd "derivations". To notate types, there are either separate &quo= t;pretypes", or else pretypes are a subset of the preterms. The thing = to the left of the turnstile is a "precontext".

In the int= rinsic style of syntax, there are contexts, types, and terms. (In principle= , you should be able to make types a subset of terms, but I haven't see= n that, and it doesn't seem appropriate for categorical semantics.) The= re may also be other things defined mutually.

In the intrinsic style= , there are no derivations. One could have opinions on whether intrinsic te= rms are more like preterms or typing derivations, but they aren't actua= lly either of those.

Techniques like bidirectional type checking don= 't seem to apply to intrinsic syntax. You don't type check intrinsi= c syntax; it's intrinsically well-typed. I'm not sure there's e= ven any analogue of bidirectional judgments for intrinsic syntax. Maybe you= know one. I bring this up because you were talking about interpreting deri= vations of bidirectional typing. That sounds interesting, but it's tota= lly not interpreting intrinsic syntax.

So you're saying you like= intrinsic syntax, and how it lets you interpret with one structural induct= ion. That makes sense. But that's not interpreting derivations. If you = interpret derivations, then you also have preterms to worry about, since th= ey are what appear in judgments.

It seems most natural to me to introduce terms as a
convenient 1-dimensional notation for derivations, and departing from
that is what causes all the problems.

What'= ;s a 1-dimensional notation?


On Sun, Oct 15, 2017 at 2:00 PM, Matt Oliveri <atm...@gmail.com> w= rote:
> In order to assign meanings to derivations, one would have to defi= ne
> derivations. Technically, to assign meanings to derivable terms, o= ne would
> only need to define derivability. All information needed to pick t= he right
> meaning would then need to be included in the terms. This might ex= plain the
> disagreement over whether unique typing is necessary. In the middl= e, you
> could assign meanings to derivable judgments...
>
> Given the usual raw-terms-then-derivations approach, interpreting
> derivations is the most flexible. Gabirel Scherer brought up funct= or
> semantics of refinement type systems, which seems to be studying t= he general
> situation, with a category of derivation meanings and a category o= f term
> meanings, and a functor from the former to the latter.
>
> With intrinsically typed syntax--what Thorsten is talking about--t= here is no
> separation between terms and derivations in the first place. This = is a style
> of syntax for type systems where--as a design constraint--all &quo= t;relevant"
> information is included in the terms.
>
> Mike, I'm surprised that you favor interpreting derivations. F= or a
> categorical semantics, there is only one "level" of mean= ing. (Not two, like
> with a functor.) So I figured you would find it more elegant to st= ick to
> systems where the meaning can be assigned to derivable terms. Even= when this
> sort of system is not directly amenable to implementation, it prov= ides an
> interface to separate syntactic and semantic concerns.
>
> On Sunday, October 15, 2017 at 12:00:36 PM UTC-4, Michael Shulman = wrote:
>>
>> I mean, it seems to me kind of like the difference between pro= ving a
>> type A is contractible by
>>
>> Sigma(a:A) Pi(x:A) (x=3Da)
>>
>> and by
>>
>> A x Pi(x y:A) (x=3Dy)
>>
>> i.e. not much. =C2=A0But maybe I am missing something?
>>
>> On Sun, Oct 15, 2017 at 7:53 AM, Michael Shulman <shu...= @sandiego.edu>
>> wrote:
>> > I'm not saying to do anything different mathematicall= y, just to
>> > *think* about "using a partial interpretation functi= on on prejudgments
>> > and showing that all derivable judgments get a meaning&qu= ot; as *being a
>> > way of* "assigning meanings to derivations and showi= ng that distinct
>> > derivations of the same judgment get the same meaning&quo= t;.
>> >
>> > On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streicher
>> > <stre...@mathematik.tu-darmstadt.de> wr= ote:
>> >>> > When writing my thesis in the second half of= the 80s I found this
>> >>> > too
>> >>> > difficult and instead used an a priori parti= al interpretation
>> >>> > function assigning meaning to prejudgements.= It was then part of the
>> >>> > correctness theorem that all derivable judge= ments get assigned a
>> >>> > meaning.
>> >>>
>> >>> Couldn't one consider the latter to be a way = of doing the former?
>> >>
>> >> In principle yes but it is very laborious. First of a= ll you have to
>> >> formalize derivations and do a double induction on th= em which I don't
>> >> know how to to perform.
>> >>
>> >> Thomas
------=_Part_24593_1462759714.1508161544764-- ------=_Part_24592_611497920.1508161544764--