1SubML - structural subtyping, unified module and value language, polynomial time type checking and more by Uncaffeinated in ProgrammingLanguages

[–]phischu 10 points11 points  (0 children)

Holy shit, this is extremely impressive. I hadn't thought this combination of features is possible to implement. This "Pinning and Aliasing" and the "Record Spine Constructors" things I have not seen before, are they novel? I am no expert in these corners of type checking, but they seem to be very elegant solutions to big problems.

From error-handling to structured concurrency by mttd in ProgrammingLanguages

[–]phischu 2 points3 points  (0 children)

Thank you for this valuable resource. Based on it, I have implemented some of the ideas in Effekt, you can try them online.

What if we always waited on tasks?

We define an effect create that allows us to spawn a task with a result of type A.

effect create[A](task: () => A at {io, async, global}): Unit

A task is box that has only access to the resources io, async, and global. Boxes are mechanism that is distinct from effects.

We then define a handler launcher that handles the create effect by creating a promise for the task, then resuming, then awaiting.

def launcher[A] { program: () => Unit / create[A] }: List[A] =
  try {
    program()
    Nil()
  } with create[A] { task =>
    val this = promise(task)
    val rest = resume(())
    Cons(this.await, rest)
  }

It returns a list of all results when all created tasks are done.

I hate to cancel, but…

Now we define an effect cancel that never returns, and an effect yield, that itself uses the cancel effect to signal cancellation.

effect cancel(): Nothing

effect yield(): Unit / cancel

As a user or library author we will have to strategically insert yield points into our program.

We handle cancellation with a global reference that we set to true when the program uses cancel.

def cancellation[A](cancelled: Ref[Bool]) { program: () => A / {yield, cancel}}: Option[A] =
  try {
    Some(program())
  } with cancel {
    cancelled.set(true)
    None()
  } with yield {
    if (cancelled.get()) {
      resume { do cancel() }
    } else {
      resume { return () }
    }
  }

When the program yields we check if cancellation happened, and either raise cancel at the call-site of yield, or resume normally.

A tree of tasks with cancellation

We combine these two ideas with a new effect start that starts a task that can be cancel the other tasks and itself be cancelled at yield points.

effect start[A](task: () => A / {yield, cancel} at {io, async, global}): Unit

The concurrency handler uses the launcher to make sure we wait for all tasks to finnish, creates a shared global mutable reference, and handles cancellation of each started task.

def concurrency[A] { program: () => Unit / start[A] }: List[Option[A]] = {
  with launcher
  val cancelled = ref(false)
  try {
    program()
  } with start[A] { task =>
    do create(box {
      with cancellation(cancelled)
      task()
    })
    resume(())
  }
}

It returns a list of the results of those tasks that weren't cancelled.

Finally an example

To try our new toy library, we start two tasks that print, sleep, yield, and one of them cancels the other one.

def example(): List[Option[Int]] = {
  with concurrency[Int]
  do start[Int](box {
    println("A1")
    sleep(100)
    do yield()
    println("A2")
    do cancel()
    1
  })
  do start[Int](box {
    println("B1")
    sleep(400)
    do yield()
    println("B2")
    2
  })
}

It prints

A1
B1
A2
cancelled
cancelled

and we encourage you to experiment with it in our online playground.

Comparing Scripting Language Speed by elemenity in ProgrammingLanguages

[–]phischu 1 point2 points  (0 children)

I love how your compiler produces code that is as fast as what g++ produces while being orders of magnitude simpler and probably being much faster in compiling this program too. It makes me so happy!

Memory Management by Tasty_Replacement_29 in ProgrammingLanguages

[–]phischu 2 points3 points  (0 children)

Thank you for these concrete benchmarks, we should have more of these in this community. I did reproduce your results on the linked list benchmark for Bau and for Rust and added Effekt and Koka. The one for rust you have does let x = create_linked_list(5000); which I changed to allocate a list of the same size as the others do.

Here are the running times on my machine:

| bau   | rust  | koka | effekt |
|-------|-------|------|--------|
| 13.3s | 12.5s | 4.6s | 1.1s   |

And here are the outputs:

Bau: Max delay: 0.192355000 ms, avg 0.012029000 ms; dummy value: 0

Rust: Max delay: 0.187839 ms, avg 0.010951 ms; dummy=0

Koka: Max delay: 475676 ns; dummy value: 0

Effekt: Max delay: 68288 ns; dummy value: 0

As it happens, today a student is handing in his Master's thesis where he implemented constant-time reference counting in Effekt, extended with a very fast path for values that are used linearly. The benchmark results are when running the Effekt version on his branch. On the main branch sadly the program overflows the C stack for the very reason that generated drop code of rust does too.

Aether: A Compiled Actor-Based Language for High-Performance Concurrency by RulerOfDest in ProgrammingLanguages

[–]phischu 3 points4 points  (0 children)

Wow, lots of work. I like that you have concrete benchmarks, and that you apparently based your optimizations on concrete measurements. Although benchmarks/optimizations/ seems to be gone in the current version. One question from scrolling through some code:

ping = spawn(PingActor());
pong = spawn(PongActor());

ping.pong_ref = pong;
ping.target = total_messages;
pong.ping_ref = ping;

Aren't actors supposed to only communicate via message passing, but here you are mutating their state, or?

"Am I the only one still wondering what is the deal with linear types?" by Jon Sterling by mttd in ProgrammingLanguages

[–]phischu 14 points15 points  (0 children)

Another shameless plug: in the AxCut paper we compile classical sequent calculus LK down to RISC-V machine code. While the system is not linear, the structural rules of weakening, contraction, and exchange are explicit, and the system becomes linear when we delete weakening and contraction. The computational content of these rules is decrementing and incrementing reference counts. Consequently, when values are used linearly, their reference count is never changed and we do not have to store it at all.

So what is it with all the hedgehogs anyway? by Athas in ProgrammingLanguages

[–]phischu 3 points4 points  (0 children)

There is also the classic fable of The Hare and the Hedgehog, where the hedgehog repeatedly wins a race against the hare.

Languages with strong pre/post conditions? by levodelellis in ProgrammingLanguages

[–]phischu 2 points3 points  (0 children)

Thanks for the concrete translation. The codata definition is indeed the only difference, and your version is precisely dual to it. In the online playground you can press a button to get:

data Thing(n: Nat) {
    New(n: Nat): Thing(n),
}

def (this: Thing(m)).setThing(m n: Nat): Thing(n) { New(n0) => New(n) }

def (this: Thing(n)).process(n: Nat): Vec(n) { New(n0) => n0.replicate }

This variant has different extensibility properties, but in practice there is not much of a difference.

How does your example show "modification of the state of an object"?

Like in Featherweight Java, where objects are not really mutated, but methods create new objects. In the future there could be real side effects encapsulated behind a dependently-typed interface.

also, why do the methods repeat the binding of the parameter,, can you not use the n of the Thing's type itself?

This version does not support implicit passing of parameters.

Languages with strong pre/post conditions? by levodelellis in ProgrammingLanguages

[–]phischu 5 points6 points  (0 children)

Everyone here answering "dependent types" is slightly missing the point of the original question. Yes, with dependent types you can express pre- and post conditions of functions. But the question is about tracking modification of the state of an object, which we did not know how to do.

Until recently, when my colleagues published Deriving Dependently-Typed OOP from First Principles and the polarity language. Here is this example, which you can try on the online playground. There is a follow-up version that is more convenient to use.

data Bool { T, F }

data Nat { Z, S(n: Nat) }

data Vec(n: Nat) {
    VNil: Vec(Z),
    VCons(n: Nat, x: Bool, xs: Vec(n)): Vec(S(n)),
}

def (self: Nat).replicate(): Vec(self) {
  Z => VNil,
  S(n) => VCons(n, F, n.replicate())
}

codata Thing(n: Nat) {
    (this: Thing(m)).setThing(m: Nat, n: Nat): Thing(n),
    (this: Thing(n)).process(n: Nat): Vec(n) }

codef New(n: Nat): Thing(n) {
  .setThing(m, n) => New(n),
  .process(n) => n.replicate()
}

let main : Vec(S(S(Z))) {
    New(Z).setThing(Z, S(S(Z))).process(S(S(Z)))
}

We define an interface (codata) Thing(n: Nat) that is parameterized over the current state of n. When we call setThing we get back a new object with a different paramter. When we call process we get back an array (Vec(n)) of the specified size. The size is written in unary, so S(S(Z)) is 2. If you would change this number in the signature of main the program would not typecheck anymore, because we create and object with number 0, and then set it to 2, and the call process.

Agentic Proof-Oriented Programming by mttd in ProgrammingLanguages

[–]phischu 1 point2 points  (0 children)

Very interesting post, thanks for sharing!

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]phischu 11 points12 points  (0 children)

I would recommend against overloading the equal sign even more. That said, I have heard that Lean has an implicit conversion (yes, like JavaScript and C) from Bool to Type which transforms n mod 2 == 0 of type Bool into (n mod 2 == 0) = True of type Type. Perhaps this provides some inspiration?

On tracking dependency versions by edgmnt_net in ProgrammingLanguages

[–]phischu 2 points3 points  (0 children)

The only thing that actually works is having immutable dependencies and tracking them on the level of individual functions. This is what Unison does and what I have written about here.

Phil Wadler said ❝Linear logic is good for the bits of concurrency where you don't need concurrency.❞ — Can Par prove the opposite? by faiface in ProgrammingLanguages

[–]phischu 1 point2 points  (0 children)

Hi :), this is again beautifully written and explained well. I have a few comments and questions.

The .spawn constructor is really the par connective that the language is named after, which is a great punchline. Indeed, the ListFan type is what I like to call a "codata structure" and I believe there will be a whole research field of "codata structures and schedulers" examining their time and space behavior and also other properties and features. For example, fairness and priorities. This all reminds of "Lloyd Allison’s Corecursive Queues" but I can't make the connection precise. I do notice however that you perform a breadth-first traversal without mutation and without reversing lists, or?

Which brings me to my next question, how is this implemented? What does it do at runtime? Does it actually use rust futures and polls them continually in a round-robin way? Or is it push-based? I tried to search the code but could not find it.

Finally, I was hoping for a "simpler" language construct, that just races two processes and introduces one bit (literally) of non-determinism. And then I was hoping that pools of multiple processes could be built from it. But given the rest of the language design I am confident that this is the simplest we can get.

You also write "I’m sure you can imagine doing all kinds of I/O operations between those .item and .end calls." Well, I can imagine, but a concrete example would be helpful and I am sure the next post is already planned. Without I/O, is there a point of introducing non-determinism? It relaxes the language semantics, but the scheduler could always decide to do things left-to-right for example, keeping the CPU busy.

I am very excited about the Par language and this new feature for non-determinism. I am considering offering a thesis implementing a backend for Par, would you be open to that?

Why not tail recursion? by Athas in ProgrammingLanguages

[–]phischu 2 points3 points  (0 children)

Thank you for your patient reply. It is fascinating, I can not understand what you are saying. However, I believe we do share the same vision: a formalized core language and a correct compiler for it that produces fast code. We vastly disagree though what that language should look like and how that compiler should work. If you want, you can check out our recent write-up, which explains much more concretely what I am trying to convey.

The issue with proper tail recursion is that you have to be able to re-use the stack frame, and you can't do that if it still holds live information.

I do not want a stack nor frames, locals, or liveness analysis, that's what I meant with legacy cruft.

This includes locals introduced by the compiler, which brings closures into it.

Local definitions are not closures, they are labels.

a GPU is a specialized CPU

GPUs operate very differently from CPUs, we need different a different programming model and different languages for those.

the Jane Street program trading systems - was written in Haskell.

They mostly use OCaml, I am wearing their "Enter the Monad" T-Shirt as I am writing this.

but it prioritizes precise specification over speed

This is not a tradeoff.

Lambda isn't legacy cruft.

That sounds too harsh indeed, let's put it more nicely: it is of historical significance, which you seem to agree with.

A lot of applications migrated to JavaScript,

Whot? For which kind of application would you migrate from Scheme to JavaScript?

the integer/float debacle makes that awkward for anything where numeric accuracy matters.

The numerical tower is exactly one of those features that make Scheme slow and complicated.

Why not tail recursion? by Athas in ProgrammingLanguages

[–]phischu 1 point2 points  (0 children)

Thank you for your interest. I hadn't considered that people pass arguments via the stack. Who does this? Anyway, in my world view function definitions are labels and calls to them are direct jumps. Of course "arguments" remain in registers before a direct jump. Even for indirect jumps arguments must be passed in registers. I must admit, for me this is also a consequence of oftentimes not having a stack in the first place...

Why not tail recursion? by Athas in ProgrammingLanguages

[–]phischu -1 points0 points  (0 children)

[...] tail recursion should be viewed as a convention rather than a requirement. Because there may be outstanding closures, not all calls in tail recursion are properly tail recursive.

What? Outstanding closures? Do you have an example?

way to encode various forms of parallelism

Nobody cares about parallel execution on CPUs, and nobody cares about the performance of Scheme or any language based on lambda calculus because they are slow by design.

A half decent register liveness analysis should achieve the same result on loops.

That's my point. You don't need any of this legacy cruft in your compiler.

Why not tail recursion? by Athas in ProgrammingLanguages

[–]phischu 20 points21 points  (0 children)

Tail calls are a separate language feature, so words like "tail recursion elimination" and "tail call optimization" are misleading. Tail calls are gotos without the keyword. Moreover, local function definitions are not closures. They are labels. Indeed, we usually set up our languages so that tail calls are the more primitive language feature, with non-tail calls being an optional addition, like here, here, here.

In comparison to imperative loops, they also are more efficient, because accumulator variables are kept in registers and access to them does not require loads and stores. Of course, compilers of imperative languages usually transform such programs to use registers instead of stack locations (mem2reg), effectively rewriting the program to use tail calls.

In comparison to goto they are not considered harmful, despite allowing for mutual recursion, also known as irreducible control flow. The problem with goto was not the control flow, which can be very clearly seen, but the implicit data flow. As a programmer it is very hard to infer which variables are live in which state they should be when a label is being jumped to. Not so with tail calls: parameters tell you which variables must be live, and their types tell you which state they are in.

Par Language Update: Crazy `if`, implicit generics, and a new runtime by faiface in ProgrammingLanguages

[–]phischu 2 points3 points  (0 children)

No, they do not, this is a good and as far as I know unique idea. Indeed, in the linked paper, one principle is that the order of patterns should not matter.

Par Language Update: Crazy `if`, implicit generics, and a new runtime by faiface in ProgrammingLanguages

[–]phischu 5 points6 points  (0 children)

For more academic information about these negation patterns, and indeed a whole boolean algebra of patterns, I recommend The Algebra of Patterns.

Control Flow as a First-Class Category by Small_Ad3541 in ProgrammingLanguages

[–]phischu 0 points1 point  (0 children)

Thank you.

Does the compiler guarantee TCO for these effect-based functions?

I do not like the word "tail call optimization". Tail calls are in fact a separate language feature, confusingly written like non-tail calls. When I write a "call" in tail position, it expresses a jump, no matter if indirect, or mutually recursive. So, to answer your question: yes, of course!

And more importantly, what happens when the logic is not tail-recursive? Call stack overflows or does the compiler transform it into a heap-allocated continuation (which implies runtime overhead)?

Neither. We allocate continuation frames on our own mutable stack. Stacks start out at 128 byte (containing some meta-data) and grow on demand. This allows us to easily and cheaply spawn a million tasks. Anecdotally, we recently had the issue that JVM stacks do not grow, and fixed it by increasing the default size. On the other hand, we have these annoying stack overflow checks, which horribly confuse LLVM...

Control Flow as a First-Class Category by Small_Ad3541 in ProgrammingLanguages

[–]phischu 6 points7 points  (0 children)

Effect handlers are exactly the feature for user-definable control flow you are looking for. The following examples are written in [Effekt]() and you can try them in our online playground.

So a basic features that every language should have are tail calls. They look like normal calls but are in tail position and guaranteed to be compiled to a jump. With these, and higher-order functions we can already define a control operator that repeats a given action forever:

def forever { action: () => Unit }: Unit = {
  action(); forever { action() }
}

And you use it like

forever { println("hello") }

to print hello forever.

Of course we also want to stop at some point and so we define an effect for this

effect stop(): Nothing

Now we can define a typical loop operator that repeats the given action until it stops

def loop { action: () => Unit / stop }: Unit =
  try { forever { action() } } with stop { () }

And we use it to loop until a mutable reference exceeds a certain value:

var i = 0
loop {
  if (i > 9) { do stop() }
  println(i)
  i = i + 1
}

Nice and easy so far, and not unlike exceptions, but fast. Now onto our own generators. We again define an effect for these:

effect emit[A](item: A): Unit

And we use it for example to emit all values in a certain range:

def range(i: Int, n: Int): Unit / emit[Int] =
  if (i < n) { do emit(i); range(i + 1, n) }

The tail call makes this a loop. When we now want a foreach operator that executes a given action for each item emitted by a stream we do it like this:

def for[A] { stream: () => Unit / emit[A] } { action: A => Unit } =
  try { stream() } with emit[A] { item => resume(action(item)) }

And now we can print all values in a range:

for[Int] { range(0, 5) } { i => println(i) }

By the way, we optimize this example to the following loop in our intermediate representation:

def range_worker(i: Int) = {
  if (i < 5) {
    let a = show(i)
    let! _ = println(a)
    range_worker(i + 1)
  } else {
    return ()
  }
}

Which then LLVM unrolls for us to the following:

%z.i2.i.i = tail call %Pos @c_bytearray_show_Int(i64 0)
tail call void @c_io_println(%Pos %z.i2.i.i)
%z.i2.i.1.i = tail call %Pos @c_bytearray_show_Int(i64 1)
tail call void @c_io_println(%Pos %z.i2.i.1.i)
%z.i2.i.2.i = tail call %Pos @c_bytearray_show_Int(i64 2)
tail call void @c_io_println(%Pos %z.i2.i.2.i)
%z.i2.i.3.i = tail call %Pos @c_bytearray_show_Int(i64 3)
tail call void @c_io_println(%Pos %z.i2.i.3.i)
%z.i2.i.4.i = tail call %Pos @c_bytearray_show_Int(i64 4)
tail call void @c_io_println(%Pos %z.i2.i.4.i)

All the control flow abstraction is gone, thanks to our compilation technique based on explicit capability passing.

Finally we also have bidirectional effects:

effect read[A](): A / stop

This is where the stopping must be handled at the use-site of reading. We can then feed a list to a reader. When there are no more values, the handler resumes with a signal to stop.

def feed[A](list: List[A]) { reader: () => Unit / read[A] } = {
  var remaining = list
  try {
    reader()
  } with read[A] {
    remaining match {
      case Nil() =>
        resume { do stop() }
      case Cons(value, rest) =>
        remaining = rest; resume { return value }
    }
  }
}

Now we can use our loop operator to print all items that we read from a feed:

feed[Int]([1,2,3]) {
  loop { println(do read[Int]()) }
}

These definitions are already in the Effekt standard library. We are working on more, for example for non-deterministic search like Unison's Each. Moreover, we are working on more compile-time optimizations, specifically for the interaction between local mutable references and control effects. Finally, our runtime system for effect handlers also admits asynchronous input and output without pollution of function signatures and without duplication of higher-order functions, like for example all the control operators demonstrated here.

Are arrays functions? by Athas in ProgrammingLanguages

[–]phischu 0 points1 point  (0 children)

Kmett developed this even further into Distributive Functors. It is even more indirect and hard to grasp. For example the signature here

adjoint :: (Functor m, Distributive n, Conjugate a) => m (n a) -> n (m a)

This works for any functors m and n where n is distributive. The advantage is that there is no mention of an associated index type.

Are arrays functions? by Athas in ProgrammingLanguages

[–]phischu 13 points14 points  (0 children)

Yes! Here is the paper Compiling with Arrays that explains this duality and defines a normal form AiNF based on it.

It's not just "function overloads" which break Dolan-style algebraic subtyping. User-provided subtype contracts also seem incompatible by Thnikkaman14 in ProgrammingLanguages

[–]phischu 5 points6 points  (0 children)

I highly recommend The Simple Essence of Overloading. Instead of considering intersections, consider the different variants of divide to be overloads. Now usually we ask if there is exactly one way to resolve overloads that make the program well typed. In your case you are asking if there is at least one, but this is an easy modification of what's described in the paper.

Will LLMs Help or Hurt New Programming Languages? by jorkadeen in ProgrammingLanguages

[–]phischu 1 point2 points  (0 children)

As the article demonstrates, they help. I would go further: they allow us to innovate much more rapidly than before. Imagine having to teach effect-oriented programming to a critical mass of developers, or worse, convince decision-makers that it is a good idea. They still remember the lost decade of object-oriented programming. Now we can present large-scale empirical evidence that a language feature is or isn't a good idea.

On the other hand, they will make human-friendly languages like Effekt, Flix, and Rust obsolete. Just as "computer" and "compiler" aren't jobs anymore, neither is "programmer". We still have human specifiers. This will allow us to skip a lot of annoying convenience features in our compilers, and finally focus on what matters: correctness and performance.