4 ms·
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](htt
by LangMakers 5y ago
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/Target/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.
- creata 5y agoI 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 https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
- throwaway17_17 5y agoThat 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.
- creata 5y agoAgreed: 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-tlca-14.pdf https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...