News for hackers. Stuff that matters.
Re:Kind: A Modern Proof Language by LangMakers on Wednesday August 11, 2021 @01:56PM (#28145337)
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!

Re:Kind: A Modern Proof Language by dwohnitmok on Wednesday August 11, 2021 @02:16PM (#28145617)
I really like the language, but you're exaggerating the verbosity of the Haskell code by not comparing them in an apples-to-apples way.

Here's the same Haskell code written in the same way you've written your Kind code.

    blocks entity floats ghost = case ghost of
      True -> True
      False -> case entity of
        Creature{..} -> True
        Tile{..} -> not isWater || True
        Wall{..} -> True
        Fire{..} -> False
The `{..}` is from `RecordWildCards`, a common extension.

I do like the omission of `let` and `where` in favor of just variable definitions. For monadic notation, instead of `get` and `return` I'd prefer something like https://github.com/monadless/monadless

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.

Re:Kind: A Modern Proof Language by overhero on Wednesday August 11, 2021 @04:00PM (#28146986)
an even more succinct way might be:

   blocks _              _      True = True
   blocks Tile{isWater}  floats _    = not isWater || floats
   blocks Creature{}     _      _    = True
   blocks Fire{}         _      _    = False
   blocks Wall{}         _      _    = True

it does not get much closer to truth-tables, if you ask me
Re:Kind: A Modern Proof Language by LangMakers on Wednesday August 11, 2021 @02:23PM (#28145720)
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.

Re:Kind: A Modern Proof Language by dwohnitmok on Wednesday August 11, 2021 @02:33PM (#28145855)
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, and you purposefully repeated field names on both sides of `->`, which is not necessary even in vanilla Haskell when you work with records.

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

RE Idris 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 {
    x = !list[0]
    y = !list[1]
    z = !list[2]
    x + y + z 
  }
but because it doesn't have to be in A-normal form anymore you can compress it all into a single line.

  Maybe {
    !list[0] + !list[1] + !list[2]
  }
So you can take any normal code you have and put in a monadic context simply by inserting brackets around the whole thing and then sprinkling in `!`s as necessary.

EDIT: Or to think of it another way, just move the `get` from the left-hand side of `=` to the right-hand side. I'd recommend renaming it to something to indicate that this is a syntactic transformation, rather than a normal function (which is why I like something like `!` or anything else that has a symbol in it to indicate this is essentially a macro).

Re:Kind: A Modern Proof Language by LangMakers on Wednesday August 11, 2021 @02:39PM (#28145933)
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!)

Re:Kind: A Modern Proof Language by lmm on Thursday August 12, 2021 @12:13AM (#28151831)
Having used various monadless-style implementations I think they're a mistake. The whole point of using a monad is because you want to explicitly sequence some (generally noncommutative) effect and be sure that refactoring won't change the behaviour (whereas if you reorder two `<-` lines then that is a behavioural change that you need to test). If you allow ! at arbitrary points in an expression then you end up with something more akin to checked exceptions where you know that an effect is happening somewhere but not what all the possible code paths are, and at that point you might as well just use side-effecting code.
Re:Kind: A Modern Proof Language by dwohnitmok on Thursday August 12, 2021 @02:20AM (#28152640)
Yeah this was the same discussion that happened when monadless was released in the Scala community. I personally don't see much of a difference between reordering `<-` lines and reordering !-ed expressions, especially in a strict language (such as Kind). The same arguments for how you rearranging different !-ed expressions can result in different behavior whereas non-!-ed expressions can be reordered with no change ring exactly analogously to me for `<-` statements vs the usual `=` in a let expression.

The fact that

  val x = something
  val y = somethingElse
  doThis(x, y)
allows for interchanging x and y if `something` and `somethingElse` are pure but

  for {
    x <- something
    y <- somethingElse
  } yields doThis(x, y)
doesn't allow for interchanging `x` and `y` feels approximately just as confusing (or not-confusing) as

  x = something
  y = somethingElse
  doThis x y
having interchangeable `x`s and `y`s but

  MyMonad {
    x = !something
    y = !somethingElse
    doThis x y
  }
not having interchangeable `x`s and `y`s.

I suppose what you're really getting at is what happens when you combine it all into a single line a la

  MyMonad { doThis !something !somethingElse }
but I still don't find it confusing for a strict language (and besides legions of developers have had a chance to familiarize themselves with this via async-await). The rules in either case are the same. If you move around `->`s behavior might change. Likewise if you move around `!`s behavior might change.

In a lazy language such as Haskell I agree that it can be rather weird to have to think about how inserting a pair of brackets and some `!`s around suddenly causes sequencing that is different from how a normal statement is evaluated (although the bangs are quite suggestive, especially given their lineage in Haskell, indeed given a `Lazy` monad these bangs just become the same thing as bangs in Haskell, so another way you can view this is as a generalization of Haskell bang patterns). But Kind is a strict language AFAICT and in a strict language evaluation from left to right and top to bottom is the norm. And that left-to-right, top-to-bottom order immediately tells you what the code paths are.

Even in a lazy context where the order of evaluation might be a bit more confusing, this async-await style of writing code is still valuable for delineating which code blocks are side-effectful are and which aren't. Checked exceptions/checked effects are still very valuable! It's valuable enough that e.g. the Haskell community is perfectly willing to compromise on knowing what all the code paths are with stuff like ApplicativeDo.

Having spent a considerable time with cats-effects in Scala and a little time with Kotlin's Arrow Fx there are times I still prefer Arrow Fx despite the general clunkiness of Kotlin's Arrow ecosystem over cats-effect precisely because I just need to stick in a `suspend` instead of having to contort perfectly fine code into a for-comprehension when I introduce some effects simply because I didn't write my pure code with the Identity monad the first time around.

Re:Kind: A Modern Proof Language by lmm on Thursday August 12, 2021 @02:54AM (#28152901)
> but I still don't find it confusing for a strict language (and besides legions of developers have had a chance to familiarize themselves with this via async-await). The rules in either case are the same. If you move around `->`s behavior might change. Likewise if you move around `!`s behavior might change.

The <-s are always in the same place on the line and always ordered top-to-bottom, whereas it's not at all clear what ordering applies to the !s - it's generally "evaluation order", but the whole point of using monads is to get away from relying on evaluation order! When it gets confusing is when you're doing something that has a nontrivial evaluation order in the expressions, e.g.

    MyMonad {
      something sortBy { (x, y) => someComparison(x, y, !z) }
    }
Even left-to-right evaluation of function arguments isn't always obvious - for some functions it would be more natural to evaluate in a different order, and not all strict languages evaluate left-to-right (I believe in C/C++ the order is undefined).

I agree that it's not so different from async/await or ApplicativeDo, but I find both those things confusing, and I hate dealing with arrow FX precisely because I can't follow what the code is doing except by thinking through what all the evaluation is doing operationally.

Re:Kind: A Modern Proof Language by dwohnitmok on Thursday August 12, 2021 @03:58PM (#28160740)
> whereas it's not at all clear what ordering applies to the !s - it's generally "evaluation order"

But the evaluation rule for ordering of effects is fairly simple. Left-to-right (taking into account paren nesting) and then top-to-bottom. It's the exact same as the `<-`s, just with an additional left-to-right dimension.

I brought up "evaluation order" in languages because I wanted to drive home that this left-to-right, top-to-bottom order is natural for developers (and C/C++ is a well-known outlier among imperative languages in this regard with a full stable of unspecified and undefined things, but Java, Python, Javascript, Rust, etc. all evaluate in that order). But it's not actually essential that any of the non-monadic code obey that evaluation order. You don't actually rely on evaluation order anymore than the sequencing provided by monads. All the expressions in the middle could be lazily or eagerly evaluated, it doesn't matter.

You bring up a good point with closures in the form of anonymous functions/objects, but that is also the only place that I would argue it's confusing for a developer coming from an imperative background (some who might expect this to be an exception to the left-to-right, top-to-bottom rule as it is e.g. with async-await in Javascript where a closure is not created and the Promise is regenerated where it is created), but you could just disallow it there or require additional annotation of the anonymous function, as e.g. happens in most languages such as Rust and JS. Even there the left-right, top-bottom rule could apply, it might just confuse some developers, who are used to it having an exception in anonymous functions.

Everywhere else not only does left-right, top-bottom give a concise and evaluation-independent (up to the sequencing constraints imposed by the monad) description of how the effects will be executed (which can be made universally true if you're willing to tolerate it for closures or you can just disallow `!`s in anonymous function bodies), this ordering also agrees with what developers coming from other languages would expect.

Put another way, I don't think most developers will be confused by the execution order of effects of `!` that doesn't have anonymous functions.

I think you could ask any developer, even those unfamiliar with FP, what order they think the effects preceded by a `!` will evaluate in the following expression and the overwhelming majority of them would get it right.

  MyMonad {
    x = !effectfulOp0
    someFunction x !(effectfulOp1 x !effectfulOp2) !effectfulOp3
  }
Again you don't need to follow what the evaluation is doing operationally. You just need to do a syntactic scan. No matter what evaluation strategy is used, the order of effects will always be `effectfulOp0`, `effectfulOp2`, `effectfulOp1`, and then `effectfulOp3`. There is no operational reasoning here at all. It's purely syntactic and local. This is true even for monads that seem to have a weird order of effects such as the reverse state monad, you just have to be very specific about what the effect actually is (the addition of thunks in the case of the reverse state monad), which is the same case as with do-notation, which is why lazy IO is so confusing, even though technically the monadic sequencing of effects is still being followed.

Indeed this distinction between operational and denotational reasoning has nothing to do with syntax (as it shouldn't since those are semantic questions), but rather your choice of monad. As Conal Elliott rightfully points out monadic IO is intrinsically a dismal failure if you want denotational semantics instead of operational semantics to begin with, even were you to write out everything with bind syntax. The problem is not with the syntax but with the monad itself (Conal would probably prefer the word monad here to have scare quotes around it when referring to monadic IO).

At the end of the day I view the differences between async-await syntax and do-notation as a difference in degree rather than kind (and indeed this is usually how I explain do-notation to developers familiar with async-await), whereas I think there's a quantum jump from normal bind/flatMap nesting and do-notation. However, I view the syntactic affordance given by async-await syntax to be a much larger win, especially if your language already begins with a block-inspired syntax with variable declaration statements rather than a lambda calculus-inspired syntax with let expressions.

Re:Kind: A Modern Proof Language by lmm on Friday August 13, 2021 @01:02AM (#28165635)
> I brought up "evaluation order" in languages because I wanted to drive home that this left-to-right, top-to-bottom order is natural for developers (and C/C++ is a well-known outlier among imperative languages in this regard with a full stable of unspecified and undefined things, but Java, Python, Javascript, Rust, etc. all evaluate in that order). But it's not actually essential that any of the non-monadic code obey that evaluation order. You don't actually rely on evaluation order anymore than the sequencing provided by monads. All the expressions in the middle could be lazily or eagerly evaluated, it doesn't matter.

My point is that you are in much the same place (and have the same difficulties in understanding and refactoring) as if you were reading code in a language with pervasive side effects. In an imperative language all the effects happen left-to-right, top-to-bottom - but if you're using monads at all it's presumably because you find that kind of code difficult to understand or maintain.

> You bring up a good point with closures in the form of anonymous functions/objects, but that is also the only place that I would argue it's confusing for a developer coming from an imperative background (some who might expect this to be an exception to the left-to-right, top-to-bottom rule as it is e.g. with async-await in Javascript where a closure is not created and the Promise is regenerated where it is created), but you could just disallow it there or require additional annotation of the anonymous function, as e.g. happens in most languages such as Rust and JS. Even there the left-right, top-bottom rule could apply, it might just confuse some developers, who are used to it having an exception in anonymous functions.

It happens anywhere you have control flow - I thought of closures first because in functional style that's the most natural way to have control flow, but if you're looking to make this something that works the way imperative programmers expect then they'll expect to be able to use if/then/while/... . Even if you only allow expressions, many programmers would expect && and || to have short-circuiting behaviour that affects any effects in their operands.

Yes, simple, straight-through code is easy to understand in this style (although even then, I'd argue that having to scan every full line for !s slows you down a lot compared to being able to scan down a single column for <-s) - but simple, straight-through code is easy to understand in any style. The measure of a programming style is how well it handles complex, messy code.

> Indeed this distinction between operational and denotational reasoning has nothing to do with syntax (as it shouldn't since those are semantic questions), but rather your choice of monad.

Disagree. Whether something is a statement or an expression is very much a question about syntax, but also very much a question of whether you reason operationally or denotationally.

> As Conal Elliott rightfully points out monadic IO is intrinsically a dismal failure if you want denotational semantics instead of operational semantics to begin with, even were you to write out everything with bind syntax. The problem is not with the syntax but with the monad itself (Conal would probably prefer the word monad here to have scare quotes around it when referring to monadic IO).

IO values (or rather "values") have extremely weak denotational semantics (and almost no algebraic properties), no argument there. But I'd actually say that that makes it even more important to put the monad laws front and center when working with IO, since they're pretty much the only laws that IO has. If you want to change the sequence of IO actions that your program performs, you can only reason about that operationally, but if you want the program to perform the same (opaque) sequence of IO actions, you can do that denotationally, and it turns out that's enough for a lot of the refactorings you would want to perform.

All that said, IO is not remotely the most important use case for monads, and for many applications I'd actually be ok with using something like monadless solely for IO, if the codebase stuck to traditional for/yield/<- style for more semantically important monads.

Re:Kind: A Modern Proof Language by dwohnitmok on Sunday August 15, 2021 @03:52AM (#28186956)
> but if you're looking to make this something that works the way imperative programmers expect

I think you're misunderstanding me and I regret bringing up the appeal to "imperative programmers." That was simply to illustrate that the semantics of the syntax are immediately accessible to the majority of programmers who have never encountered denotational semantics. But if denotational semantics are what are important to you, let me back up because the whole appeal to "imperative programmers" is not the purpose of `!`, the purpose is rather more meant here in what I wrote:

> having to contort perfectly fine code into a for-comprehension when I introduce some effects simply because I didn't write my pure code with the Identity monad the first time around.

The perspective I'm coming from is based on Moggi's original paper, which is to realize that semantically monadic code is simply a generalization of "pure" (this is kind of an underspecified term here, but I think we both understand what this is meant to refer to) code, and to have the syntax reflect that generalization, rather than draw a sharp divide between monadic code and pure code that `do`-notation introduces (most noticeably by forcing A-normal form). You still get that division at the type level and through various fencing syntax, which is good for making sure you don't lose purity guarantees, but it's important to realize that these things share the same fundamentals (this is why e.g. Haskell can claim to be pure even in the presence of effects, which is confusing to newcomers who view do-notation as a completely different part of Haskell).

Indeed I'll make a perhaps bold claim. This `!` or async-await syntax is a far more faithful representation of the denotational semantics laid out in Moggi's original paper describing the semantics of monads and computations than do-notation is.

So since we're on the subject of denotational semantics, let's start with the denotational semantics of monads. When considering denotational semantics, what is a monad? We can appeal to Moggi's original presentation of this using Kleisli triples, most notably the Kleisli extension operator and the component of the natural transformation on the identity endofunctor (for Haskell programmers this is the categorical version of the reverse bind operator and pure). In particular, Moggi gives a compelling overview of how to achieve a meaningful denotational semantic mapping here here, given a well-defined monad. This doesn't come for free in syntax inspired by the lambda calculus because the categorical representation translate function application to composition (as it does everything see e.g. the categorical representation of monoids), but we can get there by thinking of "expression sections, " by analogy to tuple sections. That is, roughly speaking, you can think of `(_ subExpr0 subExpr1)` as being the function `x -> (x subExpr0 subExpr1)` and more generally of parenthesized expression in general as a series of compositions of expression sections (with atomic values such as literals being the usual morphisms from terminal objects in the category, given that we're in the lambda calculus and therefore in a Cartesian closed category we're guaranteed these exist).

Fundamentally Moggi's insight is that the denotational semantics behind

  f x
can be augmented via a monad to be

  f* x*
where `*` here is the Kleisli extension operator (what Moggi refers to as `_*`). In Haskell terms this is

  (=<< f) (pure x)
The fact that we're using reverse-bind in one case and pure in the other case is a quirk of function application in the lambda calculus; again at the categorical level where everything including function application is just composition, these are both just applications of the Kleisli extension operator.

So what is `!` then? Well `!` is simply the absence of `*`!

  f !x = f* x
Denotationally that's all `!` is! Indeed we can choose to think of `!` as syntactic sugar, but that's optional. You can instead give it an immediate denotation instead of having to desugar things first. The reason we use `!` to denote the absence of Kleisli extension rather than its presence is because most of the time you care only about its absence. Otherwise your code would be absolutely filled with `!`s.

So that's the denotational semantics of what's going on here. There was a lot there, but it's all in service of a single point: if you care about denotational semantics `!`/monadless syntax has a much stronger story than do-notation (e.g. what exactly is the denotational semantic of `<-`?). To describe the denotational semantics of do-notation you have to essentially perform the syntax desugaring first before resorting to the non-monadic denotational semantics of the desugared code. This is completely ignoring Moggi's insight!

So from the perspective of denotational semantics, do-notation is absolutely no help! We have to actively ignore our monadic context and "undo" the do-notation and resort to the underlying original denotational semantics instead of getting any semantic help from our monad at all.

But of course most programmers have not heard of denotational semantics and don't care about denotational semantics. So for them, what is the point of `!`? The point is not to force-fit imperative code. Indeed in that case, as you point out, the natural evolution is to throw in all sorts of different kinds of if-statements, while-statements, exceptions and the like, which is not what I'm advocating. The point is to realize that all that is just a reflection of the same thing! You just need to assign a different semantic mapping is all!

  [Identity| f x |]
is one mapping where everything is "pure" in the way we normally think of it

  [Maybe| f x |]
is one with short-circuiting failure.

  [List| f x |]
is non-determinism and so on.

This desire has appeared many times in the FP community and given birth to many proposals (notably I'm basically stealing syntax from McBride's idiom brackets here, the `!` addition here essentially can be thought of as an addition to make idiom brackets work for monads instead of just applicatives, and indeed `!`-notation itself has already been implemented in Idris although in a slightly different fashion than how I've presented it).

The point of `!` is to expose the fact that monadic semantics are exactly what matters and the only thing that matters!*

That we cannot seamlessly express this relationship syntactically by just appending brackets and instead must do so through contortion to an entirely different syntax in the form of do-notation represents to me a failure of denotational reasoning! Indeed while e.g. Idris describes this notation in terms of do-notation (http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm...) (one thing I like about monadless and why I use it as my go-to example is because it doesn't define itself in terms of for-comprehensions), as I've outlined above, I believe it has a far stronger standalone semantic interpretation.

Re:Kind: A Modern Proof Language by lmm on Wednesday August 18, 2021 @01:09AM (#28217950)
Meh - I find the idea of overloading what function application means very counterproductive. You can say that function application is just a special case of Kleisli composition and the syntax should really mean Kleisli composition, but really that's just the statement that a lot of things behave as composition in some sense (which is why category theory works at all).

> Denotationally that's all `!` is! Indeed we can choose to think of `!` as syntactic sugar, but that's optional. You can instead give it an immediate denotation instead of having to desugar things first. The reason we use `!` to denote the absence of Kleisli extension rather than its presence is because most of the time you care only about its absence. Otherwise your code would be absolutely filled with `!`s.

I think it's worth tugging at this thread. Even within our effectful/imperative DSL block (which is what I see do notation as), most of the time we don't actually want to do effectful Kleisli composition. Most of the time we want our function application syntax to denote regular function application. For the same reason, I don't find Moggi's approach compelling - in theory you could understand the denotation of a do block by understanding the whole thing as Kleisli composition and then algebraically simplifying, but in practice that would be far too complex for humans. (In the same way, I felt Frank was completely the wrong approach, because I don't want to push a maximal bundle of effects in, I want to pull a minimal bundle of effects out).

In many cases I'm skeptical about using do notation at all - often using the applicative or arrow combinators expresses the denotation more clearly, putting us in a position where it's much easier to apply algebraic laws - but where I think it does succeed is in letting you mix a minimal piece of operationally-understood effect into a procedure the bulk of which is still denotationally-understood, and, ideally, lets you view that piece of code from both perspectives at the same time. So the way I'd approach it is "what is the simplest/most restricted possible set of effectful-compositions that allows us to express everything we want", and current do notation mostly fits the bill.

As you say, there's a lot of proposals and efforts to relax the restraints of do notation and offer a more expressive way of working with effects, but I've always found they lead to code that was confusing to maintain. So in the end I bite the bullet and say that yes, I will refactor the whole call chain if it turns out it needs the current time somewhere at the bottom (or else I'll decide that accessing the current time is not an effect that I care to track explicitly at all), because although it's more work up-front, it's ultimately the only way to avoid ending up with code that's confusing to read.

Re:Kind: A Modern Proof Language by thewakalix on Wednesday August 11, 2021 @04:04PM (#28147022)
> For example, working with Maybe is often frustrating in functional languages. In Kind, we have a default operator: [<>]

While (<>) in Haskell already means a monoidal operator, something similar is frequently defined, such as:

    (:?) :: Maybe a -> a -> a
    (:?) = flip Data.Maybe.fromMaybe
(Making an alternative or supplemental Prelude out of functions like this is a common step in the evolution of a Haskell programmer, like writing a monad tutorial.)

> An "abort" operator, that flattens your code:

That particular function can be written even more concisely in Haskell:

    sumFirst3 :: [Natural] -> Natural
    sumFirst3 list
      | (x : y : z : _) <- list = x + y + z
      | otherwise = 0
And in other cases, the Either monad provides the same logic:

    sumFirst3' :: [Natural] -> Natural
    sumFirst3' list = fromEither do
      x <- list !!? 0 `abort` 0
      y <- list !!? 1 `abort` 0
      z <- list !!? 2 `abort` 0
      return $ x + y + z

    abort :: Maybe a -> e -> Either e a
    abort (Just a) _ = Right a
    abort Nothing e = Left e
(fromEither and (!!?) are utility functions like (:?). For that matter, abort is just a shorter name for maybeToRight.)

> And, of course, Maybe monad:

As it happens, you can write Haskell with braces if you really want to! [0]

[0] https://en.wikipedia.org/wiki/Haskell_features#Layout

Re:Kind: A Modern Proof Language by LangMakers on Wednesday August 11, 2021 @04:13PM (#28147130)
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.
Re:Kind: A Modern Proof Language by lmm on Thursday August 12, 2021 @12:08AM (#28151783)
Isn't that the whole point of MTL-style typeclasses? You use e.g. throwError and can be confident that it'll be plumbed appropriately for whichever context you're currently in. Maybe shouldn't be a special case.
Re:Kind: A Modern Proof Language by yakubin on Thursday August 12, 2021 @05:47AM (#28154158)
I don't spend much time with Haskell, only sometimes I'll read a blog post using it. But still, to me it's one of the most readable languages out there. Day-to-day I work with C++ and Rust and I'm really annoyed with the amount of irrelevant punctuation they force on the programmer. I look at the code, and instead of seeing what it expresses, first I need to peel off the noise, curly braces, colons in weird places, commas, just noise. Scheme and, to a greater extent, SML are really good here.

Similarly, even before dwohnitmok, I can read your Haskell example much faster than the curly example.

Re:Kind: A Modern Proof Language by Syzygies on Wednesday August 11, 2021 @09:58PM (#28150746)
Wow. Thank you for that thoughtful response. C aside, Haskell is my primary recent experience, so everything you say resonates. Like Idris, you're doing a lot to clean up Haskell.