Our great sponsors
-
-
-
SurveyJS
Open-Source JSON Form Builder to Create Dynamic Forms Right in Your App. With SurveyJS form UI libraries, you can build and style forms in a fully-integrated drag & drop form builder, render them in your JS app, and store form submission data in any backend, inc. PHP, ASP.NET Core, and Node.js.
-
-
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. We plan to add opt-in termination (thus consistency) checkers, it is just not an immediate priority, 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 `Type in Type`. So it isn't problematic in itself, and removing it seems wrong.
About erasure, you can flag an argument as computationally irrelevant by writing `` instead of `(x: A)`. So, for example, in the [Vector/concat.kind](https://github.com/uwu-tech/Kind/blob/master/base/Vector/con...) 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` 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 other languages, by far.
Well `RecordWildcards` has been around for 14 years... but even without it instead of `{..}` you'd just have `_`s. The main thing that is different is that your Kind example had nested case statements while your Haskell example tried to match everything on one shot, which makes for a non-equivalent comparison.
> Not sure how that could work, though. Idris had an interesting syntax, but IIRC it wasn't general.
I assume you're talking about idiom brackets for applicatives? The general syntax is given in something like https://github.com/monadless/monadless. The idea is to basically take async-await syntax and generalize it to any monad.
So e.g. your `Maybe` example (using `!` for the equivalent of `await` for concision) would look like
Maybe {
I thought SMT2 (what you can feed to z3 -smt2), is a s-expression language that is the lowest level ("bytecode") thing. If you look at Dafny/Boogie, boogie is a much more human readable IR. I'm trying to build a pythonic variant of Boogie.
https://github.com/adsharma/py2many/blob/main/tests/cases/de...
FWIW: That project was started as an internal tool with a playful acronym and then went from obscure to well-known enough to making renaming a somewhat regrettable concept rather quickly just due to momentum. I think we'd have named it differently if we were aiming for widespread usage :-)
We had no reason to worry about making it popular, the effort was staffed to improve developing Kubernetes itself.
As for googling, I recommend adding keywords like "kubernetes" and for issues searching the repo itself or reaching out to the community for help https://github.com/kubernetes-sigs/kind#community
That tool is written in "Go" which also somewhat famously doesn't search well without changing your terms up a bit.