LangMakers

I think Kind-Core should be that language. It is the simplest proof kernel, after all, by far :) And it has nothing human or inventive. Basically just the lambda calculus with the self dependent function type. But I guess it ultimately is this old XKCD kind of problem: https://xkcd.com/927/

Speaking of names, I love yours

You're forced to be in the Either monad to use your `abort` though, which kinda beats the point (you could just use the Maybe monad...). It is refreshing to be able to just throw an abort literally anywhere in your code, and get rid of a `Maybe` without changing the structure of your code, resting assured that the `none` case is dealt with properly.

I'm both proud and ashamed of this rant. At least it changed my views about some subjects.

They are only used in case-of and monadic blocks, and allow avoiding commas and semicolons everywhere else without having the annoying issues with meaningful spaces! I totally understand your initial impression, but consider reading my thoughts below before judging prematurely. (Guess I'll end up adding a bracket-less version of case-of to satisfy the hyper demanding crowd of HackerNews...)

Oh, ok, then I was ignorant about {..} - sorry! You still need to rename every field you need, though. So Haskell is, at best, comparably verbose, and, at worst, much more. It also kind of encourage one-letter variable names.

About the monadic syntax, that is really clever, and makes a lot of sense to me. I want this implemented, now. Will keep that in mind. (And accept PRs!)

Fair point! That is a recent update of Haskell, though (one I wasn't aware of when designing the case syntax). It does agree with my point, though, right?

> The main problem with `do`-inspired monadic notation is that it forces monadic code to always be in A-normal form, which is pretty annoying. It'd be far nicer to allow for monadic code to look the same as normal code, just with say an extra brace (such as "IO { }") to indicate that you're inside a monad.

I agree with that. Not sure how that could work, though. Idris had an interesting syntax, but IIRC it wasn't general.

Hmm. I understand your rejection for `{}`, but I really think the end result feels nothing like the Java experience. Can I have a shot at defending it? :) It will be a long answer including some of my reasonings, and by all means feel free to disagree if you think I'm wrong about something.

Kind is extremely permissible and terse in general, and a lot of caution and love is put in making it very practical. While `{}` looks like noise in some places, it allows others to be less verbose, resulting in some snippets that look almost like Python, even though Kind isn't indentation aware (which, IMO, is very annoying). For example, commas and semicolons are always optional, so you can actually write lists as just `[1 2 3]`, maps as just `{"foo":1 "bar":2}` and function calls as just `f(1 2 3)`. That wouldn't work without `{}` on case.

There are many places where the Haskell-like syntax break down. We aim to fix every one of these. For example, the following Haskell function:

    blocks :: Entity -> Bool -> Bool
    blocks entity floats True = True
    blocks entity floats False = case entity of
      Creature name hp age items pos -> True
      Tile pos effect isWater -> not isWater || floats
      Wall pos -> True
      Fire pos damage kind -> False

Is equivalent to this Kind function:

    blocks(entity: Entity, floats: Bool, ghost: Bool): Bool
      case ghost {
        true: true
        false: case entity {
          creature: true
          tile: not(tile.is_water) || floats
          wall: true
          fire: false
        }
      }
          

Both do the same thing. Which one is more readable? The key insight is that we avoid repetition of variable names (a consequence of Haskell's equational notation), and the need to re-name every field of every variant every time you pattern-match (by naming fields as `matched_name.field_name` by default). That sounds like a small thing, but pattern-matching is the bread and butter of functional programming. Having such a terse syntax for case-of makes the whole language feel so much more refreshing.

Just like that, there are dozens of small little things that we do to make the syntax just work in practice. For example, working with Maybe is often frustrating in functional languages. In Kind, we have a default operator:

    let x = some(3) <> 5 // x is 3
    let y = none    <> 5 // x is 5

An "abort" operator, that flattens your code:

    sum_first_3(list: List<Nat>): Nat
      x = list[0] abort 0 // returns 0 if x is none
      y = list[1] abort 0
      z = list[2] abort 0
      x + y + z

And, of course, Maybe monad:

    sum_first_3(list: List<Nat>): Nat
      Maybe {
        get x = list[0]
        get y = list[1]
        bet z = list[2]
        return x + y + z
      } <> 0

And the same attention we gave to Maybe, we gave to so many other small things. For another example, we HATE indentation. Pattern-matching a structure with only one constructor causes a needless indentation. In Kind, you can use "open", that flattens it too:

    open vec
    vec.x + vec.y + vec.z

Another source of frustration in Haskell is setting/getting values from lists, maps, records. Things are so inconsistent. `Map.lookup`, `List.index`, `!!`. And lenses, while amazing, are currently really messy, hard to learn and read, full of dependencies and impact the performance. Kind has simple and obvious answers for all of these. For example:

    name = my_list[7]

Works just as you expect, returning the 7th element of `my_list : List<A>` as a `Maybe<A>`.

    name = my_map{"foo"}

Returns the "foo" entry of `my_map : Map<A>` as a `Maybe<A>`. And:

    name = my_record@foo

Returns the `foo` field of `my_record` as `A`. Don't need a maybe? Just default it:

    name = my_list[7] <> "anonymous"

Wanna set it?

    name = my_list[7] <- "Eric"

That gives the user the convenience of working on JavaScript lists, in a pure functional language.

Something else I noticed in Haskell is that code tends to become really messy when the function body becomes big. That is, when you need to chain many intermediate values. There isn't an obvious answer as to where stop growing horizontally and start adding lets vertically, and when to use `let` or `where`. Sometimes the computation flow becomes upside down, sometimes not. Also, foldr/foldl tends to become really messy when the function body is large. We have one straigth-forward answers to all these situations in Kind. Our let and "pure for" syntax allows for some pretty Python-looking functions:

    age_factorial(birth:_year Nat, names: List<String>): String
      // Concatenates all names in a string
      name = ""
      name = for name in names:
        name | " " | name

      // Computes the age
      age = current_year - birth_year

      // Computes the factorial of the age
      fact = 1
      fact = for n from 0 to age:
        fact * n

      if age <? 18 then
        "You're too young to use this program"
      else
        "Hello, " | name | ", the factorial of your age is " | fact

Obviously, pure fors just desugar to folds. Also, maps are well-thought. In JavaScript, `{foo: 3}` and `{"foo": 3}` both are the same map. In Kind, if you don't write `""`, then it is a variable, which makes a lot more sense. For example:

  key = "foo"
  map = {key: 3}

Just a small thing though. This answer is already big, and it doesn't even cover things like the built-in HTML syntax, the `sigma` sugars (`[x: Nat] x <? 50` is the type of Nats that are smaller than `50`), other sugars for theorem proving, like `rewrite`...

Basically, what I'm just saying that there are so many nice things behind the initial impression, perhaps you're judging prematurely because of your taste for `{}`? Give it a chance and I think you'll love it!

Is that really the case, though? Python, C, Rust, Ruby, Go, R, Swift, Perl. One is type of snake, the other is a type stone, and then there is a freaking letter. It seems like the less googlable the name is, the popular programming language becomes. Or, at least, that it doesn't matter that much. I swear I considered that when naming the language Kind. That could have been a terrible move though.

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.

Note that Kind is NOT terminating by default. It takes the opposite stand. Expressivity is the default, so you can write recursions and loops freely, as in Haskell or any other conventional language. Consistency is a planned opt-in, which you may use to ask Kind's compiler to check for termination of mathematical proofs specifically.

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/con...

Yep, there is that, too. You lose the ability to erase types when compiling, so you must have a representation of types at runtime, and you need to pattern-match on them. That inefficiency won't show up in normal programs, though, but if, for some reason, your program depends on a program that depends on a program (...) that uses Paths and `transp`, then you'll have to pay. This is kind of unavoidable and not that bad, though. We're more worried about the complexity of the built-in `transp` that must be part of Core. Currently, our core has only two computational primitives: beta-reduction and dereference. These are orders of magnitude simpler than `transp`, which looks extremely artificial. I'm very confident there are simpler primitives that would allow `transp` to be derived.

Yes! We're 1 file away from supporting a Python (and any other) back-end. For example, [this](https://github.com/uwu-tech/Kind/blob/master/base/Kind/Comp/...) is the simplified JS back-end. If you just copy/paste that file and edit the syntax to Python instead, we'll have a Python back-end. That kind of contribution is always welcome.

Yes, that is the gist of it: we can't do this. Negative results need to be communicated, too! But that's not all there is to it. The fact we do present a type almost identical to Path and Interval with self-types, and the fact that such type has almost identical proofs of relevant theorems (like `funext`), yet no proof of the very important `transp`, does make a strong hint that further additions to the core are necessary. It also gives us a direction, and even some hints of how the implementation could be simplified. Keep in mind that cubical type theories are somewhat complex (in sheer amount of code), but there is no evidence they can't be simplified further. Kind has a goal to keep its core as simple as possible. Being able to express all the Coq inductive proofs in a 700-LOC core is a miracle, isn't it?

> I suspect you will never be able to!

That makes no sense! In the worst case we could just go ahead and implement CubicalTT on Kind's Core. We just don't want to commit to that until we're sure there isn't a way to simplify it, even if slightly.