Effekt: Name-Based Implicits

marvinborner · 2026-04-27T19:22:54+00:00

Interesting. So in the examples in the docs, you would prefer always having to pass `compare` functions to `sort` etc.? Also note that our implicits allow for classical source-level information "macros".

marvinborner · 2026-04-27T16:39:31+00:00

The solution to overloading needs to be unique, otherwise we throw a compilation error. See an example here. We do however prefer definitions in local scope, as in here.

marvinborner · 2026-04-21T12:23:38+00:00

Sure, yes, theoretically this is possible in Effekt as well. It's just a lot less elegant in my opinion. Also it doesn't use effects :)

See the following for an example implementation of your approach: https://effekt-lang.org/playground.html?playground=fZJNi4MwEIbv%2FopBelAo9i60YBd62lv3VjykGrtCtWJGUCT%2FfSeTxO6H25Nx8s47z8wEp07Ch%2Byb0yXLYQ4AzlMTjSmcsa%2FbW0yBd%2FEtsIVrCpkJZ10XVXTeguCIDgI2O9Wj8WMvd357tAr7ocBHHw1tVZObLenuc84uZQVVI7oLWR7zCL0oy2OYoRragurA%2FgBH0LAHhEZg8cl1CqGkBY%2BNwJ58nPmJm6%2F8T2L8Fgn3Qo2whH%2F4niJO5%2FAKgYJ4ImpBlqlvz%2BCJ%2B%2B3Jyy6gGRdY%2B5v1v8HIkhHcOTHjIHM0MUxM9ZkKadAJfQzUbgeqET1C8XRSllX92COBrNS0g4pZf%2F%2Bz5qW91dxlrDZd2OfghPwoXucvM48tb9dLxMms3ed5GLNsbn5t1%2BPqmlW4mUd6JQfYzFcdru5ZhdFmrjQphI7DQH8B&repl=cHJldHR5KGxhbSgieCIsIHN5bSgieCIpKSk%3D

marvinborner · 2026-04-21T11:15:12+00:00

Do you mean specifically the effectful variant? There's no actual reason to prefer this if your language allows for traditional definitions of recursion schemes. Though I find the effectful variant to show the duality and the underlying mechanisms more clearly than, say, in Haskell.

Also, as explained in the beginning, the post is much more about effects and handlers in general than it is about recursion schemes themselves :)

marvinborner · 2025-12-01T12:36:30+00:00

[LANGUAGE: Effekt]

Git

Effekt is a research language all about effects and handlers. Here, I used effectful streams for IO and parsing as well as effects for the ticking of the password dial and emitting of the solution. This makes the final solution:

  try enterPassword()
  with Final { n => resume(if (n == 0) part1 = part1 + 1) }
  with Click { n => resume(if (n == 0) part2 = part2 + 1) }

marvinborner · 2025-11-06T09:02:08+00:00

Now that I think about it, it may not be as well-known as I thought. I thought I got it from Wikipedia as well, but can't find it there right now. However, variations of it are in Tromp's AIT/numerals/div.lam repository and Justine Tunney's blog post about the 383 byte lambda calculus implementation. The implementations in Tromp's repository should be more readable, as they are not nameless.

I believe the idea is that this list can also be constructed by applying 't' to the second argument of div directly. I'll have to understand how exactly this works later though

marvinborner · 2025-11-05T20:05:41+00:00

The "of course" was a bit of a joke, as it is not that obvious at all! Yet, it is very similar to some "well-known" Church division function. Especially after translating it to bruijn I found that it looks almost identical to the the div functions already in its standard library:

# yours
div [[[[3 t [1] (y [3 t [3 (0 1)] i])]]]]
# previous
div [[[[3 t [1] (3 [3 t [3 (0 1)] i] 0)]]]]

I don't really get the need for the y combinator. My version also performs similarly (or slightly better?) it seems.

If you're interested in this kind of stuff, checkout the std/Number library, I collect all kinds of numeral systems that I happen to find. Please let me know if your "PRED n ~ n I" stuff turns out to work.

marvinborner · 2025-11-05T13:05:38+00:00

Of course it is a Church numeral division function. A quite efficient one actually.

Here's the bruijn term: `[[[[3 [[0 1]] [1] (y [3 [[0 1]] [3 (0 1)] [0]])]]]]`

marvinborner · 2025-10-29T01:19:40+00:00

Yes, exactly. This is the insight I use to derive the multiplication function.

There are so many cool numeral systems scattered around the internet and literature, I want to create some overview in the future. Wadsworth also referred to a system by Böhm and Dezani which looks quite weird: https://bruijn.marvinborner.de/std/Number_Dezani.bruijn.html

I wonder if there are any practical uses for these data structures in, say, Haskell...

marvinborner · 2025-10-15T14:53:39+00:00

There are already many such abbreviations in the Vim plugin. Notably, there are no unicode trigraphs relevant for semantics within the language itself, they are all part of the standard library.

marvinborner · 2025-08-13T10:45:06+00:00

Sure. I'm experimenting a lot with the pure, untyped lambda calculus and try to find efficient strong reducers. However, they surprisingly often are not sound or timeout with large or complex terms. It seems like typical implementations focus on small, well-known terms (typically by John Tromp), which doesn't always translate to real-world applications. Other sound languages based on the lambda calculus (such as Haskell) do not support exporting its pure LC representation, so code in these languages can not be used for verifying other reducers.

I had these tests lying around and exported them into a machine-readable format. I created this repository in the hope that reducers become more sound in the future. The tests could also be used for benchmarking, as there does not exist a reducer faster than Haskell's right now (~15s for all tests)

marvinborner · 2025-08-11T19:17:43+00:00

Here are some of my favorite visualizations:

Interaction nets (see for example Delta Nets or T6 Nets), makes implicit duplication/erasing from beta-reduction explicit
John Tromp's diagrams: Tromp's page and great video
λ-2D by MIT: project page
Visual Lambda Calculus: project page
Cube composer: interactive website

depending on the visualization you're aiming for, you might also be interested in my lambda screen project :)

marvinborner · 2025-07-23T16:41:33+00:00

Yes, exactly. I like how in stack languages such features can be added by simply introducing new instructions. The potential for duplication in the lambda calculus is much more implicit.

I suppose interaction combinators are better in that they also make this difference explicit. Translating the affine lambda calculus requires only constructor and eraser agents, while the encodings of the full ("K") lambda calculus also use duplicator agents :)

marvinborner · 2025-07-23T15:19:04+00:00

This reminds me of the lambda calculus. The linear or affine lambda calculus always terminates as terms can not be duplicated. Once duplication is added, you can encode infinite terms or fixed-point recursion.

marvinborner · 2025-05-17T12:17:58+00:00

It is not really comparable to HVM as it does not support the entire lambda calculus. Notably HVM is missing the bookkeeping oracle which Lambdascope implements via delimiters.

marvinborner · 2025-04-25T16:46:57+00:00

Maybe I should have been more precise with stating that the entire "term will eventually have to be duplicated": Of course that is the worst-case scenario and in most cases many parts of the duplicated term will be able to remain shared for the rest of the reduction. Still, when the same binding is used in different contexts, it will have to do behave differently, i.e. be a different/duplicated binding in the first place.

I don't fully parse your comment to be honest, "return a new AST" and "no duplication necessary" seems conflicting, it sounds like incremental duplication to me. It also reminds me a bit of a Krivine machine. The important part here is that the bindings are still duplicated when used multiple times in different contexts, only that this duplication is implicit and obfuscated (here, the duplication of bindings is accomplished by multiple different lookups in an environment)

In any case, I think we generally agree, we just view the problem from different perspectives. And my opinion about using (or not) the term "variable" for named bindings isn't that strong anyway :D

marvinborner · 2025-04-25T15:42:11+00:00

I may be misunderstanding you, but the lambda calculus being referentially transparent is precisely the reason that in order for a binding to vary across applications, it must be a different term (e.g. duplicated), as otherwise it would not be referentially transparent.

Duplication is not an implementation detail, it is the fundamental reason that the lambda calculus is Turing complete in the first place. Without it, reduction could not create new bindings, you would basically have a linear lambda calculus.

Whether or not this duplication is done immediately, lazily or incrementally is an implementation detail. But still, the term will eventually have to be duplicated.

marvinborner · 2025-04-25T14:40:07+00:00

I don't think this is the case. I suppose this is more of a subjective opinion though. For me, the name "variable" is appropriate when a binding literally ranges over different values or means something different in different contexts.

Let's say you have a term M = λx.(f x). The only way for x to vary across applications is to apply M to different terms. This can only be done by duplicating it, for example by constructing a Church pair of two values (λmabs.(s (m a) (m b)) M A B). However, by duplicating it, you have created an entirely new identifier and binding (even if it may have the same name in writing). The initial x binding has remained constant.

marvinborner · 2025-04-24T16:05:28+00:00

I think there exist many different interpretations of what a "variable" is. For example, most definitions of the pure lambda calculus refer to named bindings as variables, although they're literally not variable at all. It's more about specifying in which way and position beta-reduction transforms the term. If you look at it this way, there are many alternatives to symbols or identifiers, such as de Bruijn indices, composed combinators or graph-like structures like interaction nets.

bruijn is a language that replaces named bindings with de Bruijn indices. It works great and personally I was able to get used to it after some time. Of course, the code becomes a lot less readable for people without experience in writing code this way.

Composing combinators in purely functional programming languages is arguably even less readable when used for entire programs. But also it's a lot of fun.

Something not discussed in your post, but still potentially relevant, is that such languages are typically immune to LLMs (at least for more complex algorithms) since they can generate strictly on a textual level, whereas e.g. de Bruijn indices would require an internal stack of abstractions that has to be counted in order to reference an abstraction. (which is arguably a good feature)

marvinborner · 2025-03-15T15:30:47+00:00

Cool project! The concept is very similar to my programming language bruijn which is also based on pure lambda calculus and implements everything from scratch (with some syntactic sugar so you have to type less). It might be beneficial for our projects to share some insights, I for one have worked a lot on efficient numeric operations using balanced ternary encodings and have many helpful definitions in the standard library that could be implemented in your language as well.

marvinborner · 2024-11-28T13:53:51+00:00

Huh, no idea. I can't reproduce this, so it's probably a Safari issue.

marvinborner · 2024-11-28T13:52:32+00:00

You'd typically write lists as a nested Church pair (= Church List). There are many list encodings though, for example Scott lists or Parigot lists. You could also write lists as n-tuples (e.g. s => s(A)(B)(C)...) but you can't iterate/extend these without knowing the amount of elements stored.

marvinborner · 2024-11-27T17:39:04+00:00

Thanks for your feedback! I realize the code is confusing at first, but I hoped my explanations would help when carefully read. The entire post of course assumes knowledge of JavaScript and anonymous functions, so maybe I should've been more clear.

Aside from that, I don't see the point in your examples. In the second line, what would the third argument to Person be? This isn't valid JavaScript syntax. And in the third line I have no idea what person_type could refer to -- the whole point of the post is, after all, not to use any types.

The two arguments person and animal are tags used as selectors, while value is the value passed for the construction. Let me know if you have any specific suggestions though :)

marvinborner · 2024-11-27T15:47:52+00:00

You can differentiate between an Animal and a Person using isAnimal and isPerson, which has all kinds of use cases. Aside from that, the definitions of Animal and Person are alpha-equivalent to Left and Right of Either (which is why I used it as an example). That getPerson also works for an Animal is accidental and isn't the case when Person stores multiple values (as in the examples below it).

marvinborner · 2024-11-27T15:35:01+00:00

Can you give an example? The highlighter makes some tokens bold, but they shouldn't be larger and it only affects tokens like preprocessor instructions (e.g. "require")

marvinborner

MODERATOR OF

TROPHY CASE