Recent submissions

Comment · 5 years ago
Comment · 5 years ago
Speaking of names, I love yours
Comment · 5 years ago
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.
Comment · 5 years ago
I'm both proud and ashamed of this rant. At least it changed my views about some subjects.
Comment · 5 years ago
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...)
Comment · 5 years ago
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!)

Comment · 5 years ago
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.

Comment · 5 years ago
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!

Comment · 5 years ago
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.
Comment · 5 years 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/...). 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.

Comment · 5 years ago
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.
Comment · 5 years ago
Comment · 5 years ago
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.
Comment · 5 years ago
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.

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton