Comments (4)
Thinking more about this, I have to wonder why I opted to have have chalk "defer" normalization the way that is does (i.e., by producing a new obligation to be solved), rather than just solving it in place (recursively). I've wondered before, but it didn't seem to make much difference. But when you think about the need to track recursion depth, it might make things mildly simpler.
from chalk.
I'm not familiar with how the code currently behaves, but to get me thinking about this and because I want to contribute, here're some bouncy thoughts:
This sounds like something that'd fall out of having a 'progress' measure. If all the atoms (types) are grouped into equivalence classes with each equivalence class having some designated element (e.g. by organizing w/ union-find and doing a union every time a ==
obligation is made) normalizing all types in encountered obligations to the 'minimum' element and 'forgetting' about duplicated obligations, then 'progress' can be measured w.r.t. whether or not 'new' obligations are generated.
The only way for the above to loop indefinitely is if there's an infinitely sized type that doesn't repeat itself. I think that should only happen in pathological cases like someone using the type system to compute π or whatever (and that can then be sort-of-caught by checking the sizes of produced types). Though, then there's no 'recursion limit' per se, one'd need to give a limit to the maximum type size instead.
EDIT: well, okay, union-find wouldn't work because one'd need to map from the members of the set back to the designated member, but the gist of it is still there derp
EDIT EDIT: also I guess it could go infinitely if obligations are allowed to have an arbitrarily large (growing) number of atoms in them, but I don't think that's the case?
from chalk.
@nikomatsakis Is this issue still relevant? It sounds similar to (#234) and (#280). The FIXME
in the code isn't there anymore. Can this issue be closed?
from chalk.
Yeah, I'm going to close this. We may indeed find some problems relating to this underlying pattern in practice, but we may not -- my concern would be that maybe there is something that we are able to type-check if we eagerly normalize (as rustc does) but which produces an "infinite type" if we are lazy. But the best way to find that would be to be converted rustc to a more lazy approach, I think.
from chalk.
Related Issues (20)
- CI Publish job using Mac runner HOT 2
- When Rust 1.55 hits stable, replace `ControlFlow` with std version
- Recursive solver reports ambiguity HOT 7
- Idea: rework how SLG solver uses the environment
- Auto traits are not handled for generic closures HOT 8
- Consider removing unused field
- Clean up coherence chapter in the Chalk book HOT 1
- Ambiguity through unrelated env clauses because of implied bounds HOT 1
- reconcile SLG/recursive solver's attempts to merge multiple results
- book: hard to read mermaid diagram in dark themes
- Lowered command panics with auto trait HOT 1
- Recursive solver hangs on cyclic traits HOT 3
- mdbook-mermaid needs updating
- Unable to deduce projection types of dyn types from supertrait bounds
- ICE: negative subgoal had delayed_subgoals HOT 2
- any progress and roadmap? HOT 1
- Automatic releases have been failing for a couple of months
- Branch protection prevents automatic releases from updating the version number on the `master` branch
- Recursive Solver fails to solve recursive associated type with GAT
- Fails to solve some existential clause HOT 2
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 chalk.