There are some similarities with Rust's (planned) const-generics system (swapping const for Pure as appropriate):
const expressions can only refer to const variables
const values can lose their constness and be used as normal runtime/impure values (the comonadic "extract", I don't remember which Greek letter they used for it in the paper)
A const fn can be applied to a const expression to yield a const result; a non-constfn can't
And some differences:
const T in Rust isn't a type, but part of the "generics" system
Relatedly, there's no comonadic "duplicate" (const T -> const (const T))) -- which might make more sense if constwere a type
And of course, one of them is for tracking "known at compile-time" and the other is for tracking purity.
I thought you might find this interesting:
http://semantic-domain.blogspot.com/2019/07/all-comonads-all-time.html https://www.cl.cam.ac.uk/~nk480/popl20-cap-submission.pdf
There are some similarities with Rust's (planned)
const-generics system (swappingconstforPureas appropriate):constexpressions can only refer toconstvariablesconstvalues can lose theirconstness and be used as normal runtime/impure values (the comonadic "extract", I don't remember which Greek letter they used for it in the paper)A
const fncan be applied to aconstexpression to yield aconstresult; a non-constfncan'tAnd some differences:
const Tin Rust isn't a type, but part of the "generics" systemRelatedly, there's no comonadic "duplicate" (
const T->const (const T))) -- which might make more sense ifconstwere a typeAnd of course, one of them is for tracking "known at compile-time" and the other is for tracking purity.