What should we return when pattern matching on a Higher Indutive Type and the case is a Path?












1












$begingroup$


Context: Cubical Type Theory



Consider a simple HIT, say, an HitInt:



data HitInt : Set where
pos : (n : ℕ) → HitInt
neg : (n : ℕ) → HitInt
posneg : pos 0 ≡ neg 0


Or, if you don't speak Agda we can use cubicaltt:



data int = pos (n : nat)
| neg (n : nat)
| zeroP <i> [ (i = 0) -> pos zero
, (i = 1) -> neg zero ]


We want to define, for instance, a succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:



sucHitInt : HitInt → HitInt
sucHitInt (pos n) = pos (suc n)
sucHitInt (neg zero) = pos 1
sucHitInt (neg (suc n)) = neg n
sucHitInt (posneg x) = pos 1


Or in cubicaltt:



sucInt : int -> int = split
pos n -> pos (suc n)
neg n -> sucNat n
where sucNat : nat -> int = split
zero -> pos one
suc n -> neg n
zeroP @ i -> pos one


What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input Path".



My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a Path like <i> pos 1 (even this is not a member of the higher inductive family)?



What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.










share|cite|improve this question











$endgroup$

















    1












    $begingroup$


    Context: Cubical Type Theory



    Consider a simple HIT, say, an HitInt:



    data HitInt : Set where
    pos : (n : ℕ) → HitInt
    neg : (n : ℕ) → HitInt
    posneg : pos 0 ≡ neg 0


    Or, if you don't speak Agda we can use cubicaltt:



    data int = pos (n : nat)
    | neg (n : nat)
    | zeroP <i> [ (i = 0) -> pos zero
    , (i = 1) -> neg zero ]


    We want to define, for instance, a succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:



    sucHitInt : HitInt → HitInt
    sucHitInt (pos n) = pos (suc n)
    sucHitInt (neg zero) = pos 1
    sucHitInt (neg (suc n)) = neg n
    sucHitInt (posneg x) = pos 1


    Or in cubicaltt:



    sucInt : int -> int = split
    pos n -> pos (suc n)
    neg n -> sucNat n
    where sucNat : nat -> int = split
    zero -> pos one
    suc n -> neg n
    zeroP @ i -> pos one


    What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input Path".



    My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a Path like <i> pos 1 (even this is not a member of the higher inductive family)?



    What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.










    share|cite|improve this question











    $endgroup$















      1












      1








      1


      1



      $begingroup$


      Context: Cubical Type Theory



      Consider a simple HIT, say, an HitInt:



      data HitInt : Set where
      pos : (n : ℕ) → HitInt
      neg : (n : ℕ) → HitInt
      posneg : pos 0 ≡ neg 0


      Or, if you don't speak Agda we can use cubicaltt:



      data int = pos (n : nat)
      | neg (n : nat)
      | zeroP <i> [ (i = 0) -> pos zero
      , (i = 1) -> neg zero ]


      We want to define, for instance, a succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:



      sucHitInt : HitInt → HitInt
      sucHitInt (pos n) = pos (suc n)
      sucHitInt (neg zero) = pos 1
      sucHitInt (neg (suc n)) = neg n
      sucHitInt (posneg x) = pos 1


      Or in cubicaltt:



      sucInt : int -> int = split
      pos n -> pos (suc n)
      neg n -> sucNat n
      where sucNat : nat -> int = split
      zero -> pos one
      suc n -> neg n
      zeroP @ i -> pos one


      What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input Path".



      My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a Path like <i> pos 1 (even this is not a member of the higher inductive family)?



      What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.










      share|cite|improve this question











      $endgroup$




      Context: Cubical Type Theory



      Consider a simple HIT, say, an HitInt:



      data HitInt : Set where
      pos : (n : ℕ) → HitInt
      neg : (n : ℕ) → HitInt
      posneg : pos 0 ≡ neg 0


      Or, if you don't speak Agda we can use cubicaltt:



      data int = pos (n : nat)
      | neg (n : nat)
      | zeroP <i> [ (i = 0) -> pos zero
      , (i = 1) -> neg zero ]


      We want to define, for instance, a succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:



      sucHitInt : HitInt → HitInt
      sucHitInt (pos n) = pos (suc n)
      sucHitInt (neg zero) = pos 1
      sucHitInt (neg (suc n)) = neg n
      sucHitInt (posneg x) = pos 1


      Or in cubicaltt:



      sucInt : int -> int = split
      pos n -> pos (suc n)
      neg n -> sucNat n
      where sucNat : nat -> int = split
      zero -> pos one
      suc n -> neg n
      zeroP @ i -> pos one


      What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input Path".



      My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a Path like <i> pos 1 (even this is not a member of the higher inductive family)?



      What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.







      type-theory homotopy-type-theory higher-inductive-types cubical-type-theory






      share|cite|improve this question















      share|cite|improve this question













      share|cite|improve this question




      share|cite|improve this question








      edited 3 hours ago









      Raphael

      57.5k23139314




      57.5k23139314










      asked 5 hours ago









      ice1000ice1000

      383121




      383121






















          1 Answer
          1






          active

          oldest

          votes


















          3












          $begingroup$


          it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer




          My understanding is that it matches points of path rather than path itself. This is why match is on posneg x (where x : I) rather than posneg itself.



          Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a special of regular constructors, i.e.



            posneg : I ↝ HitInt [i0 ↦ pos 0 ; i1 ↦ neg 0]


          where if you ignore "special" properties of interval, it looks like a regular constructor (in cubicaltt notation it already looks similar except that I is always treated specially).




          What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.




          It's the only way to satisfy constraints imposed by previous definitions (this works for both zero cases). In fact, agda can correctly solve even two holes (in right order):



          sucHitInt : HitInt → HitInt
          sucHitInt (pos n) = pos (suc n)
          sucHitInt (posneg i) = {!!}
          sucHitInt (neg zero) = {!!}
          sucHitInt (neg (suc n)) = neg n



          Why it's not returning a Path like pos 1 (even this is not a member of the higher inductive family)?




          Again, since we're matching on points rather than paths; for symmetry it's possible to imagine that case as equal to:



          sucHitInt (posneg i) = (λ _ → pos 1) i


          reading somewhat like "for all projections from I at i to path posneg we have projections from I at i to constant path (λ _ → pos 1)". This doesn't quite work in Agda, however the following (with the same meaning) does:



          sucHitInt (posneg i) = refl {x = pos 1} i


          PS: i'm new to cubical myself, so hopefully someone can correct or extend my answer






          share|cite|improve this answer








          New contributor




          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.






          $endgroup$













          • $begingroup$
            Yes, thanks for pointing out the interval parameter in the Path constructor! This is very helpful!
            $endgroup$
            – ice1000
            36 mins ago










          • $begingroup$
            By the way, is and used generally as you use them (for path endpoints and abstraction) in type theory?
            $endgroup$
            – ice1000
            34 mins ago










          • $begingroup$
            @ice1000 I chose just as a fancy arrow, i don't know if it was used as such. As for , it's quite commonly used in lambdas and i think i've seen it in such context as well
            $endgroup$
            – caryoscelus
            15 mins ago













          Your Answer





          StackExchange.ifUsing("editor", function () {
          return StackExchange.using("mathjaxEditing", function () {
          StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
          StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
          });
          });
          }, "mathjax-editing");

          StackExchange.ready(function() {
          var channelOptions = {
          tags: "".split(" "),
          id: "419"
          };
          initTagRenderer("".split(" "), "".split(" "), channelOptions);

          StackExchange.using("externalEditor", function() {
          // Have to fire editor after snippets, if snippets enabled
          if (StackExchange.settings.snippets.snippetsEnabled) {
          StackExchange.using("snippets", function() {
          createEditor();
          });
          }
          else {
          createEditor();
          }
          });

          function createEditor() {
          StackExchange.prepareEditor({
          heartbeatType: 'answer',
          autoActivateHeartbeat: false,
          convertImagesToLinks: false,
          noModals: true,
          showLowRepImageUploadWarning: true,
          reputationToPostImages: null,
          bindNavPrevention: true,
          postfix: "",
          imageUploader: {
          brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
          contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
          allowUrls: true
          },
          onDemand: true,
          discardSelector: ".discard-answer"
          ,immediatelyShowMarkdownHelp:true
          });


          }
          });














          draft saved

          draft discarded


















          StackExchange.ready(
          function () {
          StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f103146%2fwhat-should-we-return-when-pattern-matching-on-a-higher-indutive-type-and-the-ca%23new-answer', 'question_page');
          }
          );

          Post as a guest















          Required, but never shown

























          1 Answer
          1






          active

          oldest

          votes








          1 Answer
          1






          active

          oldest

          votes









          active

          oldest

          votes






          active

          oldest

          votes









          3












          $begingroup$


          it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer




          My understanding is that it matches points of path rather than path itself. This is why match is on posneg x (where x : I) rather than posneg itself.



          Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a special of regular constructors, i.e.



            posneg : I ↝ HitInt [i0 ↦ pos 0 ; i1 ↦ neg 0]


          where if you ignore "special" properties of interval, it looks like a regular constructor (in cubicaltt notation it already looks similar except that I is always treated specially).




          What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.




          It's the only way to satisfy constraints imposed by previous definitions (this works for both zero cases). In fact, agda can correctly solve even two holes (in right order):



          sucHitInt : HitInt → HitInt
          sucHitInt (pos n) = pos (suc n)
          sucHitInt (posneg i) = {!!}
          sucHitInt (neg zero) = {!!}
          sucHitInt (neg (suc n)) = neg n



          Why it's not returning a Path like pos 1 (even this is not a member of the higher inductive family)?




          Again, since we're matching on points rather than paths; for symmetry it's possible to imagine that case as equal to:



          sucHitInt (posneg i) = (λ _ → pos 1) i


          reading somewhat like "for all projections from I at i to path posneg we have projections from I at i to constant path (λ _ → pos 1)". This doesn't quite work in Agda, however the following (with the same meaning) does:



          sucHitInt (posneg i) = refl {x = pos 1} i


          PS: i'm new to cubical myself, so hopefully someone can correct or extend my answer






          share|cite|improve this answer








          New contributor




          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.






          $endgroup$













          • $begingroup$
            Yes, thanks for pointing out the interval parameter in the Path constructor! This is very helpful!
            $endgroup$
            – ice1000
            36 mins ago










          • $begingroup$
            By the way, is and used generally as you use them (for path endpoints and abstraction) in type theory?
            $endgroup$
            – ice1000
            34 mins ago










          • $begingroup$
            @ice1000 I chose just as a fancy arrow, i don't know if it was used as such. As for , it's quite commonly used in lambdas and i think i've seen it in such context as well
            $endgroup$
            – caryoscelus
            15 mins ago


















          3












          $begingroup$


          it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer




          My understanding is that it matches points of path rather than path itself. This is why match is on posneg x (where x : I) rather than posneg itself.



          Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a special of regular constructors, i.e.



            posneg : I ↝ HitInt [i0 ↦ pos 0 ; i1 ↦ neg 0]


          where if you ignore "special" properties of interval, it looks like a regular constructor (in cubicaltt notation it already looks similar except that I is always treated specially).




          What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.




          It's the only way to satisfy constraints imposed by previous definitions (this works for both zero cases). In fact, agda can correctly solve even two holes (in right order):



          sucHitInt : HitInt → HitInt
          sucHitInt (pos n) = pos (suc n)
          sucHitInt (posneg i) = {!!}
          sucHitInt (neg zero) = {!!}
          sucHitInt (neg (suc n)) = neg n



          Why it's not returning a Path like pos 1 (even this is not a member of the higher inductive family)?




          Again, since we're matching on points rather than paths; for symmetry it's possible to imagine that case as equal to:



          sucHitInt (posneg i) = (λ _ → pos 1) i


          reading somewhat like "for all projections from I at i to path posneg we have projections from I at i to constant path (λ _ → pos 1)". This doesn't quite work in Agda, however the following (with the same meaning) does:



          sucHitInt (posneg i) = refl {x = pos 1} i


          PS: i'm new to cubical myself, so hopefully someone can correct or extend my answer






          share|cite|improve this answer








          New contributor




          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.






          $endgroup$













          • $begingroup$
            Yes, thanks for pointing out the interval parameter in the Path constructor! This is very helpful!
            $endgroup$
            – ice1000
            36 mins ago










          • $begingroup$
            By the way, is and used generally as you use them (for path endpoints and abstraction) in type theory?
            $endgroup$
            – ice1000
            34 mins ago










          • $begingroup$
            @ice1000 I chose just as a fancy arrow, i don't know if it was used as such. As for , it's quite commonly used in lambdas and i think i've seen it in such context as well
            $endgroup$
            – caryoscelus
            15 mins ago
















          3












          3








          3





          $begingroup$


          it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer




          My understanding is that it matches points of path rather than path itself. This is why match is on posneg x (where x : I) rather than posneg itself.



          Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a special of regular constructors, i.e.



            posneg : I ↝ HitInt [i0 ↦ pos 0 ; i1 ↦ neg 0]


          where if you ignore "special" properties of interval, it looks like a regular constructor (in cubicaltt notation it already looks similar except that I is always treated specially).




          What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.




          It's the only way to satisfy constraints imposed by previous definitions (this works for both zero cases). In fact, agda can correctly solve even two holes (in right order):



          sucHitInt : HitInt → HitInt
          sucHitInt (pos n) = pos (suc n)
          sucHitInt (posneg i) = {!!}
          sucHitInt (neg zero) = {!!}
          sucHitInt (neg (suc n)) = neg n



          Why it's not returning a Path like pos 1 (even this is not a member of the higher inductive family)?




          Again, since we're matching on points rather than paths; for symmetry it's possible to imagine that case as equal to:



          sucHitInt (posneg i) = (λ _ → pos 1) i


          reading somewhat like "for all projections from I at i to path posneg we have projections from I at i to constant path (λ _ → pos 1)". This doesn't quite work in Agda, however the following (with the same meaning) does:



          sucHitInt (posneg i) = refl {x = pos 1} i


          PS: i'm new to cubical myself, so hopefully someone can correct or extend my answer






          share|cite|improve this answer








          New contributor




          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.






          $endgroup$




          it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer




          My understanding is that it matches points of path rather than path itself. This is why match is on posneg x (where x : I) rather than posneg itself.



          Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a special of regular constructors, i.e.



            posneg : I ↝ HitInt [i0 ↦ pos 0 ; i1 ↦ neg 0]


          where if you ignore "special" properties of interval, it looks like a regular constructor (in cubicaltt notation it already looks similar except that I is always treated specially).




          What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.




          It's the only way to satisfy constraints imposed by previous definitions (this works for both zero cases). In fact, agda can correctly solve even two holes (in right order):



          sucHitInt : HitInt → HitInt
          sucHitInt (pos n) = pos (suc n)
          sucHitInt (posneg i) = {!!}
          sucHitInt (neg zero) = {!!}
          sucHitInt (neg (suc n)) = neg n



          Why it's not returning a Path like pos 1 (even this is not a member of the higher inductive family)?




          Again, since we're matching on points rather than paths; for symmetry it's possible to imagine that case as equal to:



          sucHitInt (posneg i) = (λ _ → pos 1) i


          reading somewhat like "for all projections from I at i to path posneg we have projections from I at i to constant path (λ _ → pos 1)". This doesn't quite work in Agda, however the following (with the same meaning) does:



          sucHitInt (posneg i) = refl {x = pos 1} i


          PS: i'm new to cubical myself, so hopefully someone can correct or extend my answer







          share|cite|improve this answer








          New contributor




          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.









          share|cite|improve this answer



          share|cite|improve this answer






          New contributor




          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.









          answered 4 hours ago









          caryosceluscaryoscelus

          462




          462




          New contributor




          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.





          New contributor





          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.






          caryoscelus is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
          Check out our Code of Conduct.












          • $begingroup$
            Yes, thanks for pointing out the interval parameter in the Path constructor! This is very helpful!
            $endgroup$
            – ice1000
            36 mins ago










          • $begingroup$
            By the way, is and used generally as you use them (for path endpoints and abstraction) in type theory?
            $endgroup$
            – ice1000
            34 mins ago










          • $begingroup$
            @ice1000 I chose just as a fancy arrow, i don't know if it was used as such. As for , it's quite commonly used in lambdas and i think i've seen it in such context as well
            $endgroup$
            – caryoscelus
            15 mins ago




















          • $begingroup$
            Yes, thanks for pointing out the interval parameter in the Path constructor! This is very helpful!
            $endgroup$
            – ice1000
            36 mins ago










          • $begingroup$
            By the way, is and used generally as you use them (for path endpoints and abstraction) in type theory?
            $endgroup$
            – ice1000
            34 mins ago










          • $begingroup$
            @ice1000 I chose just as a fancy arrow, i don't know if it was used as such. As for , it's quite commonly used in lambdas and i think i've seen it in such context as well
            $endgroup$
            – caryoscelus
            15 mins ago


















          $begingroup$
          Yes, thanks for pointing out the interval parameter in the Path constructor! This is very helpful!
          $endgroup$
          – ice1000
          36 mins ago




          $begingroup$
          Yes, thanks for pointing out the interval parameter in the Path constructor! This is very helpful!
          $endgroup$
          – ice1000
          36 mins ago












          $begingroup$
          By the way, is and used generally as you use them (for path endpoints and abstraction) in type theory?
          $endgroup$
          – ice1000
          34 mins ago




          $begingroup$
          By the way, is and used generally as you use them (for path endpoints and abstraction) in type theory?
          $endgroup$
          – ice1000
          34 mins ago












          $begingroup$
          @ice1000 I chose just as a fancy arrow, i don't know if it was used as such. As for , it's quite commonly used in lambdas and i think i've seen it in such context as well
          $endgroup$
          – caryoscelus
          15 mins ago






          $begingroup$
          @ice1000 I chose just as a fancy arrow, i don't know if it was used as such. As for , it's quite commonly used in lambdas and i think i've seen it in such context as well
          $endgroup$
          – caryoscelus
          15 mins ago




















          draft saved

          draft discarded




















































          Thanks for contributing an answer to Computer Science Stack Exchange!


          • Please be sure to answer the question. Provide details and share your research!

          But avoid



          • Asking for help, clarification, or responding to other answers.

          • Making statements based on opinion; back them up with references or personal experience.


          Use MathJax to format equations. MathJax reference.


          To learn more, see our tips on writing great answers.




          draft saved


          draft discarded














          StackExchange.ready(
          function () {
          StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f103146%2fwhat-should-we-return-when-pattern-matching-on-a-higher-indutive-type-and-the-ca%23new-answer', 'question_page');
          }
          );

          Post as a guest















          Required, but never shown





















































          Required, but never shown














          Required, but never shown












          Required, but never shown







          Required, but never shown

































          Required, but never shown














          Required, but never shown












          Required, but never shown







          Required, but never shown







          Popular posts from this blog

          How to make a Squid Proxy server?

          Is this a new Fibonacci Identity?

          Touch on Surface Book