News for hackers. Stuff that matters.
Re:Kind: A Modern Proof Language by creata on Wednesday August 11, 2021 @01:34PM (#28145056)
I think they're referring to the least fixpoint operator μ, whose interface you can find in section 15.2.1 of PFPL.[0] The idea and consequences superficially seem to be very similar.

[0]: https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf

Re:Kind: A Modern Proof Language by throwaway17_17 on Wednesday August 11, 2021 @04:05PM (#28147032)
That is the correct reference. I don’t know if I’d say the similarities are only superficial however. The blog post on super-inductive types seems to bear out at least a strong isomorphism modulo syntax.
Re:Kind: A Modern Proof Language by creata on Wednesday August 11, 2021 @05:19PM (#28147922)
Agreed: I meant that there were superficial similarities, not merely superficial similarities. Here's the original paper (I think?) on self types; maybe there's an obvious link in there.

https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...