What should we return when pattern matching on a Higher Indutive Type and the case is a Path?
$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.
type-theory homotopy-type-theory higher-inductive-types cubical-type-theory
$endgroup$
add a comment |
$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.
type-theory homotopy-type-theory higher-inductive-types cubical-type-theory
$endgroup$
add a comment |
$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.
type-theory homotopy-type-theory higher-inductive-types cubical-type-theory
$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
type-theory homotopy-type-theory higher-inductive-types cubical-type-theory
edited 3 hours ago
Raphael♦
57.5k23139314
57.5k23139314
asked 5 hours ago
ice1000ice1000
383121
383121
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
$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
New contributor
$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
add a comment |
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
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
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
$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
New contributor
$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
add a comment |
$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
New contributor
$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
add a comment |
$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
New contributor
$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
New contributor
New contributor
answered 4 hours ago
caryosceluscaryoscelus
462
462
New contributor
New contributor
$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
add a comment |
$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
add a comment |
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.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
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
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
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