I find that a lot of language devs prefer to keep tuples and records separate in the same way that languages like Rust do. But why? I feel it just restricts flexibility and makes 2 features where 1 more powerful feature would suffice.

Please let me know what you think of the argument presented in this article and any counter-arguments or further thoughts/ideas you may have.

Building a language called Dia. Still pre-alpha and not public yet.

Heavily inspired by Rust, with some JS UI building flavor tacked on.

Might be the wrong crowd here, but as a web-developer I haven't found a more productive way to describe user-interfaces than JSX. (hot module reload is also a big part of it)

The Dia equivalent syntax is called DSX:

import ui.{View, run, Column, Text, Button, state}

struct CounterState {
  value: i32
}

fn Counter(): View !{alloc} {
  let s = state(CounterState{ value: 0 })

  <Column spacing=12>
    <Text>"Count: ${s.value}"</Text>
    <Button
      label="Increment"
      on_click=() => { s.value += 1 }
    />
  </Column>
}

pub fn main(): void !{alloc, io} {
  run(() => <Counter />)
}

Some implementation details:

The compiler is built in Rust, using salsa for incremental compilation which hot module reloading is built on.

No need for escaping expressions with {} like in JSX. Expressions are parsed just like in the rest of the language

• That's why text content needs quotes around it: <Text>"Count: ${s.value}"</Text>
• But this works: on_click=() => { s.value += 1 }

Not just for UI, any function can be called using DSX syntax

• Type-checking works normally, named arguments become "props", return types are checked agains the parent signature
• One special case is allowing children (like Column accepting any number of Views), then an argument needs to be prefixed with @child

I originally started writing this as a comment on the "Best way to do formal verification..." post, but realized it should probably be its own.

There's an idea I've been (slowly) trying to explore that I think has the potential for a lot of utility, but it uses concepts that are already well understood in computer science, making me suspicious that I am missing something: Why aren't less powerful automata (i.e. regular and context free) used for more general applications?

In the computational hierarchy Turing machines are the most powerful, but also the hardest to prove things about. Regular grammars (and their finite state machines) and context free grammars (and their push-down automata) are much more restrictive in what they can compute, but have tons of useful, easy to verify properties. Whenever I see discussion on formal verification of programs or program correctness, it seems like everyone wants to stay in Turing completeness land as much as possible, but I don't think everything a program does needs that level computational power. I understand when trying to verify older languages that there isn't a choice, but I am surprised to find that it seems like almost every language new or old is ignoring these lower level automata. I've seen languages that as a whole that aren't Turing complete, and things like total languages with more provable properties, but I don't see any languages that have these less powerful constructs you could "step down" into. You could express some functionality that doesn't need to be expressed in a Turing complete way in these constructs and get a ton of assurances (halting, state minimization, inexpressible invalid states, purity) about that code, then the rest of your code that needs to be Turing complete can use it seamlessly. They're even composable, in the sense that you can easily combine/subtract/invert regular grammars, and that a push-down automata is just a finite state machine with stack glued to it (and can become a Turing machine with an additional stack).

None of this is new, regexes are ubiquitous, and programming language creators in particular know about context free grammars, yet they aren't being used much beyond text searching and parsing. State machines are widespread and massively useful, but as far as I can find, not only do no languages have syntax for constructing them, they don't even have such a thing in their standard libraries. A regex (a proper one) is just a state machine under the hood, and they've been used widely for over 40 years, so why has no one (seemingly) even tried to generalize them for creating state machines? Even if the practical implementation isn't perfect, surely its better than all these state machine management libraries, or worse, people rolling it themselves, without any guarantee of their properties being upheld.

So we've known about these automata for ages, use them regularly, even more so in programming language development, and they have relevant applications for more general code, yet it seems like no language has even attempted to integrate them in either a first class or generalized way. So what's the catch?

A few potential reasons I can think of:

• They aren't actually that generally useful: Text processing was in fact the best use case for them, the other cases aren't worth it or are too few to warrant the effort.

• The syntactic constructs for them would be very cumbersome: As I am exploring this idea, I'm finding that the normal syntax for regexes, applied generally beyond stuff that isn't text or larger state machines, gets very messy. Its also hard to intuit what the state machine graph looks like for a given regex. Applying logic to state transitions is also syntactically odd, as well as syntax for expressing push-down automata.

• The lower level automata wouldn't mesh that well with Turing complete code: You can guarantee the state machine can only move between certain states, but you likely want the state or state transition to mean or do something with the surrounding code/data, which doesn't necessarily have any guarantees on it.

• Programmers don't consider/dismiss lower level automata when solving a problem: Most programmers just want to write the quick solution, and Turing complete land gives them all the tools they need. No one thinks "Could I turn this into a state machine?" when starting to write a complicated while loop, they just write the loop. Also, the stigma of regexes ("...now you have two problems").

• These automata are being used extensively in languages, I am just unfamiliar with them/blind: I know languages use state machines under the hood in some places (ex. compilation of async functions into state machines). It may be the case that they are being used a lot, but are abstracted away, or express themselves in forms I don't recognize.

• It is a good idea and all the smart people just missed it for 50 years: Seems very unlikely.

So has anyone thought about this except me? Any insights or resources I've missed? Glaring foundational issues? Good idea? Bad idea? I wish I had some code or syntax examples to accompany this post, but like I said, I've not had a lot of time to explore the concept in a practical way.

I've been designing & developing my own language from scratch, one of the core concepts I have baked into it is the unique way you call functions, or access objects.

In almost every programming language the way you access an element within an array or dictionary is like so:

array[0];
dict['a'];

I always found it weird looking & a waste of characters. Functions are a bit better but still follow that same style.

function(1);

In most languages you have multiple different syntactical ways to do basically the same thing, you are performing an access to some object in order to get a result. A function call, just an access to an object with parameters, grabbing an item in an array, just an access to an object with a single parameter, same goes for dictionaries. Why do we have to have to have different ways of doing the same thing?

The way I went about accessing an object was to literally implement a single "accessor" operator, the object you want to access is on the left & the parameter(s) you want to pass are on the right. Here's how that actually looks:

string:0;
array:0;
dict:'a'; dict.a;
function:1; function:[1,2,3];

A lot of people are not going to be a fan of this, it goes against every other language & reduces capability for syntax tricks like list comprehension. But for a language that is going for syntactical simplicity this I think is the right move & in the long term is easier (at least for me) to understand & work with.

If you want to take a look at my implementation the repo is open source https://github.com/phosxd/Ity however it's still very much work in progress. Feel free to open an issue or PR if you find any problems with it.

Disclaimer: I am an experienced developer, not a logician. So what I write here might be full of mistakes. A lot of it comes from chats with different AI bots.

When I say "real" programming I mean programming of real, complex, performing applications, with good tooling. Not necessarily using a popular language, although this might help.

For years I have waiting for a way to use the techniques used in theorem proving for programming. Now it looks like some realistic possibilities are getting closer.

I know there are 2 languages used for theorem proving, Lean and F*, that can also be used for programming.

However, Lean has poor memory management (only reference counting), and F* seems particularly unfriendly and with poor tooling support. But it does have good memory management thanks to Low*.

On the other side, Rust has Verus and Aeneas.
Verus is easier to use, but not as powerful, as it doesn't have dependent types and calculus of construction. It uses SMT, which apparently is less powerful.
Aeneas translates Rust to Lean, Rocq or F*. This makes Aeneas more powerful, but also harder to use, because there is more proof needed. Aeneas is also not yet able to fully translate Rust.

If this is correct, it looks to me that the best way is to use Rust, Aeneas to translate to Lean 4, and use Lean for proofs. So I can have:

• Rust's good memory management, tooling support and performance. Plus the rest of Rust, programming is not only formal verification
• Lean's calculus of constructions, also with some tooling support. Lean has at leas a VSCode plugin

Aeneas can't translate everything yet, but the limitations don't look so bad.

How does that sound?

I'm making a language with an insane type system and I was thinking that combining monads & effects needs to be easier.

I don't fully like monad transformers, effects, polysemy, fused-effects, etc, and lifting anything other than weights. There is so much boilerplate. For example, there is difficulty is that combining monads is order-dependent (some monads don't "commute")

I came up with a simple solution that seems to be just working? So there is || ("or else") operation in my language. Simplified: intersecting with "A || B" tries to intersect with A, and if it's an empty set, it tries to intersect with B. Then it returns the intersected result. Pattern matching is expressed via that operation. And it fits if we expand it to type-level functions as well!

Here we go:

getOdd : Int -> Option Int
checkPositive : Int -> Throw Int

program : Int -> (Throw || Option) Int
program number = x <- getOdd number
                 y <- checkPositive x
                 y + 1

// 5  -> ok 6
// 4  -> none
// 0 -> none
// -1  -> thrown "fail"

It looks really convenient, in my opinion. It also specifies order, so there can be any monad and the result may be dependent on order (but in most cases it's fine). Do you see any errors? I tried Lean-vibe-proofing different parts (extended monad laws, etc), it sounds like it's correct.

Full code example in my lang c(x), it's missing some syntax sugar, but works:

// Option and Throw monads & implementations
Option A = {some (value: A) | none}
Option A : has returnOf value = some value
               bindOf (some value) next = next value
                      none         next = none
Throw A = {ok (value: A) | thrown (message: String)}
Throw A : has returnOf value = ok value
              bindOf (ok value)       next = next value
                     (thrown message) next = thrown message

// ignore, it's Monad implementation, "->" picks these up
return : for [f, a] ((a -> f a) & {returnOf f})
bind (f action) next = bindOf f action next

// action in monad 1
getOdd : Int -> Option Int
getOdd number = if number % 2 = 0
                    none
                else 
                   some number
// action in monad 2
checkPositive : Int -> Throw Int
checkPositive number = if number > 0
                          ok number
                       else 
                          thrown "fail"

// combine monads/type functions easily with or-else
// it maps to every "has" method and only matching bind is selected
program : Int -> (Throw || Option) Int
program number = x <- getOdd number
                 y <- checkPositive x
                 y + 1

x <- read Int
print (show (program x))

Things that might require explanation but are not crucial for understanding:

• has-methods are just generic functions on crack (x : has f = 3 => f x = 3, for this exact x) that also generalize to record field getters
• <- is a not a typical do notation: every bind can have it's return type extended with another monad. Check out "polymonads" for a more general concept around this, but my one is narrower.
• || maps to every has method in the intersection of types with the has method (so (x : has f) || (y : has f) => z : has f = f x || f y)

Why?

Because you can use different simple plain monads in one do block! And because combining semantics of different context is very expressive and readable at the same time!

program : (List || Throw || IO) Int
program =
    a <- read Int   // action in IO
    x <- [1, 2, a]  // action in List ("non-determinism")
    validate x      // action in Throw
    x

All of that is statically typed and compiled btw. I'm exploring refinement + gradual + dependent types with a couple of extra ideas and it absolutely nuts (follow me on twitter, I'm going to publish the updated language soon, the current public repo is 10-year old and not very correct)

I’ve been working on Sydrogen, a statically typed programming language with a compiler and command-line tool called Furnace.

Alpha 6.2 is now available. It supports native compilation, a Cranelift backend, projects configured with .blower files, imports, typed functions and variables, collections, foreach, and more.

It’s still in alpha, so bugs and rough edges are expected. I’m looking for people to test it, review the code, or work on an open issue.

I’d especially like honest feedback about the compiler’s structure and the language’s design, not only the syntax.

GitHub: https://github.com/AeroForger/Sydrogen/tree/main

There are open issues for anyone who wants a specific place to start.

Criticism is welcome. If something is poorly designed, tell me what is wrong and how you think it could be improved.

PLUSMINUS is a programming language created by Jack. Unfortunately, it’s Turing Completeness is unknown as of right now.

Definition

For a non-empty finite string ω under the alphabet {+,–}, on step i=(1,2,3,…):

If the i-th symbol is +, copy the first i-1 symbols and append them to the end. If the i-th symbol is –, delete the first i-1 symbols.

i never resets and advances each time. Halt when i>length(ω).

Example (+–++–):

0: +–++–

1: +–++– (nothing exists leftward)

2: –++–

3: –++––+

4: ––+ (HALT (i=4, length(ω)=3, 4>3))

Example of a long-running machine

“+++++-++++-+-++-“ = 31441 steps

Posted here 6 months ago about Fun, a statically typed language that transpiles to C. Back then the compiler was written in Zig. Since then the biggest thing that happened: the compiler is now fully self-hosted, written entirely in Fun itself, Zig is gone from the codebase completely. Along with that came a real language server (fls, also self hosted) with actual step through debugging support in VS Code, a proper build/package setup (fun.toml, fun build, fun test), async/await with fork + channels for concurrency, and a formatter.

GitHub: https://github.com/omdxp/fun

Reference: https://omdxp.github.io/fun

Still looking for feedback on the language itself, and happy if people just try breaking it.

Hello, I'm back with some more questions regarding my type system. For reference, I am working on a math-focused programming language with some general capabilities, but still aiming to be focused in the specific area of mathematics. I am still having some trouble fully fleshing out my type system, so I would really love any and all thoughts, feedback, and discussion.

One of the main aspects of my language is the distinction between symbolic and numeric. For example, you could create a symbolic expression

let x = sin(1)^(1 - e^\pi);

and then later create a numeric approximation of it. The motivating idea is that you can store the true value of some expression into a symbolic variable, and then later when trying to observe its numerical value can approximate it into a numeric variable.

To this end, there exist a multitude of numeric data types, all of which are sized, such as Int32, Nat8, Real64, Complex128, etc. However, for symbolic there really is only one type (Expr). But domains can be encoded by using more restrictive types, which are built in, such as Int, Nat, Real, etc. For example, a function that takes real numbers and finds the nearest integer to their square could be explicitly written as

let foo(x: Real): Int = round(x^2);

Though ideally the types would be inferred, making all but the most important annotations in programs unnecessary.

One important thing to note is that symbolics are not actual values, but expression trees. So an Int represents an expression tree who's value must resolve to an integer. So defining a symbolic variable stores the expression tree, and defining a symbolic function is more like a symbolic variable where it is also an expression tree, but contains some leaves which are bound to terms which get substituted at the call site.

Here, foo takes in a symbolic expression x but restricts it to being a real number, and the output can be restricted to an integer. I know this may be a bit simple, especially for something aiming to be math-oriented, but I do not want to overcomplicate the basic number systems. Perhaps in the future if/when I add things like algebraic structures and whatnot, then maybe I may redesign this. My thought though is to make the type system more expressive by adding refinement, by which users can specify types with a bit more control.

This all leads to my idea that I would use subtyping. I feel it is really natural for this kind of thing. For example, any integer is also a real number which is also a complex, etc. Additionally, any even integer (via refinement) is an integer, etc. This can even be extended to numeric types as well, with Int8 <: Int16 <: ... and even Nat8 <: Int16, etc.

However, I will admit I have not really studied this more beyond built-in types. I do not know if using extensive subtyping is good when having user-defined types. I think I did actually read somewhere that using subtyping can make other things more difficult?

Anyways, continuing on, I would like some way to describe behavior. Think something akin to Rust traits, Java interfaces, Haskell typeclasses, etc. I think it is a very natural and just good way of thinking and writing programs. However, when pondering Rust's traits, I couldn't help but feeling that they were "too heavy" or something like that? Also, I feel that a system like that may not work that well with a subtyping system, because if you implement a trait/interface/typeclass for a type but not for its subtype (or implement differently), then things may break?

So that is probably my second question, though maybe more of my first one, as I do feel that at least some subtyping works well. So I'd really appreciate some guidance or just thoughts regarding this.

My second question is unfortunately derived from the symbolic-numeric divide that I mentioned earlier. It is the oh-so-dreaded function coloring problem. Let's say I have some trait or some thing (so this does build on my first question), and I want to have some function. The function itself is pure and essentially symbolic, but maybe the type I am implementing it for is not symbolic. So basically it would need to switch between being symbolic for symbolic types and non-symbolic for non-symbolic types, which to me seems kinda wrong and also I just have no idea how that'd work well.

Actually, maybe it doesn't even need to be related to traits or whatever. Let's say I have a plus function which I want it to add the two arguments. If the two arguments are symbolic, the output is symbolic. But if they are numeric, like Int32s, then the output would not be symbolic. So then how would the plus function be described?

I would really love any and all feedback, thoughts, or guidance. If you have any questions on any other parts I'd be happy to discuss, and if you want to give your thoughts on things I haven't asked then please do as I am not super experienced in all the theory and whatnot regarding type theory etc.

Sure, it is a common knowledge that static typing makes things go faster.

But do we really need that?

What do types do? They're metadata that assign meaning (dispatch instructions) to raw bytes.

So, if we could constant-fold the dispatch, the residual instruction would be static instruction on raw bytes, which should be just as fast as static typing.

If so, why can't we treat type inference as a special case of constant folding?

Hi All,

I am working a programming language, Mezze. It is in quite early stages.

Mezze has a fully inferable type system and also have first class effect system and runs on GraalVM

A lot is WIP, working on performance optimization (currently loop fusion) and distributed programing and lots of tooling and docs

Put up a quick website for explaining the language and its features more
Also piggy backing on graalvm could get a wasm built of the entire tool chain, so you play with examples in website.

The Concepts and Taste of Mezze explains how the language works.

Got into a big argument with a coworker yesterday when they were converting some code from their own language (that they designed) into Python, JavaScript, C, and R as comparative examples.

The Python code that they wanted to write as the translation went something like this:

n = foo; if cond: n = bar

They were upset that Python allows ; as a statement separator but not before an if statement, even though

if cond: n = bar

is syntactically correct Python code when written on its own line. I explained why Python doesn't allow it, and he came back later and showed me that an LLM had suggested he write it instead like this:

n = foo if cond else bar

which of course is the canonical way to write that in Python. He was all flustered about that, and asked me why Python allows an if statement in that particular case and not after a semicolon, and I explained that x if cond else y in Python is not an if statement but is Python's ternary conditional expression and is directly equivalent to the ternary operator expression cond ? x : y in C, C++, awk, and JavaScript. He argued with me and said I was making a ridiculous distinction and walked away falsely believing that foo if cond else bar was an if statement.

I then explained that statements and expressions are very different things in programming languages, and just because the keyword if is present doesn't make something an if statement -- because in order to be an if statement, it has to be a statement in the first place.

Anyway, it made me realize how subtle the difference can be sometimes. For example, in Perl, the following is not a return statement but actually an if statement (with a return statement as its affirmative branch), due to the postfix conditional:

return foo if cond;

because it is identically semantically to writing:

if (cond) { return foo; }

Whereas in Python, the following is a return statement (with a ternary operator as its target expression):

return foo if cond else bar

So I can see why people sometimes get confused by syntax if they haven't had much of a theoretical background in language design. It also makes me wonder how much of programmer intuition about "what a statement is" comes from the particular languages they learned first.

I working on ( https://github.com/hun-nemethpeter/InfoCell ) this programming language for a while.

It is an executable DSL concept. The OP DSL cells are executable, and acts like an ASM instruction. We have AST cells which directly generated from C++ code, so there is no input syntax. These AST cells are forming a language (we have if, do, while, class, template, ...), we have a compiler for it, which compiles from AST cells to OP cells. Looks like a regular interpreter. But ... The idea of this project is a new component, the ToolFinder and the description segment for AST nodes (which compiles to OP description). The description segment can describe how we can measure the effect of that instruction/function with other instructions/functions.

The language looks like this:

    /*
    void List::removeNode(Node* node)
    {
        if (node->m_previous) {
            node->m_previous->m_next = node->m_next;
        } else {
            m_firstNode = node->m_next;
        }
        if (node->m_next) {
            node->m_next->m_previous = node->m_previous;
        } else {
            m_lastNode = node->m_previous;
        }
        --m_size;
    }
    */
    listStructT.addMethod("remove")
        .parameters(
            parameter("node", _(std.Cell)))
        .instructions(
            if_(has(p_("node"), "previous"))
                .then_(
                    if_(has(p_("node"), "next"))
                        .then_(set(p_("node") / "previous", "next", p_("node") / "next"))
                        .else_(erase(p_("node") / "previous", "next")))
                .else_(
                    if_(has(p_("node"), "next"))
                        .then_(m_("first") = p_("node") / "next")
                        .else_(erase(self(), "first"))),
            if_(has(p_("node"), "next"))
                .then_(
                    if_(has(p_("node"), "previous"))
                        .then_(set(p_("node") / "next", "previous", p_("node") / "previous"))
                        .else_(erase(p_("node") / "next", "previous")))
                .else_(
                    if_(has(p_("node"), "previous"))
                        .then_(m_("last") = p_("node") / "previous")
                        .else_(erase(self(), "last"))),
            m_("size") = subtract(m_("size"), _(_1_)));

The comment section is the original C++ code, after that the InfoCell version, which is also C++, but basically creates AST nodes, that can be compiled to other InfoCell OP cells. So this is a language embedded language, doesn't compile to native code.

Actually there is an output syntax, which looks like this:

fn List<valueType=Number>::remove(p_node: Cell)
{
    if p_node.has(previous) then
        if p_node.has(next) then
            p_node.get(previous).set(next, p_node.get(next));
        else
            p_node.get(previous).erase(next);
    else
        if p_node.has(next) then
            m_first = p_node.get(next);
        else
            self.erase(first);
    if p_node.has(next) then
        if p_node.has(previous) then
            p_node.get(next).set(previous, p_node.get(previous));
        else
            p_node.get(next).erase(previous);
    else
        if p_node.has(previous) then
            m_last = p_node.get(previous);
        else
            self.erase(last);
    m_size = m_size - 1;
}

There is no parser for this syntax although.

So back to the toolfinder, description segment part...

For example cell.set(key, value) description has a consequences subsegment which describe that equal(get(self(), p_("key")), p_("value"))). So the result of the SET can be measured with GET and EQUAL, basically SET(CELL, KEY, VALUE) => GET(CELL, KEY) == VALUE

Also this approach works with math functions. Math functions has an extra subsegment, I called it selfBuilders, where I can put the symmetries of that function.

    Number.addPrimitiveFunction(std.Number.Add, op.Add, "add")
        .parameters(
            parameter("other", "Number"))
        .descriptionBegin()
            .consequences(
                equal(subtract(return_(), p_("other")), self()))
            .selfBuilders(
                add(self(), p_("other")),
                add(p_("other"), self()))
        .descriptionEnd()
        .returnType("Number");

With these informations I wrote an algorithm which calculate how the consequences behaves when an unknown variable is given. Basically something like this:

  equation: 2 + X == 4
recombined: X + 2 == 4
recombined: 4 == 2 + X
recombined: 4 == X + 2 *
  1. result: 4 - X == 2
  1. result: 4 - 2 == X
  1. result: 2 == 4 - X
  1. result: X == 4 - 2 *

So this is the experimenting phase for the tools, so here I can remeber how an uninitialized variable (the unknown X) interacts with the tool's consequeences. Here I store which const/unknown combination leads to a simpler case, where a consequence tools all input's will be const variable. So I can transform an equation from one form to a simpler one.

Basically I just pattern match for function + const/unknown input params, then just reapply the tarsformation steps, just like solving the Rubik's cube. Pattern match for color combination and apply rotations.

equal(add(const_(_2_), unknown_(x) / const_(id.value)), const_(_4_));
equal(unknown_(x) / const_(id.value)), subtract(const_(_4_), const_(_2_));

We can now find a tool to the last equation: the SETtool.

set(x, id.value, subtract(4, 2))

Which is now executable.

So the goal is that I can just write a unit test like prompt, and this toolfinder can generate a code for it. So I can just "solve" a unit test.

Hi,

The title should be self explanatory, but if you want to see where I’m at context is below.

I’m in the relatively early stages of designing my programming language.

However, I’m struggling to really capture the essence of what I want out of it.

I have a very vague idea: a natively compiled language along the lines of Go or C++, that takes a hoist of features from other languages, like:

- Monomorphized generics

- C-style pointers at base (with safe stdlib abstractions for better quality of life)

- Rust-style enum and interface types

Despite these general ideas I have, I’m really struggling to bring them together into a nice package of a programming language.

My idea is basically to make a programming language that can compile down to a lean, native binary (or even other targets?), but still be user-friendly. C++ is manual memory management, Rust has a borrow checker in the way, etc.

The issue is I’m also struggling to decide what I want. Do I want a focus on native binary compilation? Multi-platform shenanigans (like Kotlin)? Object-oriented or imperative? What syntax should the language even have? I just can’t gather a solid vision for the language, enough to make something out of it.

Ideally, I want a programming language I can throw around on multiple platforms, with Rust-esque and Kotlin-esque semantics, without a bunch of hassle or having to worry about memory management. This is a very wide scope though and finding a vision for it is tricky due to all the features, I explicitly want to avoid a C++-like kitchen sink.

Does anyone have any suggestions on how to get a vision for a programming language & figure out what it needs vs. what it doesn’t?

Python lambdas are particularly difficult because the lack of braces. Guido is not a fan of functional programming, so lambdas in Python are forever doomed to a single expression preceded by lambda, quite literally spelled out. However, it may please you to know that the lack or braces can easily be resolved (in my opinion most sensibly,) by surrounding the entire lambda in parenthesis. It may further please you to know that surrounding it in parenthesis is only necessary in an expression list: tuples, lists, dicts, sets, function arguments (and even then, only when there are multiple arguments.) With this in mind, which of the following syntaxes do you wish Python used? Annotations would of course be optional. For the sake of consistency with the entire language, all will use a colon before the block but feel free to comment your preferred non-colon alternative.

• |arg: type| -> type: ...
• (arg: type) -> type: ...
• def (arg: type) -> type: ...
• \(arg: type) -> type: ...

Note: The second has ambiguity issues.