Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorZhen Lin
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownI started an article about [[Martin-Lof+dependent+type+theory|Martin-Löf dependent type theory]]. I hope there aren't any major mistakes! One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

   I started an article about Martin-Löf dependent type theory. I hope there aren't any major mistakes!

   One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

2. • CommentRowNumber2.
   • CommentAuthorNeel Krishnaswami
   • CommentTimeSep 9th 2011
   • (edited Sep 9th 2011)
   • PermaLink
   Author: Neel Krishnaswami
   Format: TextDear Zhen Lin, In programming languages research (closely connected to, but not quite the same as, type theory) $\mathrm{case}$ is the usual name of the finite sum type. However, the dependent sum type is usually given a projective elimination: <latex>\begin{matrix} \frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B} {\Gamma \;\vdash\; \pi_1(t) \;:\; A} \\ \\ \frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B} {\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]} \end{matrix} </latex> My understanding is that this formulation is equivalent to, but has a slightly simpler metatheory than, the $\mathrm{cases}$ form given in your article.

   This comment is invalid XML; displaying source. Dear Zhen Lin,<br /><br />In programming languages research (closely connected to, but not quite the same as, type theory) $\mathrm{case}$ is the usual name of the finite sum type. However, the dependent sum type is usually given a projective elimination:<br /><br /><img src="https://nforum.ncatlab.org/extensions//vLaTeX/cache/latex_e347ec5f74fb4fb8e72ac63ece801330.png" title="\begin{matrix}<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_1(t) \;:\; A}<br />\\<br />\\<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]}<br />\end{matrix}<br />" style="vertical-align:-20%;" class="tex" alt="\begin{matrix}<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_1(t) \;:\; A}<br />\\<br />\\<br />\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}<br /> {\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]}<br />\end{matrix}<br />" /><br /><br />My understanding is that this formulation is equivalent to, but has a slightly simpler metatheory than, the $\mathrm{cases}$ form given in your article.
3. • CommentRowNumber3.
   • CommentAuthorNeel Krishnaswami
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: Neel Krishnaswami
   Format: TextThis comment worked in the preview...?

   This comment worked in the preview...?
4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeSep 9th 2011
   • (edited Sep 9th 2011)
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHere's Neel's comment: > Dear Zhen Lin, > In programming languages research (closely connected to, but not quite the same as, type theory) $\mathrm{case}$ is the usual name of the finite sum type. However, the dependent sum type is usually given a projective elimination: >$$\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}{\Gamma \;\vdash\; \pi_1(t) \;:\; A}$$ >   >$$\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}{\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]}$$ > My understanding is that this formulation is equivalent to, but has a slightly simpler metatheory than, the $\mathrm{cases}$ form given in your article.

   Here’s Neel’s comment:

   Dear Zhen Lin,

   In programming languages research (closely connected to, but not quite the same as, type theory) $\mathrm{case}$ is the usual name of the finite sum type. However, the dependent sum type is usually given a projective elimination:

   $$\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}{\Gamma \;\vdash\; \pi_1(t) \;:\; A}$$

    

   $$\frac{\Gamma \;\vdash\; t \;:\; \Sigma a:A.\,B}{\Gamma \;\vdash\; \pi_2(t) \;:\; B[\pi_1(t)/a]}$$

   My understanding is that this formulation is equivalent to, but has a slightly simpler metatheory than, the $\mathrm{cases}$ form given in your article.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex@Zhen: Thanks!! I added the unit and empty types, which Martin-Lof obtains as special cases of finite types, and added a remark about how to get the other finite types from those. I also added some links and some comments about identity types and AC. Finally, I changed your remark about *ex falso quodlibet* to refer to [[excluded middle]], since *ex falso* is just the eliminator of the empty type (Martin-Lof actually mentions this in the reference, when he gives the $\bot$-elimination rule). There are, of course, more type constructors in Martin-Lof's paper than you've given here: he describes natural numbers, lists, W-types, and universes. Did you plan to expand this article to include those, and possibly more general inductive types and families? I'm not entirely sure exactly what collection of type-formers is officially called "Martin-Lof type theory". @Neel: I suspect that Zhen wanted to stay close to the choices made in Martin-Lof's original paper, where he uses the "cases" eliminator for dependent sums. I don't have a problem with using the same name for the eliminators of binary sums and dependent sums, since both are after all special cases of inductive types. @Zhen and Neel: I think math tends to give the best results on the forum if you use the "Markdown+Itex" filter.

   @Zhen: Thanks!! I added the unit and empty types, which Martin-Lof obtains as special cases of finite types, and added a remark about how to get the other finite types from those. I also added some links and some comments about identity types and AC. Finally, I changed your remark about ex falso quodlibet to refer to excluded middle, since ex falso is just the eliminator of the empty type (Martin-Lof actually mentions this in the reference, when he gives the $\bot$-elimination rule).

   There are, of course, more type constructors in Martin-Lof’s paper than you’ve given here: he describes natural numbers, lists, W-types, and universes. Did you plan to expand this article to include those, and possibly more general inductive types and families? I’m not entirely sure exactly what collection of type-formers is officially called “Martin-Lof type theory”.

   @Neel: I suspect that Zhen wanted to stay close to the choices made in Martin-Lof’s original paper, where he uses the “cases” eliminator for dependent sums. I don’t have a problem with using the same name for the eliminators of binary sums and dependent sums, since both are after all special cases of inductive types.

   @Zhen and Neel: I think math tends to give the best results on the forum if you use the “Markdown+Itex” filter.

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThere is an important difference between eliminating sum types through cases and eliminating them through projections. (This difference disappears in the presence of identity types, however, so possibly only I care about it.) This is analogous to the difference between the inductive types in Thierry Coquand's Calculus of Inductive Constructions (perhaps best known through its implementation in the theorem prover Coq) and Martin-Löf's $W$-types (although the equivalence between these is more complicated). Categorially, at least when restricted to a sum of a constant family, the difference is that between a [[copower]] (a kind of colimit, elimination through cases) and a [[product]] (a kind of limit, elimination through the projection operators of the cone).

   There is an important difference between eliminating sum types through cases and eliminating them through projections. (This difference disappears in the presence of identity types, however, so possibly only I care about it.) This is analogous to the difference between the inductive types in Thierry Coquand’s Calculus of Inductive Constructions (perhaps best known through its implementation in the theorem prover Coq) and Martin-Löf’s $W$-types (although the equivalence between these is more complicated).

   Categorially, at least when restricted to a sum of a constant family, the difference is that between a copower (a kind of colimit, elimination through cases) and a product (a kind of limit, elimination through the projection operators of the cone).

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeSep 9th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex@Toby: I care about that too. I've gathered that it matters in syntactic study of type theory as well, e.g. the theory of "logical relations" has to treat the two cases differently (maybe one is called "positive" and the other "negative", though I can never remember which is which). Maybe that is part of the "metatheory" Neel was referring to. I thought that Martin-Lof's W-types were literally a special case of CiC's inductive types, though — why do you say that that difference is analogous?

   @Toby: I care about that too. I’ve gathered that it matters in syntactic study of type theory as well, e.g. the theory of “logical relations” has to treat the two cases differently (maybe one is called “positive” and the other “negative”, though I can never remember which is which). Maybe that is part of the “metatheory” Neel was referring to.

   I thought that Martin-Lof’s W-types were literally a special case of CiC’s inductive types, though — why do you say that that difference is analogous?

8. • CommentRowNumber8.
   • CommentAuthorZhen Lin
   • CommentTimeSep 10th 2011
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItex@Mike: > Is that (reflexivity, symmetry, and transitivity) a rule we are giving, or an assertion we are making about derivability? Hmmm. I'm not very sure. I believe it is derivable for the equality judgement in the presence of substitution rules (which I have omitted). On the other hand, in Maietti's 2005 paper, _Modular correspondence between dependent type theories and categories including pretopoi and topoi_, she says > [...] we need to add all the inference rules that express the reflexivity, symmetry and transitivity of the equality between types and terms [...] The structural rules of weakening, substitution and of a suitable exchange are not added since they are derivable. This is also the approach taken by Nordström, Petersson and Smith in their article _Martin-Löf's type theory_. So perhaps it's a matter of taste? As for distinguishing between the equality type and equality judgement, I must defer to the expertise of others here; I thought it might be neater to get rid of the equality judgement given that ‘$I(A, a, b) \; \mathrm{true}$ _is_ a judgement, which will turn out to be equivalent to $a = b \in A$’, according to Martin-Löf [1984]. @Neel, @Toby: Maietti [2005] states, > [...] we will refer to an equivalent formulation of the lex calculus in which the elimination and conversion rules for the indexed sum type are replaced by projections satisfying $\beta$ and $\eta$ conversions. This formulation with projections is equivalent to that of the indexed sum type given previously, but only because of the presence of the extension equality type (see Martin-Löf (1984) for a proof of the equivalence), that is, the equivalence does not hold in the intensional version of Martin-Löf's type theory [...] Question: Why do we demand that the (extensional) equality type has at most one canonical inhabitant? This seems to be one of the differences between the equality type and the (intensional) identity type.

   @Mike:

   Is that (reflexivity, symmetry, and transitivity) a rule we are giving, or an assertion we are making about derivability?

   Hmmm. I’m not very sure. I believe it is derivable for the equality judgement in the presence of substitution rules (which I have omitted). On the other hand, in Maietti’s 2005 paper, Modular correspondence between dependent type theories and categories including pretopoi and topoi, she says

   […] we need to add all the inference rules that express the reflexivity, symmetry and transitivity of the equality between types and terms […] The structural rules of weakening, substitution and of a suitable exchange are not added since they are derivable.

   This is also the approach taken by Nordström, Petersson and Smith in their article Martin-Löf’s type theory. So perhaps it’s a matter of taste? As for distinguishing between the equality type and equality judgement, I must defer to the expertise of others here; I thought it might be neater to get rid of the equality judgement given that ‘$I(A, a, b) \; \mathrm{true}$ is a judgement, which will turn out to be equivalent to $a = b \in A$’, according to Martin-Löf [1984].

   @Neel, @Toby:

   Maietti [2005] states,

   […] we will refer to an equivalent formulation of the lex calculus in which the elimination and conversion rules for the indexed sum type are replaced by projections satisfying $\beta$ and $\eta$ conversions. This formulation with projections is equivalent to that of the indexed sum type given previously, but only because of the presence of the extension equality type (see Martin-Löf (1984) for a proof of the equivalence), that is, the equivalence does not hold in the intensional version of Martin-Löf’s type theory […]

   Question: Why do we demand that the (extensional) equality type has at most one canonical inhabitant? This seems to be one of the differences between the equality type and the (intensional) identity type.

9. • CommentRowNumber9.
   • CommentAuthorTobyBartels
   • CommentTimeSep 10th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex>I thought that Martin-Lof's W-types were literally a special case of CiC's inductive types, though — why do you say that that difference is analogous? That is true; in fact, identity types and dependents sums are both themselves examples of CiC inductive types, and for that matter so is everything else other than dependent products. But I meant to focus only on those CiC inductive types that correspond directly to $W$-types. On the other hand, I think that it was too strong to say that this is analogous. The elimination rule for all CiC inductive types is basically the same; they're *all* eliminated by case analysis on the constructors, and Martin-Löf's $W$-type elimination rule is different, and correct only via using the identity types. However, it's not really analogous to elimination by projection, so the analogy falls apart there.

   I thought that Martin-Lof’s W-types were literally a special case of CiC’s inductive types, though — why do you say that that difference is analogous?

   That is true; in fact, identity types and dependents sums are both themselves examples of CiC inductive types, and for that matter so is everything else other than dependent products. But I meant to focus only on those CiC inductive types that correspond directly to $W$-types.

   On the other hand, I think that it was too strong to say that this is analogous. The elimination rule for all CiC inductive types is basically the same; they’re all eliminated by case analysis on the constructors, and Martin-Löf’s $W$-type elimination rule is different, and correct only via using the identity types. However, it’s not really analogous to elimination by projection, so the analogy falls apart there.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeSep 10th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>This formulation with projections is equivalent to that of the indexed sum type given previously, but only because of the presence of the extension equality type (see Martin-Löf (1984) for a proof of the equivalence), that is, the equivalence does not hold in the intensional version of Martin-Löf's type theory That seems too strong to me; I'll have to review the equivalence, which I thought worked even in the intensional version. >Why do we demand that the (extensional) equality type has at most one canonical inhabitant? Because we're not doing [[homotopy type theory]], I guess!

    This formulation with projections is equivalent to that of the indexed sum type given previously, but only because of the presence of the extension equality type (see Martin-Löf (1984) for a proof of the equivalence), that is, the equivalence does not hold in the intensional version of Martin-Löf’s type theory

    That seems too strong to me; I’ll have to review the equivalence, which I thought worked even in the intensional version.

    Why do we demand that the (extensional) equality type has at most one canonical inhabitant?

    Because we’re not doing homotopy type theory, I guess!

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011
    • (edited Sep 10th 2011)
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHere's what Martin-Lof gives as the W-elimination rule (p44 in my copy, p81 in the Bibliopolis version). I'll write $W$ for the W-type defined from a dependent type $x\colon A \vdash B(x)\colon Type$, which Martin-Lof writes as $(\mathcal{W}x\in A)B(x)$, and sup for the constructor $x\colon A, y\colon B(x) \to W \vdash sup(x,y) \colon W$. Here C is a type dependent on W. $$\frac{\vdash c \colon W \qquad x\colon A, y\colon B(x) \to W, z\colon \Pi_{v\colon B(x)} C(y(v)) \vdash d(x,y,z)\colon C(sup(x,y)) }{ something \colon C(c) }$$ Here's some Coq: Parameter A : Type. Parameter B : A -> Type. Inductive W : Type := | sup : forall a:A, (B a -> W) -> W. Check W_rect. which prints forall P : W -> Type, (forall (a : A) (w : B a -> W), (forall b : B a, P (w b)) -> P (sup a w)) -> forall w : W, P w from which, applying some alpha-equivalence, we get forall C : W -> Type, (forall (x : A) (y : B x -> W), (forall v : B x, C (y v)) -> C (sup x y)) -> forall c : W, C c which looks the same as Martin-Lof's eliminator to me.

    Here’s what Martin-Lof gives as the W-elimination rule (p44 in my copy, p81 in the Bibliopolis version). I’ll write $W$ for the W-type defined from a dependent type $x\colon A \vdash B(x)\colon Type$, which Martin-Lof writes as $(\mathcal{W}x\in A)B(x)$, and sup for the constructor $x\colon A, y\colon B(x) \to W \vdash sup(x,y) \colon W$. Here C is a type dependent on W.

    $$\frac{\vdash c \colon W \qquad x\colon A, y\colon B(x) \to W, z\colon \Pi_{v\colon B(x)} C(y(v)) \vdash d(x,y,z)\colon C(sup(x,y)) }{ something \colon C(c) }$$

    Here’s some Coq:

    Parameter A : Type.
    Parameter B : A -> Type.
    
    Inductive W : Type :=
    | sup : forall a:A, (B a -> W) -> W.
    
    Check W_rect.
    

    which prints

    forall P : W -> Type,
      (forall (a : A) (w : B a -> W),
        (forall b : B a, P (w b)) -> P (sup a w)) -> 
      forall w : W, P w
    

    from which, applying some alpha-equivalence, we get

    forall C : W -> Type,
      (forall (x : A) (y : B x -> W),
        (forall v : B x, C (y v)) -> C (sup x y)) -> 
      forall c : W, C c
    

    which looks the same as Martin-Lof’s eliminator to me.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> Why do we demand that the (extensional) equality type has at most one canonical inhabitant? I would say that's more or less the definition of "extensional".

    Why do we demand that the (extensional) equality type has at most one canonical inhabitant?

    I would say that’s more or less the definition of “extensional”.

13. • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeSep 10th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexSorry, Mike, that's my faulty memory. It's not the $W$-types per se, but those $W$-types that CiC can implement *without* thinking of them *as* $W$-types (that is, without having a constructor with "->" in it). For example, to construct $\mathbb{N}$ (if you don't already have it by hand) as a $W$-type, you take (following your notation above) $A$ to be $1 + 1$ and $B$ to be defined by cases, first $0$ and next $1$. So the eliminator is $$ \frac {\vdash c\colon \mathbb{N}; \qquad x\colon 1 + 1, y\colon B(x) \to \mathbb{N}, z\colon \Pi_{v\colon B(x)} C(y(v)) \vdash d(x,y,z)\colon C(sup(x,y)) } { something \colon C(c) } .$$ But a much simpler eliminator is $$ \frac {\vdash c\colon \mathbb{N}; \qquad d\colon C(0); \qquad y\colon \mathbb{N} \vdash e(y)\colon C(y^+) } { something \colon C(c) } .$$ And now I see no clear analogy, except this: I want to think of the latter eliminator as correct, and (IIRC) we need identity types to prove them equivalent. I should probably look at this in more detail, lest more of my memory be wrong.

    Sorry, Mike, that’s my faulty memory. It’s not the $W$-types per se, but those $W$-types that CiC can implement without thinking of them as $W$-types (that is, without having a constructor with “->” in it).

    For example, to construct $\mathbb{N}$ (if you don’t already have it by hand) as a $W$-type, you take (following your notation above) $A$ to be $1 + 1$ and $B$ to be defined by cases, first $0$ and next $1$. So the eliminator is

    $$\frac {\vdash c\colon \mathbb{N}; \qquad x\colon 1 + 1, y\colon B(x) \to \mathbb{N}, z\colon \Pi_{v\colon B(x)} C(y(v)) \vdash d(x,y,z)\colon C(sup(x,y)) } { something \colon C(c) } .$$

    But a much simpler eliminator is

    $$\frac {\vdash c\colon \mathbb{N}; \qquad d\colon C(0); \qquad y\colon \mathbb{N} \vdash e(y)\colon C(y^+) } { something \colon C(c) } .$$

    And now I see no clear analogy, except this: I want to think of the latter eliminator as correct, and (IIRC) we need identity types to prove them equivalent.

    I should probably look at this in more detail, lest more of my memory be wrong.

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexToby: Ah, yes, I see. I didn't realize you needed identity types for that equivalence. I just tried messing around in Coq, and I was able to prove without using equality that the CiC eliminator implies the W-type eliminator. But I couldn't see how to do the other direction without assuming not just identity types but function extensionality! Gee, that's bothersome. If that's correct, it makes me much less happy about W-types. Maybe we ought to consider initial joint-algebras for finite families of polynomial endofunctors all the time instead.

    Toby: Ah, yes, I see. I didn’t realize you needed identity types for that equivalence. I just tried messing around in Coq, and I was able to prove without using equality that the CiC eliminator implies the W-type eliminator. But I couldn’t see how to do the other direction without assuming not just identity types but function extensionality!

    Gee, that’s bothersome. If that’s correct, it makes me much less happy about W-types. Maybe we ought to consider initial joint-algebras for finite families of polynomial endofunctors all the time instead.

15. • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeSep 11th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>without assuming not just identity types but function extensionality That fits with the quotation from Maietti above, even though I didn't remember the need for extensionality.

    without assuming not just identity types but function extensionality

    That fits with the quotation from Maietti above, even though I didn’t remember the need for extensionality.

16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have edited the sub-section structure at [[Martin-Löf dependent type theory]]. Originally the section "Equality type" had lots of subsections, which I think was unintentional. Also I created a Properties-subsection, made "Axiom of choise" be subordinate to that and created a new subordinate section "Models" with a very brief remark on models for the extensional and the intensional version. Finally I added in the References a pointer to chapter 1 in Michael Warren's PhD thesis, which I am finding a useful text to read.

    I have edited the sub-section structure at Martin-Löf dependent type theory. Originally the section “Equality type” had lots of subsections, which I think was unintentional.

    Also I created a Properties-subsection, made “Axiom of choise” be subordinate to that and created a new subordinate section “Models” with a very brief remark on models for the extensional and the intensional version.

    Finally I added in the References a pointer to chapter 1 in Michael Warren’s PhD thesis, which I am finding a useful text to read.