From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 16 Oct 2017 09:20:40 -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_1672_794410280.1508170841058" ------=_Part_1672_794410280.1508170841058 Content-Type: multipart/alternative; boundary="----=_Part_1673_243146537.1508170841059" ------=_Part_1673_243146537.1508170841059 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit I understand your argument as a good reason to consider intrinsic syntax as being more analogous to derivations than to preterms. But still, trying to consistently call all those things judgments and derivations, and having nothing syntactic called terms or types seems impractical. Like I said, one could have opinions about whether (the things I call) intrinsic terms are more like preterms or derivations, but my terminology recommendation is not dependent on that. The existing papers on intrinsic syntax always seem to call them terms, even when they point out that they're a lot like derivations. I realized my terminology proposal didn't include anything convenient for the metalanguage types of intrinsic syntax objects. Normally, "judgments" would be OK, since that's what they correspond to. But for now I want to distinguish them easily from the extrinsic judgments, which involve preterms. I'll call them "classes". They are strongly-typed versions of the things often called "syntactic classes" or "syntactic categories" in CS. (Of course, calling them "categories" here would be super confusing.) So now let's try out your opening sentence in my terminology: [I would rather characterize intrinsic style by saying there are no *preterms*: all you have are classes and terms.] That's not so bad, is it? I feel like what makes you want to reject the term "term" is that you want to emphasize that *preterms* are not involved at all. Anyway, now I think I know what you meant before, about interpreting derivations. But I think it wasn't clear, because it sounded like you were talking about the usual extrinsic derivations. On Monday, October 16, 2017 at 11:06:11 AM UTC-4, Michael Shulman wrote: > > I would rather characterize intrinsic style by saying there are no > *terms*: all you have are judgments and derivations. Look at an > inductive-inductive encoding: its meta-language types are the > object-language judgments, and its meta-language terms are the > object-language derivations. Some of the judgment forms may be put > together out of a context (another judgment) and a type in that > context (a third judgment), but not all of them (e.g. not the judgment > for "is a context"); and you can also call a derivation a "term", but > that could be misleading. In particular, this perspective makes it > more clear that there is a bidirectional version of intrinsic style: > the two "directions" become simply two different judgment forms, and > the derivations are inductively generated by the bidirectional > "typing" rules. > > On Mon, Oct 16, 2017 at 6:45 AM, Matt Oliveri > wrote: > > 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 < > shu...@sandiego.edu> > >> >> 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_1673_243146537.1508170841059 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
I understand your argument as a good reason to consider in= trinsic syntax as being more analogous to derivations than to preterms. But= still, trying to consistently call all those things judgments and derivati= ons, and having nothing syntactic called terms or types seems impractical. = Like I said, one could have opinions about whether (the things I call) intr= insic terms are more like preterms or derivations, but my terminology recom= mendation is not dependent on that. The existing papers on intrinsic syntax= always seem to call them terms, even when they point out that they're = a lot like derivations.

I realized my terminology proposal didn'= t include anything convenient for the metalanguage types of intrinsic synta= x objects. Normally, "judgments" would be OK, since that's wh= at they correspond to. But for now I want to distinguish them easily from t= he extrinsic judgments, which involve preterms. I'll call them "cl= asses". They are strongly-typed versions of the things often called &q= uot;syntactic classes" or "syntactic categories" in CS. (Of = course, calling them "categories" here would be super confusing.)=

So now let's try out your opening sentence in my terminology:[I would rather characterize intrinsic style by saying there are no *pret= erms*: all you have are classes and terms.]
That's not so bad, is it= ? I feel like what makes you want to reject the term "term" is th= at you want to emphasize that *preterms* are not involved at all.

An= yway, now I think I know what you meant before, about interpreting derivati= ons. But I think it wasn't clear, because it sounded like you were talk= ing about the usual extrinsic derivations.

On Monday, October 16, 20= 17 at 11:06:11 AM UTC-4, Michael Shulman wrote:
I would rather characterize intrinsic style by saying ther= e are no
*terms*: all you have are judgments and derivations. =C2=A0Look at an
inductive-inductive encoding: its meta-language types are the
object-language judgments, and its meta-language terms are the
object-language derivations. =C2=A0Some of the judgment forms may be pu= t
together out of a context (another judgment) and a type in that
context (a third judgment), but not all of them (e.g. not the judgment
for "is a context"); and you can also call a derivation a &qu= ot;term", but
that could be misleading. =C2=A0In particular, this perspective makes i= t
more clear that there is a bidirectional version of intrinsic style:
the two "directions" become simply two different judgment for= ms, and
the derivations are inductively generated by the bidirectional
"typing" rules.

On Mon, Oct 16, 2017 at 6:45 AM, Matt Oliveri <atm...@gmail.com> w= rote:
> On Monday, October 16, 2017 at 1:10:20 AM UTC-4, Michael Shulman w= rote:
>>
>> What you call "intrinsically typed syntax" is what I= favor. =C2=A0I want
>> initiality theorems that are proven by a straightforward struc= tural
>> induction over something that is inductively generated, and
>> derivations are the basic inductively generated object of a de= ductive
>> system.
>
>
> I want to set up some terminology, which we should try to use cons= istently
> for this thread. (I mean Mike and me, but others could follow alon= g too. It
> might be helpful.)
>
> In the extrinsic style of syntax, which is the usual one, there ar= e
> "preterms" and "derivations". To notate types,= there are either separate
> "pretypes", or else pretypes are a subset of the preterm= s. The thing to the
> left of the turnstile is a "precontext".
>
> In the intrinsic style of syntax, there are contexts, types, and t= erms. (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 sem= antics.) There
> may also be other things defined mutually.
>
> In the intrinsic style, there are no derivations. One could have o= pinions on
> whether intrinsic terms are more like preterms or typing derivatio= ns, but
> they aren't actually either of those.
>
> Techniques like bidirectional type checking don't seem to appl= y to intrinsic
> syntax. You don't type check intrinsic syntax; it's intrin= sically
> well-typed. I'm not sure there's even any analogue of bidi= rectional
> judgments for intrinsic syntax. Maybe you know one. I bring this u= p because
> you were talking about interpreting derivations of bidirectional t= yping.
> That sounds interesting, but it's totally not interpreting int= rinsic syntax.
>
> So you're saying you like intrinsic syntax, and how it lets yo= u interpret
> with one structural induction. That makes sense. But that's no= t interpreting
> derivations. If you interpret derivations, then you also have pret= erms 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 departi= ng 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...@gm= ail.com> wrote:
>> > In order to assign meanings to derivations, one would hav= e 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, inte= rpreting
>> > derivations is the most flexible. Gabirel Scherer brought= up functor
>> > semantics of refinement type systems, which seems to be s= tudying the
>> > general
>> > situation, with a category of derivation meanings and a c= ategory 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 pla= ce. 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 deriv= ations. 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 eleg= ant to stick to
>> > systems where the meaning can be assigned to derivable te= rms. 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 be= tween proving 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 math= ematically, just to
>> >> > *think* about "using a partial interpretati= on function on
>> >> > prejudgments
>> >> > and showing that all derivable judgments get a m= eaning" as *being a
>> >> > way of* "assigning meanings to derivations = and showing that distinct
>> >> > derivations of the same judgment get the same me= aning".
>> >> >
>> >> > On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streiche= r
>> >> > <stre...@mathematik.tu-darmstadt.de> wrote:
>> >> >>> > When writing my thesis in the secon= d half of the 80s I found this
>> >> >>> > too
>> >> >>> > difficult and instead used an a pri= ori partial interpretation
>> >> >>> > function assigning meaning to preju= dgements. It was then part of
>> >> >>> > the
>> >> >>> > correctness theorem that all deriva= ble 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. F= irst of all you have to
>> >> >> formalize derivations and do a double induct= ion on them which I
>> >> >> don't
>> >> >> know how to to perform.
>> >> >>
>> >> >> Thomas
------=_Part_1673_243146537.1508170841059-- ------=_Part_1672_794410280.1508170841058--