Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 23rd 2012
    • (edited Oct 23rd 2012)

    created an entry modal type theory; tried to collect pointers I could find to articles which discuss the interpretation of modalities in terms of (co)monads. I was expecting to find much less, but there are a whole lot of articles discussing this. Also cross-linked with monad (in computer science).

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 23rd 2012

    added paragraph Examples - Geometric modality: Grothendieck topology. (deserves being re-written already, but I am too tired now, feel free if you have the energy). Linked to Goldblatt's article. Does anyone have a copy of that article? I only saw the first page. Also cross-linked with Lawvere-Tierney operator

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 23rd 2012

    So this is what Valeria de Paiva was talking about here. I wonder how these different approaches relate, such as with the modality-coalgebra-comonad approach.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeOct 23rd 2012
    • (edited Oct 23rd 2012)

    Thanks!

    I feel unable to read that second reference right now. Is it possible to quickly summarize the coalgebraic formulation of modality?

    Since, as we discussed at some length not long ago, an algebra over an endofunctor is equivalently an algebra over the corresponding free monad, a kind of direct relation between the two algebraizations immediately suggests itself. But I don’t know.

    If you look at Moggi’s original article in def. 4.7, he immediately identifies a modal operator with an algebra over the given operad.

    • CommentRowNumber5.
    • CommentAuthorTim_Porter
    • CommentTimeOct 24th 2012

    Another possible link is to here. The paper gives an interpretation of the proof theory of Intuitionistic S4 in terms of homotopy theory! I don’t see where to put the link.

    There is a lovely survey article by Goldblatt on algebraic semantics of modal logics. (see algebraic model for modal logics).

    There is a considerable literature on comonads, streams, see Alexander Kurz’s homepage. I have created Alexander Kurz.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeOct 24th 2012
    • (edited Oct 24th 2012)

    Another possible link is to here.

    Thanks, I have added that to the list at modal type theory.

    The paper gives an interpretation of the proof theory of Intuitionistic S4 in terms of homotopy theory!

    Is that true? I just see that it uses (augmented) simplicial sets, but not the homotopy theory of simplicial sets.

    By the way, it seems to me that the simplicial set which they assign to a type in Definition 20 is the bar construction of the modality, regarded as a (co)monad. In as far as we follow Moggi, Kobayashi, de Paiva et al and identify modal operators with monads (in computer science) such bar constructions are available always.

    However without some genuie homotopy theory in the game, these bar constructions are not resolutions of anything. So I’d be careful with saying that this is homotopy theoretic.

    (see algebraic model for modal logics).

    Thanks. I didn’t even know that this entry existed. It wasn’t linked to from modal logic. (There was a broken linked that probably meant to point there. I have fixed that and did a bunch of further formatting on these and related entries.)

    • CommentRowNumber7.
    • CommentAuthorTim_Porter
    • CommentTimeOct 24th 2012

    There was a very recent meeting at Dagstuhl. Its webpage has a good motivation section.

    • CommentRowNumber8.
    • CommentAuthorTim_Porter
    • CommentTimeOct 24th 2012
    • (edited Oct 24th 2012)

    I think that in that Intuitionistic S4 paper , Eric and Jean do not exploit any homotopy theoretic aspect, except to think of proofs as being homotopies in some sense. It is some time since I studied that paper so I am not sure. They used the decalage I think.

    There is a page on logic which lists a lot of those pages. I have added a link to modal type theory.

    I think the link was under algebraic semantics.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 24th 2012

    Is it possible to quickly summarize the coalgebraic formulation of modality?

    I think this paper gives quickest access. But briefly, in the propositional case, on the syntactic side we have Boolean algebras. There’s an endofunctor corresponding to the addition of a modal operator, such that algebras for the endofunctor are modal algebras. Across the syntactic-semantic divide via Stone duality, we have categories of models. The composition of the dualising passage to syntax, the modal endofunctor, and the dualising return to semantics is an endofunctor on models. Coalgebras for this endofunctor provide the semantics for modal theories. E.g., maybe the introduction of an accessibility relation between worlds.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 24th 2012

    @David #9: Boolean algebras are the syntactic side? I usually think of a Boolean algebra as the semantics of classical propositional logic.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeOct 24th 2012

    There’s an endofunctor corresponding to the addition of a modal operator, such that algebras for the endofunctor are modal algebras.

    I see. Thanks. That doesn’t seem to be on the nnLab, or is it? Maybe you could paste your summary to the Idea-section of a suitbale entry?

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeOct 24th 2012

    I edited the page some, trying to clarify where “modality” means something acting on propositions and where it means something acting on more general types.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 24th 2012

    @Mike #10, but any Boolean algebra is the Lindenbaum-Tarski algebra (classes of logically equivalent propositional sentences) of a propositional theory. Shouldn’t I see that as syntactic? Then maps into 22 effectively give us the lines of its truth table, i.e., the models.

    But then is it straightforward to distinguish syntactic and semantic anyway? I get confused by this. For one thing, there are term models. But then when 22 and then SetSet play their dualising roles between syntax and semantics, I should consider the dualising objects as both syntactic and semantic?

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeOct 24th 2012

    Thanks, Mike.

    So suppose somebody sees this list and feels like deducing a simple general statement:

    Modal type theory is type theory equipped with (co)monads.

    I imagine many modalists would complain when seeing such a statement. What would such complaints be? To which extent am I entitled to make the identification between modal type theory and the simple notion of type theory with (co)monads? Which subtleties would such an identification be missing? Are any of these subtleties “essential”?

    • CommentRowNumber15.
    • CommentAuthorTim_Porter
    • CommentTimeOct 24th 2012
    • (edited Oct 24th 2012)

    As I said on another thread:

    In case this helps for the semantics vs. syntax discussion, there is an entry on the Lindenbaum-Tarski algebra of a normal modal logic.

    There is also a coalgebraic canonical model. This has the set of Λ-maximal consistent formulae as its set of states. (see that entry). Both the algebra and the coalgebra are considered as giving the semantics of the logic. Note that in maximal consistent, the link with ultrafilters is mentioned, and of course they come in quite naturally from the context.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeOct 24th 2012
    • (edited Oct 24th 2012)

    Modal type theory is type theory equipped with (co)monads.

    I imagine many modalists would complain when seeing such a statement. What would such complaints be?

    I started reading

    • Satoshi Kobayashi, Monad as modality, Theoretical Computer Science, Volume 175, Issue 1, 30 (1997), Pages 29–74

    which concerns this question. With Moggi the author amplifies that strong monads on the type system have some defect when it comes to regarding them as an interpretation of modalites (and then he discusses that neverteless “\mathcal{L}-strong monads” work nicely in this respect ).

    What is it that makes these authors reject a type system with a strong monad as a modal logic? It seems to me that there are two separate issues:

    1. Type systems with strong monads on them don’t have a “natural modal logic” that is “like S4”. (see e.g. beginning of Kobyashi’s section 4)

    2. Type systems with strong monads on them violate some aspect of “proofs-as-programs”. (this Kobayashi fixes in his section 7 by introducing \mathcal{L}-strong monads instead)

    My impression is that the first point is purely a matter of taste, while the crux is in the second point. For over at modal logic we cite modal textbooks that admit that nobody has a global definiton of what modal logic is and what it is not. So if something is almost but not quite like S4 modal logic, then how would we know that we definitely don’t want to call it another flavor of modal logic?

    The second point seems to contain the actual technical content. I haven’t absorbed Kobayashi’s section 7 yet (dinner was over before I got through, now I need to do something else). Is this somehow related to whether or not we can find a “computationally effective” implementation, or decidable etc.?

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeNov 3rd 2012

    @David 13: I guess I use the word “syntactic” more narrowly than some people. To me, syntax is about symbols written on a page. The moment you scoop up a bunch of those symbols, mod them out by some equivalence relation and put some structure on the resulting set, then you have a model, i.e. semantics, even if it’s a semantics “built out of syntax”. The term model is the “initial semantics” but it is itself already semantics.

    @Urs: My view is that a “pluralistic” view of modal logic does not restrict it to considering modalties which behave like the most classical “necessity” and “possibility” modalities. From that point of view, type theory with (co)monads is most definitely a modal type theory. I guess this is what you mean by saying that Kobayashi’s first point is a matter of taste. On the other hand, I would certainly shy away from claiming that everything one might call a “modality” is either a comonad or a monad.

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 3rd 2012

    I think it’s good that the coalgebra community tries to make contact with historical understanding of modality as ways of describing the status of certain propositions. See, e.g., Modal Logics are Coalgebraic

    …the vast and growing family of modal logics, which are characterised by having operators that qualify formulas as holding in a certain way, e.g. ’necessarily’, ’in the future’, ’everywhere’, ’probably’, ’as everyone knows’, or ’normally’.

    And

    In a seemingly simple piece of knowledge such as ’Normally, the likelihood of road congestion is smaller on weekends’, one implicitly makes use of default logics (’normally’), probabilistic reasoning (’the likelihood’) and temporal knowledge (’weekends’) under a quantitative regime (’smaller’).

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeNov 3rd 2012

    @Urs: As for your second point, what I got out of Kobayashi’s paper was different: it seemed to me that he was saying that strong monads don’t match the traditional meaning of “possibility”-like modalities (your first point) and that therefore Moggi thought that “modal logic” — meaning S4-like logics rather than the more pluralistic view I would favor — doesn’t have a good categorical semantics and thus can’t have a good proofs-as-programs interpretation. In other words, it sounded to me as though the entire paper was predicated on the idea that “modal logic” means specifically S4-like things, and if we take a more pluralistic point of view on the meaning of “modal logic” then all problems disappear.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2012

    @David, thanks for the reference, I put that into the relevant entries now!

    @Mike:

    type theory with (co)monads is most definitely a modal type theory

    Okay, good.

    if we take a more pluralistic point of view on the meaning of “modal logic” then all problems disappear.

    Okay, good.

    I would certainly shy away from claiming that everything one might call a “modality” is either a comonad or a monad.

    I had this hope that we could say “modal type theory is type theory with (co)monads” because it would make the situation nicely systematic. Because otherwise, it’s disconcerting to have a concept in foundations without a definition. So I tend to wonder now which examples of “modal” type theories are not (co)monadic, and whether they might maybe all have a “fix” that makes them (co)monadic after all. It’s not so important, but that’s what I’d naturally wonder about now…

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2012

    Consider a modality like “Joe believes that …”. Unless Joe is omniscient, we don’t have AA \Rightarrow “Joe believes that AA” for all AA. And unless Joe is infallible, we don’t have “Joe believes that AAA\Rightarrow A for all AA either. So this modality has no unit or counit, hence seemingly can’t be a monad or a comonad.

    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 4th 2012

    Epistemic modalities appear to be very weak. E.g., reasonable versions of belief or knowledge don’t even satisfy distribution

    (pq)(pq)\Box (p \to q) \to (\Box p \to \Box q).

    So I may know pqp \to q and pp, but have not put them together to deduce qq. Same goes for belief. I remember as a child the shock of putting together ’if mammalian mother, then lactates’ and ’mother whale is mammalian’.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2012
    • (edited Nov 5th 2012)

    The thing is, to me it is not even clear why FOL + “Joe believes”-operator deserves to be called a “modal logic”. Unless we call every operator on a plain logic a “modal logic”. Is that what we do?

    Can we have a term for those modalities that are indeed (co)monadic? Of course “monadic modality” could work, but maybe we can better characterize in terms of modality itself what it means to be ‘monadic?

    Maybe “faithful modality” (since it respects at least part of the notion of truth)?

    Is there any established term for this?

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2012

    S4S4 is the modal logic for which

    • (pq)(pq)\Box (p \to q) \to (\Box p \to \Box q)
    • pp\Box p \to p
    • pp\Box p \to \Box \Box p

    This strength makes it just right for topological, and in the first order case, sheaf-theoretic treatment.

    There’s a good list of modal axioms and their frame counterparts here.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2012

    The thing is, to me it is not even clear why FOL + “Joe believes”-operator deserves to be called a “modal logic”.

    I think the meaning of the word “modality” demands it. Along with scads of stuff written by modal logicians. Don’t they get to decide what “modal logic” means?

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2012

    Don’t they get to decide what “modal logic” means?

    But did they?

    • CommentRowNumber27.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 6th 2012

    I doubt you’ll find any very neat definition of what a modal logic is. Along with necessity and possibility, we find

    tense logic: henceforth, eventually, hitherto, previously, now, tomorrow, yesterday, since, until, inevitably, finally, ultimately, endlessly, it will have been, it is being …

    deontic logic: it is obligatory/forbidden/permitted/unlawful that

    epistemic logic: it is known to X that, it is common knowledge that

    doxastic logic: it is believed that

    dynamic logic: after the program/computation/action finishes, the program enables, throughout the computation

    geometric logic: it is locally the case that

    metalogic: it is valid/satisfiable/provable/consistent that (Goldblatt, Mathematical Modal Logic: a View of its Evolution).

    The metalogical version was important in the history of modern modal logic. Gödel played an important role there.

    As is common with such matters, the linking of a philosophical pursuit to something more practical tends to focus minds. Computer scientists have explored modal logics extensively, as with model checking.

    • CommentRowNumber28.
    • CommentAuthorTim_Porter
    • CommentTimeNov 6th 2012

    David. Can you adapt that to give a bit more info on modal logics somewhere on a relevant page? Complete with sources. Perhaps a new page linked to the old one would work well.

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2012

    David,

    can you put this kind of information into the entry on modal logic?

    I understand that in the broad sense every operator that I might think of might be thought of as inducing a modal logic. Nevertheless, when I look at the mathematical literature on modal logics it is only very specific ones that are studied and hence apparently only very specific ones that are considered interesting. I haven’t yet seen a disucssion of the mathematical aspects of the “Joe believes”-logic (though of course that need not mean much, feel invited to give me such a reference).

    The modal logics that I see discussed in the literature are monadic. So therefore I am wondering (still): what do we actually lose (concerning mathematical logic) if we restrict to these? I’d just like to get a feeling for how much the liberty of considering non-monadic modal logic buys us.

    What are major mathematical articles on non-monadic modal logics? What are central structures of interest here? Do you have any pointers?

    • CommentRowNumber30.
    • CommentAuthorTim_Porter
    • CommentTimeNov 6th 2012
    • (edited Nov 6th 2012)

    @Urs: There is quite an extensive literature in the AI and CS communities on belief logics. These are highly mathematical in nature BUT not in motivation. (BTW monadic has two meanings in that area. The other one refers to single ’variable’ operators.) The ‘monad’ axiom is called 4 which gives a ’multiplication’.

    Johan van Benthem has written on these for instance here. These logics often have a common knowledge operator.

    Another source is work by Baltag on Belief revision.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2012
    • (edited Nov 6th 2012)

    Thanks for the links. I have put them into epistemic logic. But let’s further discuss modal logic in the thread on modal logic

    Concerning modal type theory: I have added the pointers

    and a pit more to Modal type theory - References.

    • CommentRowNumber32.
    • CommentAuthorTim_Porter
    • CommentTimeNov 6th 2012

    I have done some changes mentioned on the modal logic thread.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeNov 9th 2012
    • (edited Nov 9th 2012)

    Hey Mike,

    now that I have actually read your note Higher modalities I am both happy and confused:

    • happy, because you say there precisely what in #14 and #23 above I was wondering if we’d be entitled to say: that a modality is a (co)monad on the type system (in the note you go even further and demand it to be an idempotent monad).

    • confused, because in #21 and #25 you seemed to be expressing the view that this is not a justifyable terminology.

    And from this side remark in your note:

    Andrej has suggested that conversely, any “logic” in which implication and universal quanti cation are “natural” ought to come from a modality

    I gather that people like Andrej Bauer have a similar same stance towards modalities as under point “happy” above.

    I also made a little survey among type theorists near me, if they like to consider modalities that are non-monadic. The answers were: no.

    So all that makes me quite happy. I am just confused then about what happened in this discussion here. Maybe there was some misunderstanding?

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeNov 9th 2012

    I think for me it’s an issue of local terminology vs. global terminology. In a particular context where all I care about are monadic modalities, I’m happy to say plain “modality” and mean only monadic ones, just in doing commutative algebra one might say “ring” to mean only commutative ones. But in the context of a wiki page on “modality” in general, I feel obligated to point out that not all modalities are monadic.

  1. In modal type theory are two references broken: #Goldblatt 2006, Lawvere [9]

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeDec 4th 2012
    • (edited Dec 4th 2012)

    Fixed now:

    • Bill Lawvere, Quantifiers and sheaves, Actes, Congrès intern, math., 1970. Tome 1, p. 329 à 334 (pdf)

    And Goldblatt2006 is just Goldblatt as cited there (apparently the online version of that article is dated 2006, so that’s what Google tends to produce.)

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeJan 12th 2014
    • (edited Jan 12th 2014)

    have added to the top of the references at modal type theory a pointer to

    • Matt Fairtlough, Michael Mendler, On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem, Types for Proofs and Programs Lecture Notes in Computer Science Volume 2277, 2002, pp 63-78 {#FairtloughMendler02}

    since this is one of the rare articles that rather explicitly talks about modal type theory (“computational type theory”) as type theory with a monad on the type system, and what it’s good for.

    (I feel with much of the literature this simple basis is somehow never stated very clearly, but I may have been looking at the wrong literature all along, of course.)

    • CommentRowNumber38.
    • CommentAuthorspitters
    • CommentTimeJan 13th 2014

    It is not so clear to me yet how these modal type theories connect to the ones we use in homotopy type theory. The latter are idempotent, for one.

    • CommentRowNumber39.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 13th 2014

    So in the Fairtlough-Mendler paper (p. 5), [K,L)[K, L) is idempotent, but conjunctions of these need not be?

    Is there a reason HoTT should be committed to idempotent modalities?

    • CommentRowNumber40.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 13th 2014
    • (edited Jan 13th 2014)

    Curry’s proposal was to take ϕ\bigcirc \phi as the statement “in some stronger (outer) theory, ϕ\phi holds”. As examples of such nested systems of reasoning (with two levels) he suggested Mathematics as the inner and Physics as the outer system, or Physics as the inner system and Biology as the Outer. In both examples the outer system is more encompassing than the inner system where reasoning follows a more rigid notion of truth and deduction. The modality \bigcirc, which Curry conceived of as a modality of possibility, is a way of reflecting the relaxed, outer notion of truth within the inner system.

    A fun idea, but what does it mean? It’s surely not the idea that physicists’ notions of proof are weaker than mathematicians, as in that Jaffe-Quinn criticism of the sloppy habits of physics invading maths. If I recall correctly, they were after some kind of warning sign to show that a result had only been reached to a lesser standard. Maybe ϕ\bigcirc \phi could mean ’we have a physicist’s proof of ϕ\phi’.

    (Then idempotency fails since ’we have a weak proof that we have a weak proof of ϕ\phi’ is not the same as ’we have a weak proof of ϕ\phi’?)

    Curry’s idea seems in line with Neel’s here:

    In the judgmental approach to modal type theory, we view modal types A\Diamond A as internalizations of categories of judgment.

    That is, in Martin-Löf’s judgmental methodology, we take the assertionPP is true”, and then introduce a judgement of “PP is true”, which explains what constitutes evidence for PP (the introduction rules), and how to use a PP (the elimination rules). We can extend this to modalities by introducing new judgements to represent new categories of assertion. So in addition to “PP is true”, we might also have categories of judgment such as “PP is known to XX”, “PP will eventually be true”, “PP is possible”, and so on. Then, a modal type like A\Diamond A is an internalization of a judgement. That is, we can say that the introduction rule for the judgement “A\Diamond A is true”, is actually evidence for the judgement “AA is possible”.

    In categorical proof theory, we typically take a judgement to be a category \mathbb{C}, with the types represented by the objects of \mathbb{C}, derivations of judgements given by morphisms f:ΓAf : \Gamma \to A (with the context Γ\Gamma represented by some kind of tensor product), and type constructors interpreted by (possibly nn-ary and contravariant) endofunctors T:T : \mathbb{C} \to \mathbb{C}.

    To extend this to judgmental modal type theory, we can introduce categories ,𝔻\mathbb{C}, \mathbb{D} and so on for each category of judgment, and then take type constructors to be functors between these different categories. This makes the appearance of monads and comonads in modal type theory very natural. In some sense, adjoint functors give an “optimal” way of relating different categories, and composing a pair of adjoint functors gives you a comonad or monad, depending on which way around you go.

    As a concrete example, take \mathbb{C} to be the category of predomains and continuous functions, and 𝔻\mathbb{D} to be the category of pointed domains and strict continuous functions. Then, we can interpret morphisms of \mathbb{C} as proofs that a proposition is true, and 𝔻\mathbb{D} as “possible proofs”. That is, 𝔻\mathbb{D} supports unrestricted recursion (has a natural transformation 𝕗𝕚𝕩 A:(AA)A\mathbb{fix}_A : (A \Rightarrow A) \to A), and so non-normalizing terms can be defined, by taking fixed points that don’t decrease along a well-order.

    If you move back to model theory, all this is is a way of saying that models are lattices, and modal operators come via monotone functions between lattices and Galois connections. This all makes me feel that some variant of the Stone representation theorem should enable you to produce worlds and Kripke models from this “point-free” account of modal logic.

    • CommentRowNumber41.
    • CommentAuthorspitters
    • CommentTimeJan 13th 2014

    David, Idempotent modalities are used to obtain a well-behaved dependent eliminator see Mike’s note.

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2014

    Bas,

    It may be harder to specify the syntax for non-idempotent modalities, but that seems no reason to not consider them. In fact HITs are going to be defined via non-idempotent monads.

    • CommentRowNumber43.
    • CommentAuthorspitters
    • CommentTimeJan 13th 2014

    Urs, I mentioned how idempotency was used. It may be possible to generalize this, but I don’t think it has been done yet.

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2014
    • (edited Jan 13th 2014)

    I keep having this perspective that we have the syntax/semantics equivalence of relation between type theory and category theory. In this sense we certainly know precisely what the semantics of modal type theory with non-idempotent monads is. Maybe somebody still has to write out the syntax for this (not sure, this is the issue we are discussing over at computational type theory, too, some type theorists at least behave as if this exists), but this seems to be a matter of sitting down and doing it, not of principle.

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2014

    In the introduction of the 95 article by Valeria de Paiva et al there is a nice comment on why monads on a type system fit well with the original idea of modal logic (and they consider not-necessarily idempotent monads). I have recorded that in the entry as follows:


    Following (Moggi91, Benton-Bierman-de Paiva 95, Kobayashi 97) modal type theory is specifically understood as being a type theory equipped with a monad on its type system, representing the intended modality. Since monads in computer science embody a notion of computation, some authors also speak also of computational type theory here (Benton-Bierman-de Paiva 95, Fairtlough-Mendler 02).

    According to (Benton-Bierman-de Paiva 95, p. 1-2) this matches well with the default interpretation of (S4) modal logic as being about the modality TT of “possibility”:

    The starting point for Moggi’s work is an explicit semantic distinction between computations and values. If AA is an object which interprets the values of a particular type, then T(A)T(A) is the object which models computation of that type AA. [...][...] For a wide variety of notions of computation, the unary operator T()T(-) turns out to have the categorical structure of a strong monad on an underlying cartesian closed category of values. [...][...] On a purely intuitive level and particularly if one thinks about non-termination, there is certainly something appealing about the idea that a computation of type AA represents the possibility of a value of type AA.


    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeJan 13th 2014

    Urs, you keep having that perspective, and we keep telling you that the problem of finding syntax that has these semantics is really hard and not “just a matter of sitting down and doing it”.

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2014
    • (edited Jan 13th 2014)

    Sorry, but I am still not getting the complaint. For instance we have an entry internal logic that does just this, assert that every category comes with its internal logic. By just the same reasoning every category comes with its internal type theory. I don’t see why one should not be allowed to talk about this.

    Moreover, in the present case at hand there are plenty of type theory articles on non-idempotent modalities in type theory. Are these somehow objectionable?

    • CommentRowNumber48.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2014
    • (edited Jan 13th 2014)

    Let’s see at which point precisely the issue is.

    Take Seely’s functor from suitable categories to type theories

    Lang:LCCCategoriesMLTypeTheories Lang \;\colon\; LCCCategories \longrightarrow MLTypeTheories

    refined to a 2-functor by Clairambault-Dybjer (references just for completeness, I know that you know this well).

    This 2-functor is an equivalence and takes monads to monads. The image of a monad under LanLan we may hence call a “modal type theory”.

    So is the issue maybe that there is a more formal notion of type theory than appears in these articles by Seely and Clairambault-Dybjer, one defined in terms of some sequent calculus (these authors don’t talk about natural deduction)? Is it maybe indicated to distinguish different “levels of formality” of “type theory”?

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeJan 13th 2014

    I thought you were talking about homotopy type theory and (,1)(\infty,1)-categories. It’s the \infty-monad part that’s difficult. Ordinary 1-monads in extensional type theory are, as far as I know, not problematic.

    The statement “every category comes with its internal logic” does not have a precise meaning. It’s a heuristic which guides us to discovering an appropriate internal logic for each given kind of category.

    • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    Mike, when you have a second, could you maybe react to the last part of the question:

    What Seely’s article and in particular what Clairambault-Dybjer’s article calls a “type theory”, isn’t that something that deserves to be called “type theory” but is less formalized, in a sense, than those things that you implement on computers? Doesn’t it make sense to speak of this “type theory” and of “fully formalized type theory”, where the latter is what is given by symbol rewriting rules, whereas the former is given more at the usual level of mathematics?

    At the usual level of formality in mathematics it seems to me we easily assign an internal logic to any category, and my impression is (or at least was) that this is what everybody always meant who edited the entry on internal logic: it’s the logic whose propositions are the subobjects, whose implications are the morphisms between them, whose conjunctives are product and coproduct in the slice, if they exist, and so on. This seems to be more than heuristics, while of course it is less than having a computer implementation of this logic.

    • CommentRowNumber51.
    • CommentAuthorZhen Lin
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    The word “logic” here is being abused somewhat, perhaps. To me, a logic necessarily has an associated deductive system – after all, it is supposed to be a mathematical model of reasoning. It makes no sense to talk about logic at “the usual level of mathematics”. The so-called “internal logic” is just a language and an associated semantics – it does not come with a deductive system. If we are to take the stance that every category has an internal logic in the fashion you describe, then the implicit deductive system we get is useless: not even the basic structural rules of sequent calculus – the kind that people like to forget about but use all the time – will be valid.

    • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014
    Okay, good. Now isn't it right that the same applies to the way "type theory" is used in the articles by Seely and maybe more so that by Clairambault-Dybjer, mentioned above?
    • CommentRowNumber53.
    • CommentAuthorZhen Lin
    • CommentTimeJan 14th 2014

    I am not familiar with either paper, but it appears to me that Clairambault and Dybjer are honest and (except for the title) do not conflate type theories with related structures (e.g. categories with families). I do not accept your claim that the latter deserve the name “type theory”.

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    This is not something that I dreamed up. If there is something to be objected to here, than various nnLab entries need to be re-written or at least equipped with more qualification, notably relation between category theory and type theory.

    That quotes Clairambault-Dybjer as completing the proof of the equivalence between dependent type theories and locally cartesian closed categories. I seem to remember that this was pointed out by Mike in the first place, but in any case this nLab entry has been discussed widely among people who should know, and there was never an objection.

    But it is good that we finally maybe discuss this issue, it seems to have been implicitly behind various unfruitful exchanges elsewhere.

    I’d be inclined to come back to my suggestion in #48 that we should have two terms to distinguish between two shades of “type theory”. Or something.

    But I’d really like to hear Mike’s comment on this.

    • CommentRowNumber55.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 14th 2014

    Re #51: it might make more sense however to refer to the “logic” associated with a doctrine (which here might mean a 2-monad on CatCat, at least as a first approximation). For example, there is a logic of symmetric monoidal categories, a logic of finite limit categories, a logic of exact categories, and so on. The basic idea being that the free structured categories of some type capture the appropriate notion of equivalence classes of deductions. The further point being that the mode of deductive system (sequent calculus, natural deductions, Hilbert-style proofs, or whatever) is not necessarily the most important thing, but what is important is that differing modes of presentation agree on the appropriate equivalence classes of deduction, two deductions being equivalent if their interpretations as morphisms in free structures agree. These are the invariants of the “logic”.

    • CommentRowNumber56.
    • CommentAuthorZhen Lin
    • CommentTimeJan 14th 2014

    Re #53:

    The point I was trying to make is that syntactic categories are not themselves logics (or even logical theories). In my view it is perfectly reasonable to distinguish between Morita-equivalent theories (e.g. vector spaces over a field kk and modules over the matrix ring M n(k)M_n (k)).

    Re #55:

    Yes, I agree: we should only speak of, say, “the internal logic of D\mathsf{D}-categories” for some doctrine D\mathsf{D}. But I insist that there must be at least one reasonable deductive system associated with that “logic”, which is hopefully computable in an appropriate sense. Recall the story of the Mickey Mouse proof system [Miller, p.57], which is sound and complete but utterly useless…

    • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    So what do you like to call the something that is associated to a specific category. The “internal language”? “internal logical language”? “internal type language”? “internal type theoretic language”?

    Generally, how would you suggest to restate all the statements at relation between category theory and type theory?

    • CommentRowNumber58.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    Also for instance syntactic category would need to be re-written, if these complaints here are to be reflected. Various related entries probably too.

    How do we deal with this? (And why did this issue not come up before?)

    • CommentRowNumber59.
    • CommentAuthorZhen Lin
    • CommentTimeJan 14th 2014

    There are three components to the “internal logic” of a category (or indeed any structure whatsoever): a language L\mathsf{L} in the appropriate formal system, an interpretation MM of L\mathsf{L}, and the collection T\mathsf{T} of all sentences that are true under that interpretation. I have no objections to calling L\mathsf{L} the “internal language”, but as Paul Taylor points out, this language is in fact an entity at the meta level, i.e. external. MM could be called the “canonical interpretation” or, tongue in cheek, “intended semantics”. Model theorists call T\mathsf{T} the “L\mathsf{L}-theory of MM” (or perhaps {M}\{ M \}). The ideal theorem would say that MM is a universal model of T\mathsf{T}.

    I can’t think of a good name for the triple (L,M,T)(\mathsf{L}, M, \mathsf{T}). But maybe we shouldn’t give it a name – these three things are different, and not realising that they are different caused me some confusion when I was learning this stuff…

    • CommentRowNumber60.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    Re #57: the phrase “internal language” seems alright to me (internal language of a topos, of a cartesian closed category, etc.). Typically this has a type-theoretic flavor (with basic types being objects, and with terms coming from morphisms). Notice that the sense of internal language is relative to a doctrine (so that the internal language of a topos EE is not the same as the internal language of EE considered as a ccc): the rules of type and term formation in these cases differ and are dictated by the doctrine D\mathbf{D}. Actually, the language would correspond to the free D\mathbf{D}-object F(E)F(E) generated by the given structured category or D\mathbf{D}-object EE. There is then an interpretation F(E)EF(E) \to E given by the doctrinal counit. The internal theory would be F(E)F(E) coupled with a description of when two terms in F(E)F(E) have the same interpretation in EE; it corresponds to the canonical presentation

    FF(E)F(E)EF F(E) \stackrel{\to}{\to} F(E) \to E

    and EE could be considered the universal model of that theory.

    But what do you mean “all the statements at relation between category theory and type theory” [need to be corrected]? What I saw at the article looked pretty good (I didn’t read all the way through), and actually was in accord with this doctrinal point of view. Are there particular statements there you could point to that you now think need revision?

    • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    Todd, thanks,

    over at relation between category theory and type theory it seems that “type theory” (following at least Seely) is used for what here is being argued should not be called such, but should just be called “internal language”.

    In particular the main statements there concern equivalences between , notably, the 2-category of locally Cartesian closed catgeories and 2-categories “of dependent type theories”. But by what you are saying here instead it should say “dependent type theory is the theory of the doctrine of locally Cartesian closed categories” or something, while the equivalence in the entry is between the 2-category of lcc categories and that of their internal languages.

    Well, I am not arguing myself that the entry needs to be changed this way, I am just saying that given what you say, it would have to be changed.

    No?

    • CommentRowNumber62.
    • CommentAuthorMike Shulman
    • CommentTimeJan 14th 2014

    I’m still back on #50. There is, I guess, a difference between a fully formalized and implemented type theory and a less formal one, but that is not what’s going on here. I also don’t think that Zhen’s point about deductive systems is what is going on.

    Consider basic MLTT. This is a formal system, with deductive rules, which can be interpreted into any LCCC. Moreover, if you add some “undefined” types and terms to it as axioms, then you get a new type theory, say TT, which can be interpreted into any LCCC CC as soon as you specify the interpretation of those types and terms as objects and morphisms in CC. In particular, if you start with the LCCC CC, then you can construct the type theory TT whose axioms are precisely the objects and morphisms of CC. This is the “internal logic” or “internal language” of CC.

    The theorem of Seely-Clairambault-Dybjer is that LCCCs are biequivalent to a 2-category whose objects are type theories of this form: MLTT augmented by some type-and-term axioms. This is most evident in Seely’s paper; it’s hidden a bit in the Clairambault-Dybjer paper because they reformulate the latter notion in terms of categories-with-families, I think to make it into a 2-category more easily.

    However, when we say “modal type theory”, we mean an augmentation of the basic system of rules of MLTT, not an adding of axioms. The intent is then that if we consider this type theory with added rules, and consider the 2-category of type theories obtained by adding axioms, that would be equivalent to the 2-category of LCCCs-with-monads, or something of that sort. I think this is what Todd is getting at by talking about the “doctrine”. When you fix a doctrine of a kind of category, then that is supposed to determine (although there is no algorithm for this) a basic type theory with rules; then the “internal language” of any particular category in that doctrine is an augmentation of that basic type theory by axioms that represent the objects and morphisms of that category.

    • CommentRowNumber63.
    • CommentAuthorZhen Lin
    • CommentTimeJan 14th 2014

    I think #62 hits the nail on its head perfectly and says what I was trying to say much more clearly. The deductive system / language / theory distinction is not as clear in type theory as it is in traditional logic, but what I would say that the difference Mike pointed out is precisely that. In my view, Martin-Löf type theory is a deductive system, a language with respect to that deductive system is a list of constant type and term symbols, and a theory with respect to a language is a deductively closed collection of judgements in that language.

    • CommentRowNumber64.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014
    • (edited Jan 14th 2014)

    Thanks, Mike!

    I follow that. Please bear with me now when I ask yet another question (I am not trying to be obnoxious, I just would like to have this sorted out for myself and for communication with you and others):

    By what you say, there are two things which we’d rather like to distinguish, but which are both called “type theories”, only with different qualifiers.

    There is what you call “basic type theory”/”basic system of rules” and then there are “new type theories” obtained from this by adding “types and terms to it as axioms”. Indeed, you confirm now that an internal language is a “type theory”:

    you can construct the type theory T whose axioms are precisely the objects and morphisms of C. This is the “internal logic” or “internal language” of C.

    Good, that’s a relief. If this is so then we don’t need to change a bunch of nnLab entries (as would be the case if we adopted Zhen Lin’s standpoint).

    I suppose this also refines your complaint above that the entry internal logic is “just a heuristic”. If I understand you correctly all that this entry is missing is some global statement at the beginning of the form “Fix a doctrine once and for all, and let CC be a category in this doctrine. Then the internal logic of CC is…”

    But now here is finally my remaining question: if the “internal language” of some specific LCCC is “a type theory” by your above statement (albeit not a “basic” one) then the internal languag of some specific LCCC with a monad on it should be “a modal type theory, albeit not THE basic modal type theory”.

    Right? I suppose what I am asking for is a clear terminology to distinguish between those “basic type theories”/”basic rules” and the “new type theories” which are “internal languages”, as you say.

    • CommentRowNumber65.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 14th 2014

    I guess the ’theory’ of ’type theory’ doesn’t help. One talks of a first-order theory meaning something couched in first-order logic, with some specified predicate, relations, constants and axioms. Had it been, say, ’type calculus’, then ’a type theory’ would have been clearer.

    • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeJan 14th 2014

    I wouldn’t use “modal type theory” to mean a type theory with a monad on it, but rather a type theory with rules that model a monad on the semantics.

    Unfortunately, I don’t think a clear terminology on the type-theoretic side exists to distinguish between “theories” and “doctrines”. You just have to get used to it. )-:

    • CommentRowNumber67.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2014

    Hm, well, I wouldn’t have any problem getting used to the fact that the terminology is ambiguous were it not for the fact that I nevertheless hear not to use it this way or that way. But, yeah, I suppose that I have to get used to.

    • CommentRowNumber68.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 15th 2014

    So is the lesson to draw from this discussion that nobody has devised a type theory with rules that model a monad on the semantics (#46), while it has been done in the case where the monad is idempotent?

    • CommentRowNumber69.
    • CommentAuthorUrs
    • CommentTimeJan 15th 2014

    Type theory with deduction rules for non-idempotent monads has been considered, see for instance section 2 of de Paiva et al..

    What has not been done is the analog for \infty-monads in homotopy type theory.

    To recall: the discussion above comes from me saying that since we know what the semantics of these is, and since whatever syntax for it one comes up it’s supposed to be equivalent to that semantics, analogous to the Seely-Clairambault-Dybjer equivalence, that it doesn’t hurt to speak about it. Mike feels that doing so doesn’t sufficiently highlight the trouble of actually writing down the syntax (which I assume he is working on, at least in part, for formulating HITs). Then I asked which words I could be excused to use for expressing the evident statement that does have a right to be expressed here. And it seems the answer is that such words have not been agreed on.

    • CommentRowNumber70.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 15th 2014

    Yes, I dropped the \infty.

    I wonder why the \infty case is harder. Doesn’t truncation often make things more complicated?

    • CommentRowNumber71.
    • CommentAuthorUrs
    • CommentTimeJan 15th 2014
    • (edited Jan 15th 2014)

    Because of the coherences. Therefore I suppose, as we discussed in the other thread, that for \infty-monads which are explicitly given as the endomorphism monads of an \infty-adjunction it is much easier. While this is naturally the situation in the applications that I am currently considering, it is probably of little use for the discussion of HITs.

    • CommentRowNumber72.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2014

    which I assume he is working on, at least in part, for formulating HITs

    No, actually, the nice thing about HITs is that you can describe the initial algebras for a presented monad in terms of the presentation only, without having to make any sense of the monad itself.

    • CommentRowNumber73.
    • CommentAuthorUrs
    • CommentTimeJun 10th 2018

    Added pointer to Licata-Shulman-Riley 17 and Licata 18 also here at modal type theory, where it seems to more properly belong than at adjoint logic.

    diff, v36, current

    • CommentRowNumber74.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 10th 2018

    I posed the issue of the best way to record this work over here. I think when Mike’s nn-theories ideas are settled (perhaps they are already) that would provide the ideal framework.

    • CommentRowNumber75.
    • CommentAuthorspitters
    • CommentTimeJun 11th 2018

    A bit of self-promotion for our article on modal type theory and dependent right adjoints.

    diff, v37, current

    • CommentRowNumber76.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018

    added pointer to the video recordings of Licata-Wellen 18

    diff, v38, current

    • CommentRowNumber77.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 5th 2018

    Added

    It is informally understood that the purpose of modal type constructors in programming calculi is to control the flow of information between types. In order to lend rigorous support to this idea, we study the category of classified sets, a variant of a denotational semantics for information flow proposed by Abadi et al. We use classified sets to prove multiple noninterference theorems for modalities of a monadic and comonadic flavour. The common machinery behind our theorems stems from the the fact that classified sets are a (weak) model of Lawvere’s theory of axiomatic cohesion. In the process, we show how cohesion can be used for reasoning about multi-modal settings. This leads to the conclusion that cohesion is a particularly useful setting for the study of both information flow, but also modalities in type theory and programming languages at large.

    diff, v41, current

    • CommentRowNumber78.
    • CommentAuthorUrs
    • CommentTimeMar 17th 2019

    added pointer to

    diff, v43, current

    • CommentRowNumber79.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 18th 2019

    Is the eagerly anticipated

    • A Fibrational Framework for Substructural and Modal Dependent Type Theories, 2019

    appearing very soon? I’d like to mention it.

    • CommentRowNumber80.
    • CommentAuthorUrs
    • CommentTimeMar 18th 2019
    • (edited Mar 18th 2019)

    added the following pointers:


    diff, v44, current

    • CommentRowNumber81.
    • CommentAuthorAli Caglayan
    • CommentTimeMar 18th 2019

    @David do you mean

    A Fibrational Framework for Substructural and Modal Logics

    • CommentRowNumber82.
    • CommentAuthorMike Shulman
    • CommentTimeMar 18th 2019

    Re #79 I hope so; the details are very fiddly and we keep having to change it around. Plus some of us had some personal issues that delayed things. But Dan is talking about it this week at HoTTEST if you want to hear the latest and the greatest.

    • CommentRowNumber83.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 18th 2019

    Re #82, I look forward to it.

    Re #81, no it’s the next instalment: modal unary type theory; modal simple type theory; modal dependent type theory, as explained here.

    • CommentRowNumber84.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 4th 2019

    Added the reference

    • Daniel Gratzer, Jonathan Sterling, and Lars Birkedal, Implementing Modal Dependent Type Theory, (pdf)

    Perhaps we need a special page for modal dependent type theory.

    diff, v46, current

    • CommentRowNumber85.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2019

    Added pointer also to the implentation on github.com/jozefg/blott

    diff, v47, current

    • CommentRowNumber86.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2019

    added pointer to

    • Daniel Gratzer, Implementing Modal Dependent Type Theory, talk at ICFP 19 (slides pdf)

    diff, v49, current

    • CommentRowNumber87.
    • CommentAuthoratmacen
    • CommentTimeAug 21st 2019
    Were “slides” and “pdf” supposed to be separate links?
Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)