Lambda the Ultimate

we can have a factorial function in traditional functional syntax:

fact: int -> int;

fact 0 = 1;
fact x = x * (fact (x - 1));

Translated to my language, that would be:

Fact <= (
    (
        @int                     <= @int
    ) <- (
        1                        <- 0         |
        (@x * @Fact <- (@x - 1)) <- x : x > 0
    )
)

Now, the problem is that I use "Fact" symbol as a single pivot for storing data results also (so I can access it when needed). With non-recursive function, the solution is clear, the pivot gets populated only once. But for recursive call, the pivot gets "functional-reactively" accumulated with all the future recursive results, causing the whole set of recursive results to start popping up, and the processing never ends.

I was thinking I could get around by using monads, but obviously monadic functions get accumulated too with recursive data, the same as pure functions, as far as my understanding goes. So, I think I'm going to solve this without monads by introducing a simple rule: when reaching a symbol, you can see all data from the right side, but you can't see the future data from the left side, i.e. you can see the past, but not the future. This would leave programmer level functional reactiveness out of the equation, while hoping that I can still provide it at user level somehow (maybe by putting special placeholders on demand instead of past variables, so they could get populated in the future.)

What a complication with me!

Does your language also accumulate across independent calls? If not, you might get a different semantics for a fixpoint expression of the recursive function.

...independent calls. If we write later:

X <= @Fact <- 3
...
Y <= @Fact <- 4

all that is stored under node "X" is separated from a value of node "Y".

But in contrary, if we apply, say: "(Fact <= (...)) <- 3", at the point of "Fact" definition, the result gets inherited for the future instances of "Fact", namely "X" and "Y". In this case if we apply a value at function definition, we can't apply it again at defining "X" and "Y", as "Fact" already became a result. Also the future instances of "X" and "Y" (like "U <= @X") inherit their "result containment" / "application expectation". If we don't apply a value to a node, it is still considered as a function, until an application is made, when it becomes a resulting value (or a resulting function in higher order constructs).

If not, you might get a different semantics for a fixpoint expression of the recursive function.

I'm not sure I understand.

By fixpoint expression I mean something like:

Y f = f (Y f)

Fact' self 0 = 1
Fact' self x | x > 0 = x * self (x - 1)

Fact = Y Fact'

And it is possible to express Y non-recursively, too, and even without variables, for example via SKI combinators.

Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))
S f g x = f x (g x)
K f x = f
I f = f

Named recursion is unnecessary. Names, in general, are unnecessary. You can express any recursive function anonymously.

Since your language is overloading names to awkwardly accumulate information, you might consider fixpoint as a workaround. (But this being a workaround raises some dire questions about your semantics and ability to abstract code.)

That fixpoint combinator looks like a clever method of avoiding recursion.

Anyway, I decided not to accumulate information (it seems unsound anyway), yet to see only past applications, not the future ones. It should work, I believe.

A monad has a "before variable", a transition function, and an "after variable". Is it possible to recursively feed "after variable" to "before variable" in some other way, other than using "do" monad, maybe by some regular functional function? Like feeding "after - 1" to "before", somehow in a functional way? But maybe I'm looking for ghosts...

But this helps too, one solution is there, thanks.

If you rewrite the do notation into calls on the monad bind operator then the recursion is easier to see:

test n = test (n-1) >>= (\x->return (x+1))


A longer explanation of the rewriting is here.

Ok, so implementing the above code in my language, I get the following monadic (in my own understanding) expression:

// "<=" is for defining functions
// "<-" is for applying parameters
// "@"  is used to reach existing variables
test <= (
    (
        @int <= (@int                             <= @int) <= @int
    ) <- (
        @b   <- ((b <- (1 + (@test <- (@a - 1)))) <- @a  ) <- (a : a > 0) |
        @b   <- ((b <- 0)                         <- @a  ) <- (a : a = 0)
    )
)

But it seems to me that this is equaivalent to pure version:

test <= (
    (
        @int                      <= @int
    ) <- (
        (1 + (@test <- (@a - 1))) <- (a : a > 0) |
        0                         <- (a : a = 0)
    )
)

Getting back to existing functional languages, is "a->(a->b)->b" construction everything what is needed to construct a monad? I think I got it wrong, or I'm not using it right. I'm still chrunching Marco's explanation from parent.sibling thread.

Hmm, I would say, read an introduction. But it's just about unit and bind. Any monadic structure is defined on unit and bind, and some monadic laws I find nonsensical from a foundational perspective, i.e. categorical sloppiness.^1

unit : a -> M a                    <- inject a value
bind:  M a -> (a -> M b) -> M b    <- calculate along

Now, why I say it's just overloading apply is trivially explained in two steps.

Erase the theory M.

unit : a -> a                
bind:  a -> (a -> b) -> b    

Change the order of arguments of bind.

unit : a -> a                
bind:  (a -> b) -> a -> b    

You get back id and apply, i.e., you just overloaded function application to calculate 'modulo a theory'. Anything which does that gives you something back equivalent to a monad.

(Anyways, your question about 'can I solve this with a monad' is somewhat silly too. The theory you stick into a monad can be anything, from solving a differential equation to baking a pizza. So the answer is always yes. Doesn't imply you should and usually implies you shouldn't.)

^1: 'Useless' from a programmer's perspective too. I might want to observe the amount of 'calls' to bind, or define another 'run' function.

The Monad in Keean's example doesn't do anything - it is just there as an example of the syntax. So it should reduce away to nothing: bind . unit = id. If you want to see the difference try working through a more complex example. Take a look at the examples using Maybe in this chapter. Perhaps they will be helpful?

Yah. For that you need to believe that monads form a category which satisfy monad laws, then you need to believe that even in a categorical setting the monad laws are sensible, then you need to believe that Haskell types/classes/functions model categories, and lastly you need to buy into that category theory models anything at all. (Last I looked half the math department, which has no problem assuming a Platonic world, wasn't convinced category theory has anything resembling a model. Simple stuff like duality might not exist.)

No.

Are you proposing that monads don't exist, together with category theory?

I.e. what can you do with monads that you can't do with pure lists?

What do you mean with exist? Math is sloppy. If a mathematician writes down some function from natural numbers to natural numbers he doesn't really care whether it 'exists'. He assumes there is something somewhere in a Platonic world.

As a computer scientist you do care, right? A function from nat to nat is not a Platonic object, but a calculation. And then you're stuck with for it to exist the numbers must be able to be modeled, and the function should preferably terminate, and a proof for that termination should also exist.

So you have mathematicians who assume some Platonic world and computer scientists who think that all math is computation. They already have different opinions on what exist.

But category theory is worse, right? Mathematicians are not sure it even 'exists' in a Platonic world. Doesn't matter much to them, it is useful just as ordinary sloppy math is useful to them.

But now you've got people trying to do foundational stuff (not the math foundational stuff, say algebra, but the logical foundational stuff) with it. Or it is being applied in Haskell, and -predictably- now stuff starts to crack. Because Haskell is as much about computation as it is about math.

Lately, I've read some comment from Andrej Bauer that Hask (the category of Haskell objects) doesn't exist. And his claim was: it doesn't. (Lots of categorical laws don't apply.)

But he got it reversed, right? He stated he is a constructive mathematician but then his conclusion should have been not that Hask doesn't exist, but that if Hask doesn't exist then neither does category theory. (In a strict foundational computer science sense.)

So it depends on who you ask. Ask a sloppy mathematician and he'll say yes, but he means it is useful to him. Ask a good logician and my bet will be he says no.

Math is a kind of science where human intuition is excessively used. Even Martin Löf's Type Theory is based on human intuition. And humans are beings who make a lot of errors, as we are sloppy if we don't check ourselves somehow. And what is a better check than a check from something that doesn't make errors, namely the Universe machine? "Making Errors" is the middle name for humans without empirical data to correct us.

If something isn't completely formalized, that means we don't know the complete truth about that something. It means that we have a majestical hint that that something should behave this or that way. But that doesn't mean we know nothing about that something. If the Category Theory has difficulties for being completely formalized, that doesn't mean that all of our assumptions about Category Theory are wrong. In my opinion, the most of important assumptions can be used, formalizing them each in their own domain, even if they don't logically fit together when we put them side-by-side in the same domain. (This is my assumption about Category theory of which I know nothing, but it should follow the pattern if I'm right.)

But to get the whole image, all pieces should fit together. And then, in my opinion, extraordinary possibilities should open. I don't know how far we are from that point, but until then, we are doomed to stitch pieces by hand, and not by deeply understanding what is going on in between.

Sure, the whole Universe could be simulated and programmed in an assembler, but we are not that much smart. We need utilities, which ultimately end in a form of more and more general theory. That theory could be approached from the side other than the empirical side; that theory could be approached from the theoretical side, from a point of knowledge about knowledge... about which we know pieces that still have to be understood how they mutually interact, and how they mutually exclude themselves. What I mean is that that theoretical side is about laws of knowledge, not about laws of the Universe.

By "exists" I mean that its whole does not exclude any of its pieces. To be more formal, I mean that it doesn't imply false when running a proof checker on that isolated piece of knowledge as a whole. Surely it can exclude other wholes, but I don't think it should be rejected as useless. Actually, I don't know what is really going on when two wholes exclude each other, but it is a fact that some of them somehow work when we isolate them, and we should use that property in a meanwhile, until we reach the more general whole.

Another question now arises: "Does the more general whole even exist?"

No certainty whether it has a model, no idea what equality is assumed, unclear reasoning about what a type is, no computational interpretation. Lots of definitional handwaving when applied.

I call it the finger paint of math.

No, I disagree. Last I know they tried formalizing pieces of math with a categorical approach to it. And if I got it correct, they managed to prove that small isomorphic algebras are equal to each other. So, 0=1.

I believe it is useful to people but I don't think you can foundational stuff with it. I'll be happy to be proven wrong, of course. Don't think I could prove 1+1=2 these days if my life depended on it.

Being near math now, you know what tickles my mind for a decade now?

1. increment is a base and let's say it's the first order operation
2. addition is repetitive increment and let's say it's second order operation.
3. multiplication is repetitve adition and let's say it's third order operation
4. to the power of is repetitive multiplication and lets say it's fourth order operation
5. ... so on ...

So, all we have here are integer order operations. I wonder, how would look like, say, an operation of 2.5 order??? Consider the power operation. It is not easy to imagine real number exponent just like that. But people somehow concluded: if we have an exponent of 2.5 = 5/2, then we have the square root of (x^5). Maybe something similar could be done with enumerated operations? Maybe 2.5 order operation could be something between addition and 5. order operation? I believe if we had a decent theory about theories, the solution would pop out just like that.

I know, I know, I drink too much coffee :-)

It is a somewhat meaty idea. The standard notation is called Knuth's Up Arrow Notaton and is used to write large numbers. The question of what kind of meaning could be assigned to non-integer values is interesting as the operator has a definition as a discrete recursion function. More coffee required :)

To-the-power-of operation also exhibits some recursion operation, yet it combines powers and roots for non-integer numbers. I think we need something reversed to up-arrow, analogically to root, maybe down-arrow?

R. L. Goodstein (the same wiki page) had equivalent, but more expressive notation we could use. For example, addition is denoted as [1], multiplication as [2] and so on. To solve this puzzle, we need define what would fractions like [1/2] represent, and what would negative numbers like [-2] represent.

Fractions could simply represent reversed positive integer operations, but I have a problem imagining negative integer operations. Maybe simply x [-2] y = 1 / (x [2] y), like with powers, but I'm not sure. Is there any way to check this out?

I believe this puzzle has a connection to the bases of numeric systems, so maybe it would be then possible to define a numeric system of base e. I also have a hard time imagining this proposition.

And what would x [e] y mean?
And x [0] y? Identity?

Each of the instances of the operator (e.g. [1], [2] etc) defines a different operation on the set (class). Each of these operations is a discrete operation (over the integers) that can be extended in a consistent way to a smooth operation over the reals. Because the reals form a field we can then define things like fractional exponents - the existence of a division operator implies that we can interpolate between different values in the domain. But these fractional values are operands for an operator over a smooth set.

The operators themselves are not smooth - they are a discrete set (class?) of mappings over the value domains. There is no division operator that exists and no smooth interpolation between one operator and another. As far as I know there is also no hard result that shows that it is impossible to define.

One one hand, an obvious objection is that because the set is discrete the values have no differentials so it is not possible to define division. But on the other hand, there is a nice result that pops up here from time to time about differentiating grammars with respect to a particular symbol (lovely short paper from a few decades ago, cannot remember the name of the technique). I have a vague memory that if you treat regex as a ring then with the additional operator it looks a bit like a field in some ways.

for example, and consider x^(1.5). Actually, power operation niether exists on real numbers solely. But if you convert it to x^(3/2), you get combination of x^3 and x^(1/2), with x^(1/2) being square root. The result lies in the interpolated set of integer, while the operation itself would be defined only on integers.

So, "x [1.5] y" could be seen as "x [3/2] y", transformed (maybe) to "(x [3] y) [1/2] y", with [3] being power and [1/2] being division - opposite of [2] being multiplication. The result would also lie in the interpolated set of integers, while the operation itself would be defined only on integers.

I still don't know how to check if:
x [3/2] y == (x ^ y) / y

But, I checked it on this example and it doesn't work on exact linear scale:

prove that x [4/2] y == x [2] y

1) if [1] is increment,
then: 2 [4/2] 2 = (2 ^ 2) - 2 = 4 - 2 = 2
while: 2 [2] 2 = 2 + 2 = 4

2) if [1] is addition, 
then: 2 [4/2] 2 = (2 ^ 2 ^ 2) / 2 = 16 / 2 = 8
while: 2 [2] 2 = 2 * 2 = 4

3) if [1] is multiplication, 
then: 2 [4/2] 2 = sqrt (2 ^ 2 ^ 2 ^ 2 ^ 2) = 65536
while: 2 [2] 2 = 2 ^ 2 = 4

Maybe we should check it somehow by putting a numerator or denominator part on a logarithmic or exponential scale, just to be sure? Something between case 1) and 2)? Or something analogous to that rule where: log (x^y) = y * log x?

I think that you have the division in the wrong place to make that work. It's a little like the old joke in Ireland about asking for directions to a place, only to be told "well, this isn't the best place to start from". Showing that x [u/v] y = (x [u] y) / (x [v] y) would capture the (probable) distributive law of the operators slightly better.

The example that I couldn't remember is in the LtU archives from a couple of months ago:
Derivatives of Regular Expressions. It's a good example of building an operator that behaves as we would expect division to behave (in some circumstances) on a set that is discrete. Perhaps it will lend you some inspiration.

Please *define* too much coffee?

...is a legal mild narcotic. It makes me think and do stuff I would never think and do if I would be silver. And some of those things might be insane.

Though the do argument is usually understood to be a transition, it doesn't need to be. In specific, if monadic calculations are overloading the apply operator such that you can calculate 'modulo a theory', that doesn't imply that you actually know what is going on in that theory, the argument doesn't imply a transition is made (in a computational sense, like outputting a value). Just something like that you augmented the theory with new information.

Still, it is overloading apply so somewhere you ask something like, can I set the output parameter 'y' such that I can reason backward such that if 'f x = y', I can calculate something about 'x'?

No, you can't, output is output. But you can create a monadic structure for 'f x' and let it search backward for values which would, for example, equate 'y'.

I think I've seen Dan Pipponi do stuff like that, but it's a long time ago and I am not sure I got it at that point.