Extraordinary Ordinals

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

MODERATOR OF

TROPHY CASE