Overloading the lambda abstraction in Haskell (2022)

The fun thing is that this sounds like "just" a more type-safe version of the way DSLs are usually implemented in imperative languages, particularly scripting languages.

In Python, if I have:

    def foo(x):
        return x**2 - 1

I can plug in a concrete argument:

    >>> foo(2)
    3

But I can also plug in abstract values provided by some library where all operators are overloaded to return another AST node. For instance:

    >>> from z3 import *
    >>> expr = foo(Int('x'))
    >>> expr
    x**2 - 1
    >>> type(expr)
    <class 'z3.z3.ArithRef'>

And then I can perform abstract operations on the resulting AST node, like solving for x:

    >>> solve(expr == 0)
    [x = -1]

Of course this is completely non-type-safe. And without purity, there's no guarantee that `foo(Int('x'))` is truly equivalent to running foo on an abstract value `x`. If there's an `if` statement in there, the condition will either pass or not, and the returned AST node will only include that control flow path. The DSL in question tries to block that by preventing AST nodes from being converted to boolean, but it's not perfect. Haskell has an advantage there.

On the other hand, for the situation at the end of the post, where the author wants to model imperative computations, it seems like an imperative language would make for easier embedding. In an imperative language, each AST node can be given its own unique ID when it's constructed. So there's no trouble distinguishing between, e.g., calling some function bar() and then using the return value twice, versus calling bar() twice. No need to use a separate <- operator for assignments.

But to be fair, explicitly distinguishing side effects is kind of the whole point of Haskell!

(And if you wanted badly enough to do it in Haskell without requiring <-, you could use unsafePerformIO to assign AST node IDs.)

The linear functions/SMC work is really cool, but I am surprised to see the author calling it more mature than the compiling to CCCs work. The linear-smc library hasn't had an upload in a while, and it's currently missing any haddocks beyond the extracted type signatures. It's also a shame that it had to build its own typeclass for monoidal categories instead of using the one in https://hackage.haskell.org/package/categories .

Meanwhile KittyHawk did actually use the compile-to-CCCs work to compile Haskell to C in https://github.com/sellout/compiling-anything-to-categories and someone from there talks about it at https://www.youtube.com/watch?v=VUBj8NW7uMA

I think the linear-smc work is more exciting and I hope it matures with a bit more elbow grease. There was an ICFP talk that accompanied the linked paper ( https://www.youtube.com/watch?v=90OJz0QE4qE ) and monoidal categories can model lots of "boxes and wires" things. Linear functions potentially give you a much more ergonomic DSL for building up those boxes-and-wires models, and in a way that lets you write abstractions that work over any model.

What a delightful blog post. One need not fully understand all the prologue bits to understand the interface and implementation produced.

This technique could be very useful in developing other DSLs on Haskell. Basically the author found a simple monadic-looking mapping of Haskell functions onto a different Category where you can do interesting things with those functions. In TFA's case the idea is to write flow diagrams where "boxes" embed [user-provided] Haskell functions, then the machinery can do whatever might be expected for diagrams, like: render visual representations of them, evaluate them, analyze them, etc. Because the boxes embed Haskell functions the flow diagrams can do useful work, so they're more than just documentation, they can be code and documentation. Basically this is a flow diagram programming language as a DSL embedded in Haskell.

Imagine using this technique to build things like networking stacks, say. Or emulators of various sorts (CPUs/ISAs, say). Or maybe one could use this to make something like a PLC in Haskell. It's really quite a neat and powerful idea, especially if it really does compile to efficient code.

What else might one use this for?

Kinda tangential (since the linear vs Cartesian distinction wasn't made a big deal of here) but I liked the clarifying discussion (to layman me) of how "linear" and "affine" are related to the usage ones learns in uh middle school?

https://old.reddit.com/r/haskell/comments/txk3mn/why_are_the...

[And even the comment from the athletic river horse is thrilling to read]