feat: add purity annotation #191
Conversation
Next task: add EffectKind.purity into Com.
…into purity-annotation
…s for readability
Since `toType2` is marked as reducible, we don't need to unfold it before using `infer_instance`
There was a problem hiding this comment.
Thanks @alexkeizer and @bollu for the heroic effort here! It's nice that you've also documented things well in this PR. Overall, I'm happy with it. I've left a few comments here that are small to address.
There's a bunch of TODO's introduced by this PR, and it's certainly not worth doing them all right now. It would be nice to have maybe an issue tracking the cleanup of this and all the TODO's, so we don't forget to do it afterwards?
| If `m` is a `Functor`, but not a full `Monad`, then `e.toMonad m` should still be a functor too. | ||
| However, actually having these instances causes diamond problems with the aforementioned instances | ||
| implied by `Monad`. Thus, we just assume `m` is always a monad. | ||
| -/ |
There was a problem hiding this comment.
Fair enough. Why don't we just ask for the Monad m instance (ibid LawfulMonad) for the definition of toMonad then?
There was a problem hiding this comment.
@goens principle of least privilege :) One can call toMonad even when m is not necessarily a monad. So, I'd rather not add a [Monad m] constraint on toMonad.
| T.foldl (fun _ s a => insert ⟨_, a⟩ s) ∅ | ||
|
|
||
| @[simp] | ||
| theorem HVector.vars_nil : | ||
| --TODO: find a name that better encapsulates that it's the *transitive* closure |
There was a problem hiding this comment.
What about uses like you suggest below? The transitivity is not quite explicit, but uses does feel more transitive than vars.
There was a problem hiding this comment.
@goens This is a good refactor, but to be consistent, we would need to change a lot of names of lemmas, theorems, and other definitions that use the vars terminology right now. I'd suggest doing this after.
Co-authored-by: Andrés Goens <[email protected]>
Co-authored-by: Andrés Goens <[email protected]>
Co-authored-by: Andrés Goens <[email protected]>
Co-authored-by: Andrés Goens <[email protected]>
|
I think we should address #250 in this very PR, if possible, as it will minimize the diff of this PR quite a bit. |
Also made necessary adaptations to bundle the side-effect monad `m` into the `Dialect` structure The `ScfFunctor` file is still broken
Add a custom field into each
Opthat declares if its signature is pure or not. If it is pure, it returnsa, and if impure, it returnsIO a. The default signature object is pure.