Re:Kind: A Modern Proof Language
by LangMakers on Wednesday August 11, 2021 @01:05PM
(#28144680)
Thanks for the compliment on FmcToJS! It is probably the most messy part of the whole project though. We can't wait to port it entirely to [JavaScript.kind](https://github.com/uwu-tech/Kind/blob/master/base/Kind/Comp/...). That said, we put a lot of work on it and hell it does produce some satisfying JavaScript code.
I'm not familiar with that mechanism, do you have a link? The dependent function type, `∀ (x : A) -> B(x)` allows the type returned by a function call, `f(x)`, to depend on the value of the argument, `x`. The self-dependent function type, `∀ f(x : A) -> B(f,x)` allows the type returned by a function call, `f(x)`, to also depend on the value of the function, `f`. That is sufficient to encode all the inductive datatypes and proofs present in traditional proof languages, as well as many other things.
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.
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.
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...
As a quick question, the self types as the primitive for induction seems to resemble the general mechanism Robert Harper exposes in PFPL, i.e. a recursive construct over a sum. If that is not the inspiration, do you have any publications (or blogs, etc) that talk in more depth about the induction principle in Kind?