New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

`cps` attribute #1557

Open
mtzguido opened this Issue Oct 8, 2018 · 1 comment

Comments

Projects
None yet
1 participant
@mtzguido
Contributor

mtzguido commented Oct 8, 2018

We have a cps attribute in prims, which is used for the M effect to make it processable by DM4F.

assume val cps : attribute
(* .... *)
effect M (a:Type) = Tot a (attributes cps)

But, we special case it a lot, to the point that one can even delete the definition of the cps attribute, since the desugarer recognizes that when it sees cps, it means to add the CPS cflag, without trying to interpret/lookup cps in any way.

So what's the point of the attribute? And did we expect to have many cps effects? Perhaps for layering?

For layering, I would have assumed the syntax would be something like:

new_effect_transformer StateT = {
    repr = fun a -> s -> M (a * s); 
    (* ... plus the usual DM4F *)
}

new_effect StExn = StateT EXN (* or similar *)

without a need for another M.

Summoning @kyoDralliam @nikswamy @catalin-hritcu @msprotz in case you guys remember. Personally I vote for removing the attribute and corresponding CPS flag.

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 16, 2018

Contributor

The cflag exists since the M effect gets unfolded (as it should) during typechecking, and we'd lose track of it otherwise. But the desugaring is crazy anyway.

Contributor

mtzguido commented Oct 16, 2018

The cflag exists since the M effect gets unfolded (as it should) during typechecking, and we'd lose track of it otherwise. But the desugaring is crazy anyway.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment