jonsterling
commented
9 years ago There are a couple things to note. First, informally we usually consider each theory to be adding operators to a pre-existing sort. However, we can show that our theories are more modular than that in reality, by parameterizing them over a sort, as I have done in the OCaml implementation.
I haven't been writing to my blog, and I don't have time to clean up my thoughts right now. But I wanted to put this down somewhere so I don't forget it.
The primary purpose of this exercise is to develop meaning explanations for intensional type theory which are as modular as the ones for extensional type theory. In the past I have thought, "Meaning explanations for ITT may be read as NBE + bidirectional typechecking", but now I think it may be more profitable to consider it from the opposite direction, and say "NBE + bidirectional typechecking may be 'informalized' as meaning explanations for ITT". Writing a small proof assistant suffices as a good way to tell just how modular the meaning explanations really are, and clarifies technical issues that are very murky when considered (only) informally.
First, what does it mean for meaning explanations to be modular? In my view, it means being able to divide the logic up into separate theories, each of which contains some self-sufficient portion of the logic. A theory in ETT/CMCP introduces the following things: canonical operators, non-canonical operators, computation rules, and evident judgements with conclusions of the following kinds:
A is a canonical type,M is a canonical verification of A,M and N are equal canonical verifications of A.A theory in ITT would introduce operators intersected across two axes: canonical vs non-canonical, and syntactic vs semantic; also introduced are mappings from syntactic terms to their denotations, and
reify/reflectfor semantic terms, and lastlyquotewhich takes semantic terms back to syntax. This is largely technical, and the details of this may differ in various formulations, but it is not so important. Additionally, an ITT theory introduces evident judgements of the following kinds:M is a canonical verification of A in context Gandu is a direct use of R synthesizing A in context G, or something along these lines.Whether ITT or ETT, the separate theories are composed together into a larger theory, and then the meanings of the derived judgement forms are instantiated. In ETT, this means the judgements for non-canonical forms and also the sequent judgement. In ITT, this means the judgements for non-normal forms, namely the familiar
G !- M <= AandG !- R => Ajudgements; additionally, the equality judgements are also defined all at once, since the equality in ITT is intensional and based on NBE yielding sufficiently canonical forms for comparison. Sadly the sequent judgement must be part of the most primitive atomic judgements for ITT, since it represents derivability and not admissibility; as such, it's not possible to define it separately using hypothetical judgement, since the meaning of hypothetical judgement it actually admissibility rather than derivability (this is why in ETT, you can sayx : False >> 34 ε Bool).[Please see #1 for technical discussion of the shortcomings of the OCaml implementation and how to fix them.]