added pointer to the thesis

- Martin Lundfall,
*Models of linear dependent type theory*, 2017 (pdf)

(which became the preprint Lundfall 18, arXiv:1806.09593 – both, apparently, unpublished)

]]>added these two pointer:

Matthijs Vákár,

*A Categorical Semantics for Linear Logical Frameworks*, In: A. Pitts (ed.),*Foundations of Software Science and Computation Structures*FoSSaCS 2015. Lecture Notes in Computer Science, vol 9034. Springer 2015 (arXiv:1501.05016, doi:10.1007/978-3-662-46678-0_7)Matthijs Vákár, Section 3 of:

*In Search of Effectful Dependent Types*(arXiv:1706.07997, uuid:e91e19b3-7e10-4fda-9433-f23b469e4049)

I seem to be seeing polynomial functors wherever I look these days.

]]>And one more:

- Mike Shulman,
*A type theory for fibred functors and polynomials*. Unfinished note, 2018. pdf

Added some references for other kinds of DLTT.

]]>Added arXiv number and comlete publication data to

- {#FKS20} Peng Fu, Kohei Kishida, Peter Selinger,
*Linear Dependent Type Theory for Quantum Programming Languages*, LICS ’20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)

added pointer to:

- Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger,
*A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper*, in I. Lanese, M. Rawski (eds.)*Reversible Computation*RC 2020. Lecture Notes in Computer Science, vol 12227 (arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9)

and added cross-links with the new entry *quantum programming language*

Added reference

]]>Yes, that sentence seems like it should probably be moved to the “Semantics” section.

]]>After the “great split” where much of this page was sent over to indexed monoidal (infinity,1)-category, the links in

What should be the categorical semantics of dependent linear type theory was discussed in (Shulman 08, Ponto-Shulman 12, Shulman 12, Schreiber 14)

no longer work.

A simple fix is possible, but without wishing to provoke the tensions which tend to arise in these parts from differences of opinion on the necessity for syntax when one speaks of a type theory, is the page due a make-over? Why was that quoted sentence in the section ’Syntax’ in any case?

Alternatively we wait for the roll out of the LSR program when all modal dependent type theories will be given their proper setting.

]]>I added this recent reference

- Martin Lundfall,
*A diagram model of linear dependent type theory*, (arXiv:1806.09593)

I wish I had time to read Vákár’s thesis carefully. It looks like he may be solving the problem in the non-homotopy case, specifying a syntax and a semantics and proving that they match up (p81):

The structure we obtain is that of a strict indexed symmetric monoidal category with comprehension

We also get a mention (p71):

Although in the last while some suggestions have been made on the nLab and nForum of possible connections between the syntactic and semantic work, no account of the correspondence was published.

(-:

]]>Thanks for the alert. I had not seen that yet.

]]>Matthijs Vákár’s thesis is out, so I’ve added that to his page. I don’t know whether its separate strands supersede individual publications, such as the one in #48.

]]>Have added two new references to *dependent linear type theory*:

Matthijs Vákár has new talk notes [2] expanding on his article [3] and Neelakantan Krishnaswami with Pierre Pradic and Nick Benton have an article in preparation [4].

[2] http://users.ox.ac.uk/~magd3996/research/10-11-2014-Oxford-Linear%20dependent%20types.pdf

[3] http://arxiv.org/abs/1405.0033

[4] http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf

]]>Have edited a bit more.

I’ll have to leave it the way it is for the moment, have to rush off now. I am going to use part of this as a script for a talk to the type theory group at Paris-Diderot today, around Paul-André Melliès. My goal is to

first convince the audience that six-functor Yoga in Wirthmüller style is precisely what ought to be regarded as the semantics for dependent linear (homotopy-)type theory (i.e. any proposed syntax ought to have that as its semantics),

then to indicate that in such contexts one may elegantly axiomatize “secondary integral transforms”,

point out that these capture/generalize the exponential modality construction,

highlight that it is manifestly a path-integral-like construction

and finally to indicate that in the model of parameterized modules this gives matrix calculus,

and to claim that in the model of parameterized spectra it gives pull-push in bivariant tiwsted generalized cohomology.

We’ll see how it works.

(I’ll duly highlight Mike’s many contributions to this. )

]]>Have edited a good bit more at *dependent linear type theory*. Will continue tomorrow.

The main new addition so far is maybe that I added the definition of *fundamental classes* and of *secondary integral transforms* in terms of dependent linear type theory. Added also the example which shows (or states at least) that for parameterized modules this reproduces matrix calculus.

Maybe I’ll further expand the included table *twisted generalized cohomology in linear homotopy type theory – table* now, but then I need to quit for today.

I am filling content into *dependent linear type theory*.

Now it says the entry is locked by an anonymous. This used to be a spurious message appearing all the time in the old days, and was a bug. Now I am not sure. If anyone reading here is really editing then: please wait – I am in the middle of editing.

]]>Okay, thanks. I really think it would be worthwhile, but I should say: don’t let me distract you too much from what I guess your advisor/coauthors would want you to do instead!

While we are at it, here is a trivial typo which I spotted:

p. 10 in “Judgements”, below “…of the following six forms”:

the second line needs “$\sigma$” to be replaced by $A$;

the third item needs a capitalization of the second “$a$”

Another comment: I gather your discussion of comprehension in the linear dependent context is an elaboration on the observation that I had made here (and on p. 48 of “Quantization via Linear homotopy types”), right? I think your readers might really appreciate it if you made it clearer what is going on here. Presently your article jumps right into some fairly non-obvious syntax on p. 6 and p. 21, and I think the reader who doesn’t already know what you are after here will find this somewhat mysterious and unmotivated. (I may be very wrong here, after all I am not a logician and I realize that logicians are a very different species ;-) In footnote 18 you start giving what I would consider an actual explanation of what’s going on with comprehension here. Maybe some such explanation could be moved right to a prominent position in the main text, to help the reader follow you? Just an idea.

]]>In the next version I will make the suggested changes and generally move things from footnotes and proofs into actual statements in the paper. Also, the example isn't formulated optimally, now. (Although I already have a new version ready.) It, in fact, always has a comprehension. The construction is really taking the free linear predicate type theory on Set given a propositional linear type theory. (or coFree as it is right adjoint to the forgetful functor of evaluating a linear predicate type theory on Set at 1) I didn't explain this properly yet in the current version. This also explains (partly) why the example is so discrete.

I'm not entirely sure yet, though, if I should go for the real internal language syntax... if I find time, I could add an appendix.

Really appreciate the feedback. Thanks! ]]>

Hi Matthijs,

thanks, again, for dropping by, also here!

I understand, and my only suggestion is that it would be useful — for readers, for “the community”, for purposes of references — to state the syntax/semantics equivalences that are clearly very clear to you personally also very clearly in text.

Currently you have, somewhat hidden inside the proof of your theorem 9, a throwaway remark that the relevant fragment of your syntax is indeed the internal language of strict indexed symmetric monoidal categories. I missed this statement on first reading, and it is easy to miss, being inside the proof of another statement which is only fragmentarily related.

A text on the syntax and semantics of dependent linear type theory I would ideally hope to have a tabulated list of the form:

the syntax for strict indexed symmetric monoidal categories is precisely A

the syntax for strict indexed closed symmetric monoidal categories is precisely A+B

the syntax for strict indexed symmetric monoidal categories with comprehension is precisely A+C

etc.

Think of it this way: I would like to exapnd the table on the page *relation between type theory and category theory* by including entries with fragments of “dependent linear type theory” on the left and on the right pointers to the literature.

In fact I’ll add a row to that table now, pointing to your article. But as it stands the reader may have a bit of trouble isolating the statement in your article (as I had, on first reading).

]]>Thank you for the pointer, Noam! Indeed, I completely missed the CLF paper. In general, I'm much more of a category theorist than a syntactician. Just having had a quick glance at the paper, both syntaxes do indeed look quite similar. Obviously, the CLF syntax has been designed with computation in mind, while what I wrote down was meant to be a bit more towards the pure maths side of things, hoping to find a correspondence with certain categories. In particular, it should be a fairly straightforward generalisation of (rather bare) dependent type theory so we can use it to obtain a game semantics for dependent types, by taking the natural interpretation in a category of games and strategies.

I haven't been able to have a sufficient look at CLF and am still a bit daunted by all the 'weird symbols'. It is very nice to see, however, that a similar system has been developed that has a good syntactic metatheory. I'd be very interested to see as well if we can find a correspondence with some variant of my categorical semantics.

Urs, regarding the syntax-semantics correspondence here: I think I have a pretty good idea of most of it. Perhaps things would be clearer to you if we have syntax in which the categorical aspect of comprehension is also modular? (I think all other things are modular in my syntax/semantics, basically.) I'd be happy to write down this syntax for you if that would clarify things. What you do is you just take an intuitionistic (non-dependent) type theory and a linear type theory in each intuitionistic context with substitution operations by intuitionistic terms that go from one linear type theory to the other. (Basically, this is a strict indexed symmetric multicategory.) Than you can add rules that allow you to glue linear types to intuitionistic contexts and linear terms to intuitionistic context morphisms. (This is your comprehension.) You get a conservative extension of my syntax that now also talks explicitly about intuitionistic terms. This is a real internal language for strict indexed symmetric multicategries (without/with comprehension). If you add tensor and I types to your syntax, you get the case of strict indexed symmetric monoidal categories.

Thanks, Bas and Urs, for the pointer to Spiwak's paper. I also didn't know that one. Haven't properly looked at it, but, it seems it considers one particular quite rich system very thoroughly from the syntactic point of view. I'm hoping this'll answer some of my questions about the computational properties of the syntax. :-) On the other hand, it looks specifically classical (rather than intuitionistic) and therefore not so close to the categories we're interested in, but I may be wrong.

I'm trying to finish some notes on the model in terms of coherence spaces, now. Hopefully, that should provide some intuition for people who are familiar with coherence spaces or domain theory. At least, I think it's quite an intuitive model, myself, that is reasonably faithful to capturing the essence of the syntax. Certainly much better than the 'free models' I briefly discussed in the paper. After I finish these notes, I'll return to the syntax. :-)

Matthijs ]]>

Bas Spitters kindly points out that a dependent linear version of system L had once been considered in

- Arnaud Spiwak, section 5 of
*A dissection of L*, Logical Methods in Computer Science 1998 pdf

Have now added a pointer (just a pointer) to that to the entry, too.

]]>I see, thanks.

Looks like somebody like RAG Seely is needed once more to come and sort out the syntax-semtantics relation cleanly.

]]>I suspect that a semantics of CLF in indexed closed monoidal categories would be sound but not complete. One of the key ideas of CLF was to maintain a syntactic separation between negative (or “asynchronous”) and positive (or “synchronous”) types, with the positive fragment “encapsulated in a monad” as the abstract of that tech report says (it might be better to say that the two categories of types are related by an adjunction; note that this is a bit different from the idea of a “linear-non-linear adjunction”, since here both categories of types are linear). Formally, this separation is used in order to derive a very simple equational theory: terms are only quotiented by $\alpha$-equivalence, together with a simple notion of “permutative conversion” which expresses that the monad is commutative (in fact this latter condition could be dropped and the theory would still hang together, but it is useful for the intended applications to modelling concurrency). Notice that I have not mentioned $\beta$ or $\eta$! Those are not taken as axioms—rather, the type theory is structured to maintain the invariant that all terms are fully $\beta$-reduced and $\eta$-expanded. (This was a very innovative idea at the time, since it entirely side-stepped one of the traditional thorny issues in dependent type theory.)

Since the monad/adjunction is actually present in the type theory (i.e., there is a corresponding type constructor), a complete semantics would presumably reflect this. Perhaps one could obtain a sound semantics in indexed closed monoidal categories by instantiating to the identity monad, though I haven’t checked this and don’t know if anyone else has.

As for the paper by VÃ¡kÃ¡r, well, it seems that he considers various different corners of the design space for “intuitionistic linear dependent type theory”. The specific theory ILDTT, though, does seem quite close to CLF in expressive power—in particular the restriction to types dependent on an intuitionistic context—and so I would be very interested if he could adapt his semantics to CLF (keeping in mind what I said above about the “missing monad”). This might help to resolve the conjectures listed on p.19, since these are precisely the kinds of issues which the CLF approach was designed to circumvent.

]]>