4 ms·

Kind has a "how I learned to stop worrying and love the `Type:Type`" vibe. That doesn't make it invalid as a proof language. It just inverts the priority: inste

Kind has a "how I learned to stop worrying and love the `Type:Type`" vibe. That doesn't make it invalid as a proof language. It just inverts the priority: instead of consistency being the default and expressivity being opt-in (as in Agda, with the `type-in-type` pragma), it is expressive by default, and consistency is an opt-in. I strongly believe that is the right way. It is still not implemented, but the language is completely ready for that. About Type in Type specifically, keep in mind that there are consistent, interesting type theories that feature it. So it isn't problematic in itself, and removing it seems wrong. About erasure, you can flag an argument as computationally irrelevant by writing `<x: A>` instead of `(x: A)`. So, for example, in the `Vector.concat.kind` [1] file, `A`, `n` and `m` are erased. As such, the length of the vector doesn't affect the runtime. As a good practice, you may also write `f<x>` instead of `f(x)` syntax for erased arguments, but that is optional. > TL;DR -- I think the language looks nice, and the compile to JS (from what I read of the Formcore source) looks to be well done. Also, the docs that are present are well presented in a non-academic way that I find pretty readable. Thanks for the kind words. We put a lot of effort on the compilers and, while there is still a lot to improve, I'm confident they're ahead of all the similar languages, by far. [1] https://github.com/uwu-tech/Kind/blob/master/base/Vector/concat.kind https://github.com/uwu-tech/Kind/blob/master/base/Vector/con...

throwaway17_17 5y ago
I want to offer explicit congratulations on the FmcToJs.js source, it is very, very well done and the emphasis on translation to a reasonably efficient JS program is evident from that file alone. I may even try and work a translation layer from my personal programming language to Fmc just as a fun project for the weekend. 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?
- 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 ago
    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 https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
    - throwaway17_17 5y ago
      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.
      - creata 5y ago
        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-tlca-14.pdf https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...
naasking 5y ago
> It just inverts the priority: instead of consistency being the default and expressivity being opt-in (as in Agda, with the `type-in-type` pragma), it is expressive by default, and consistency is an opt-in. I strongly believe that is the right way. I'm cautiously optimistic, but skeptical. Type:Type typically makes compilation non-terminating, which is not great. Is my program just taking a long time to compile, or is it in a loop? Also, I'm a strong believer in the adage, "you cannot add security, you must remove insecurity". A similar sentiment would seem to apply to "inconsistency".

throwaway17_17 5y ago

I want to offer explicit congratulations on the FmcToJs.js source, it is very, very well done and the emphasis on translation to a reasonably efficient JS program is evident from that file alone. I may even try and work a translation layer from my personal programming language to Fmc just as a fun project for the weekend. 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?

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 ago
  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 https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
  - throwaway17_17 5y ago
    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.
    - creata 5y ago
      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-tlca-14.pdf https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...

naasking 5y ago

> It just inverts the priority: instead of consistency being the default and expressivity being opt-in (as in Agda, with the `type-in-type` pragma), it is expressive by default, and consistency is an opt-in. I strongly believe that is the right way. I'm cautiously optimistic, but skeptical. Type:Type typically makes compilation non-terminating, which is not great. Is my program just taking a long time to compile, or is it in a loop? Also, I'm a strong believer in the adage, "you cannot add security, you must remove insecurity". A similar sentiment would seem to apply to "inconsistency".