-
Notifications
You must be signed in to change notification settings - Fork 10
Get rid of need for explicit ubiquitous fuel pattern #7
Copy link
Copy link
Open
Labels
code: redesignNew design of some part of the libraryNew design of some part of the librarypart: derivationRelated to automated derivation of generatorsRelated to automated derivation of generatorspart: generatorsRelated to generatorsRelated to generatorsstatus: discussionSuggested or reported thing is not obvious to be good enoughSuggested or reported thing is not obvious to be good enoughstatus: feature requestRequest for new functionality or improvementRequest for new functionality or improvement
Metadata
Metadata
Assignees
Labels
code: redesignNew design of some part of the libraryNew design of some part of the librarypart: derivationRelated to automated derivation of generatorsRelated to automated derivation of generatorspart: generatorsRelated to generatorsRelated to generatorsstatus: discussionSuggested or reported thing is not obvious to be good enoughSuggested or reported thing is not obvious to be good enoughstatus: feature requestRequest for new functionality or improvementRequest for new functionality or improvement
Current generators of type
Genare explicitly finite. Thus, when we define recursive generators, we use fuel pattern everywhere, especially in derived generators. Actually, for simplicity, we use it always for derived generators, even when it is actually not needed.By the way, using
Fuel -> Gen ...instead of justGen ..., we run into problems in the compiler, e.g. idris-lang/Idris2#2522We could have a possibly-infinite generators using co-data inside and to provide fuel only at the end of the day, when producing particular values.
We need to decide whether this is useful to have a distinction between definitely finite and possibly infinite generators, or not. This distinction makes it easier to run finite generators (no fuel required) but makes generators combinations and derivation more complex.