Comments (6)
Agda correctly throws a termination error with --no-forcing
. #4606 is related, but forcing removes the dot from the dot pattern.
Slightly simplified code:
{-# OPTIONS --cubical --safe #-}
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
data ⊥ : Set where
data T : Set where
zero : T
suc : T → T
eq : (x : T) → suc x ≡ x
data IsSuc : T → Set where
is-suc : (x : T) → IsSuc (suc x)
all-sucs : (x : T) → IsSuc x
all-sucs x = primTransp (λ i → IsSuc (eq x i)) i0 (is-suc x)
not-suc : (x : T) → IsSuc x → ⊥
not-suc .(suc x) (is-suc x) = not-suc x (all-sucs x)
nope : ⊥
nope = not-suc zero (all-sucs zero)
from agda.
@szumixie wrote:
but forcing removes the dot from the dot pattern.
Thanks for the analysis!
Should we disable --forcing
for --cubical
and make it unsafe to enable it?
from agda.
Should we disable --forcing for --cubical and make it unsafe to enable it?
That seems like quite a drastic solution to me. Couldn't we rather make it so that forcing does not apply to HITs, but still apply it to regular datatypes?
from agda.
Oh, it's not that easy, since the type that forcing is applied to is not a HIT itself, it only is indexed by a HIT. Rather, what we could do is to change the forcing analysis so it does not detect an argument as being forced if it appears as an argument to a constructor of a HIT.
Basically, we should check here
agda/src/full/Agda/TypeChecking/Forcing.hs
Line 167 in 35b5659
mempty
.from agda.
that the constructor is not a HIT constructor, and if it is return
mempty
.
I could easily implement this.
However, it is not clear to me what is the right thing to do.
Because we have no compiler for cubical, the forcing analysis is a bit hanging in the air, it is not clear what it should achieve.
With K (and T
not being a HIT), IsSuc
would be a proposition and erased during compilation.
In Cubical (and T
as defined), both T
and IsSuc
are contractible (as witnessed by all-sucs
), so, have no content and could be erased (!?).
Maybe nothing is wrong with the forcing analysis, but instead the termination checker should work on the compiled clauses and without K not look into lazy matches for termination witnesses?
from agda.
Because we have no compiler for cubical, the forcing analysis is a bit hanging in the air, it is not clear what it should achieve.
Semantically speaking, the forcing analysis tries to detect constructor arguments that are uniquely determined by the constructor indices. Here, the index suc x
does not uniquely determine the argument x
because suc
is not injective. Hence, in this case the forcing analysis is clearly making a wrong assumption, and my proposed change would fix that.
You seem to be making a more general claim that forcing is something that should not be done at all in case of cubical. However, I'd like to see more evidence for that claim beyond just this single issue.
from agda.
Related Issues (20)
- Normalization gives trivial `transp` HOT 1
- `--postfix-projections` do not make use of mixfix syntax HOT 1
- No warning about useless `{-# CATCHALL #-}` pragma
- HTML backend: inconsistent highlighting for macro names
- Internal error on pattern lambda with no clauses
- wrong type for unnamed record constructor
- Search for project root crashes when (parent) directory lacks permissions HOT 1
- quoteTerm loops on dependent copattern lambda HOT 3
- Caching loses reflection-generated pragmas
- Emacs: Support default value of `agda2-infer-type-maybe-toplevel` from type at point HOT 1
- Literate programming Org/LaTeX feature request
- `--save-metas` causes internal error in `lookupMetaInstantiation` HOT 3
- Consider using `Set` instead of `nub`
- Mimer options `-l` and `-s` not covered by testsuite HOT 2
- The specification of `--safe` misses the pragmas
- MAlonzo bug: `unreachable code reached` HOT 9
- Our error messages do not follow the GNU standard HOT 2
- Agda 2.7.0-rc1 crashes when run twice, probably serialization issue HOT 3
- .cabal description "...: It ..." HOT 4
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda.