Can anyone explain how syntax elements such as { } are a net win? This looks like they've tuned the syntax to not scare anyone off in the first week, at the expense of an economy of expression later.
Rob Pike once justified C syntax for its ability to survive pipes that mangled whitespace. That was then, this is now. To this old C programmer, anything that unnecessarily resembles C is ground glass in the eye.
This property is particularly important for readability of "embeddable" languages ("embeddable" in the sense of a language source code existing within another, for example JS within HTML script tags, or bash in a Dockerfile, or YAML string concatenation).
The C preprocessor would like to have a word with him.
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
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
}
}
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
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
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
open vec
vec.x + vec.y + vec.z
name = my_list[7]
name = my_map{"foo"}
name = my_record@foo
name = my_list[7] <> "anonymous"
name = my_list[7] <- "Eric"
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
key = "foo"
map = {key: 3}
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!
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
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.
blocks _ _ True = True
blocks Tile{isWater} floats _ = not isWater || floats
blocks Creature{} _ _ = True
blocks Fire{} _ _ = False
blocks Wall{} _ _ = True
> 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.
> 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
}
Maybe {
!list[0] + !list[1] + !list[2]
}
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).
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!)
The fact that
val x = something
val y = somethingElse
doThis(x, y)
for {
x <- something
y <- somethingElse
} yields doThis(x, y)
x = something
y = somethingElse
doThis x y
MyMonad {
x = !something
y = !somethingElse
doThis x y
}
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 }
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.
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) }
}
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.
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
}
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.
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.
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
f* x*
(=<< f) (pure x)
So what is `!` then? Well `!` is simply the absence of `*`!
f !x = f* x
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 |]
[Maybe| f x |]
[List| f x |]
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.
> 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.
While (<>) in Haskell already means a monoidal operator, something similar is frequently defined, such as:
(:?) :: Maybe a -> a -> a
(:?) = flip Data.Maybe.fromMaybe
> 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
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
> And, of course, Maybe monad:
As it happens, you can write Haskell with braces if you really want to! [0]
Similarly, even before dwohnitmok, I can read your Haskell example much faster than the curly example.
Great product design is a mix of flexibility and opinionatedness. You have to find your "users" and then build the thing they want. If HN commenters give you crap about it they're not your users, at least not yet, and that's ok. Your product doesn't have to appeal to everyone at the outset.
> Guess I'll end up adding a bracket-less version
Don't make a decision just by listening to some random strangers like me!
If you need to think differently (as in TLA+), I think having a different syntax that reflects the different thinking is a good idea.
I would love a language like C# or Python where you could just put in preconditions using the expression syntax of the language, and it would try to prove it. If it can't prove it, it might ask for more facts, give a warning, or add a runtime assertion. As far as I know the only language that does this was the experimental Spec#.
I would even go further and have complex preconditions as part of the types, so you could have say a Person with field "age" < 18 is of type Minor. (I know this is tricky. The objects would be immutable, or you'd only be able to specify Person|Minor and only narrow it with an assertion, for example). Nim has something a little bit in this direction with distinct types, and integer range types.
To be able to be a bit more 'terse' in assertions, they added quantifiers, expression functions, case- and if-expressions. Lots of small improvements to allow contracts, that are finally a boon to write simpler and clearer code.
Everything you're asking for here is available in Ada2012 and SPARK2014.
here is an example using mirai and contracts:
https://github.com/facebookexperimental/MIRAI/blob/master/ex...
(note: the contracts crate can be used for verifying at runtime as well)
I think there is danger in proposing 'assume' without at least trying to prove it and say you're wrong. I think in spark 'assume' is a guide, but it is checked and it is great, because footguns.
But honestly it's not that great of a user experience, though it does seem to have been improved at least a little bit since the last time I used it in ~2016 or so.
So you can say something like this:
0 but True
Since `True` is a `Bool` it automatically creates a role that has a method `Bool` that returns `True`.
my $role = role { method Bool { True }}
0 but role { method Bool { True }}
It creates a new subclass of Int and mixes in the role.
So:
0 but True
do {
my constant but-true = anon role { method Bool { True }}
my $class = anon class :: is Int does but-true {}
$class.new( 0 )
}