Re: [HoTT] A small observation on cumulativity and the failure of initiality

[Matt Oliveri <atm...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 8695 bytes --]

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 <atm...@gmail.com 
> <javascript:>> 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 <atm...@gmail.com> 
> 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 
> >> >> > <str...@mathematik.tu-darmstadt.de> 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
>

[-- Attachment #1.2: Type: text/html, Size: 10684 bytes --]