Comments (5)
Note: I have not yet convinced myself that the subst
operation for dependent tactic trees actually obeys the (relative) monad laws. I hope it does, or if it doesn't, can be replaced with something that does.
from sml-dependent-lcf.
So I've been thinking about adding relative monads to the groupoids library but haven't gotten around to it yet. We have monads now: here (see all the stuff above it for the context).
The way I was planning to do it was to define skew monoidal categories either as a separate structure or by modifying Monoidal
to support both. However, in order to get the Kleisli extensions (bind) we also need a Closed
structure (as in this) or some combined closed monoidal thing or just a direct formalization of extension systems. Should be pretty straightforward to do any of that, just a bit tedious.
The skew monoidal structures are essentially like the monoidal ones except the operations are only natural, not natural iso, if I remember right. Then you would define skew monoids on some functor, not necessarily on Endo
. Uustalu describes the construction in one of his papers.
The category of containers (and of polynomials) is also something I was thinking about. The reason I added the fibration stuff recently was to be able to work with signatures and constructions on them as (lax monoidal) fibrations which is how some of the opetope stuff is described in the literature. I think it would be nicer to work with pseudofunctors and indexed monoidal categories for that but it would be good to have both approaches available.
from sml-dependent-lcf.
FYI: the current code does not seem to compile under the development version of Agda, no matter I update the agda-prelude or not. I would actually suggest move the modeling to another repository because the testing needed for Agda code is very different from the main SML code.
from sml-dependent-lcf.
@favonia I tend to keep little Agda sketches sometimes in the repository, without any expectation that it be tested or even continue to build over time. Probably it is better to delete it for now, as the agda code was written experimentally, as a way to figure out what this proof refinement structure should look like.
from sml-dependent-lcf.
(The agda sketch is superseded by this paper: https://arxiv.org/abs/1703.05215)
from sml-dependent-lcf.
Related Issues (18)
- switch to HOAS? HOT 3
- consider dealing with generic judgment primitively HOT 1
- allow environments to use a different structure from telescopes? HOT 1
- Try making validations just open terms
- correct the monad
- Nominal LCF should be primarily based on "multitactics"
- Is it a bug or a feature that `each`/`thenl` don't check for equal list lengths HOT 2
- Integrate Dependent LCF HOT 1
- Replace example with something non-silly
- implement 'sequential' sequencing
- Add a function to apply a tactic to subgoals within a certain range HOT 3
- Add a tactic that would always fail. HOT 1
- PROGRESS tactical
- Meta information attached to subgoals? HOT 8
- Warning for too many tactics in `[_, _, ..., _]` HOT 1
- Make proof state abstract somehow
- Consider getting rid of backtracking
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 sml-dependent-lcf.