Incorporates strong typing over predicate logic programming, and, conversely, incorporates predicate logic programming into strongly typed functional languages. The style of predicate logic is from Prolog; the strongly typed functional language is Haskell.
'V' is for ... I don't know what, because 'V' is for 'Variable'
HA! Saved by the variable.
I cannot believe I didn't know, at first, what 'v' was for, but there it was, all along, so much present I didn't even see it: the variable.
That happens to you? Something is so in front of you all the time, you don't even notice it until it's gone? It happened to Emma, Darwin's wife (yes, the Darwin), she had a 10-year-old boy whom she loved, and then, one day he was gone. Alive and sweet and playful one day, and then in a casket the next, never to breathe or to eat or to sing or to cry again, just to be dead then buried six feet under the ground, and then forgotten, just like Emma is now, just like Charles the Darwin is now not. But he will be. Given enough time and enough distance and everything shrinks to insignificance, and then to invisibility, just like the 'next' number after π.
Okay, side note, this font? Verdana? I love it. I freekin love it, except for one small nagging detail. Why in the world does it make the Greek letter pi, π, look like a frikken 'n,' for goodness sake?
Okay, switching fonts now.
Let's try Geneva. π. Better, much better representation of π. Okay, moving on with this new font.
Okay, so anyway, there, always there, but then gone and forgotten.
Except in Eternity. That's why we have it. In eternity, there always is, and always will be. There is being and that's all there is in Eternity.
Math is eternal. A statement of truth in mathematics is true before (we just didn't know it yet), it's true now, and it will be true for ever (in that particular domain). In mathematics you'll always have the Fermat's thingie, first known as a conjecture, then as his Last Theorem, and now known as 'solved.'
In mathematics, you're granted eternity. Euclid, anyone? He's been going strong these last two-thousand, six-hundred years. Erosthothenese? xxx he was just some dude at the Library of Alexandria, but he just noticed something about how to find prime numbers, and his technique is by no means now the best or most efficient, but which one is the go-to algorithm for primes at school or nearly most anywhere? And who knows his name and the association? Today?
Who will know your name and what you did, twenty-six hundred years from now?
Okay, wait. Geneva font doesn't have italics?
This is getting ridiculous. JUST GIVE ME A FONT THAT DOES EVERYTHING I WANT, PLEASE! THAT'S ALL I'M ASKING!
Okay, trying Helvetica now (π). Okay, this is working so far ... (Oh, and don't you dare say, 'oh, geophf, why not just use Times New Roman like everybody else does?' Don't you dare say that! Do I look like everybody else? No? Then don't ask the question why don't I do X like everybody else does! News flash: I'm not like everybody else! THANK you!)
(But I digress.)
So you have this thing, called a variable, that prevalent in mathematics and in computer programming languages. So prevalent, in fact, that it's just taken for granted and not even seen any more, just used, and abused, and that's it.
But, what, ladies and gentlemen, is a variable?
We can revert to the epigram: "Constants aren't; Variables don't" from antiquity.
Or we can say: "Variables? Just say no."
I'm being fatuous (as always), but, as always, there's a kernel of truth I'm trying to convey here.
You all know that the 'a variable is a cup' that teachers teach you in lesson 2 of the high school class that they unknowingly mockingly name 'Computer Science I.'
Computer 'science'? Really? Where is science being done in computer science classes these days in high schools? If there were experimentation and discovery going on, then, yes, they could rightly name these classes and these, okay, really? 'Labs'? computer science. But if it's all 'Okay, class, turn to page 204 of your ... and do the exercises there' rote drilling, then it's not computer science, it's more like, 'big brother grinding out mindless automatons so you can work for the Man until you die I.'
I mean, come on, let's be honest, please.
Anyway. But I digress.
What I'm (trying to) say(ing) here is that there are different representations of what variables can be, including the 'pure' approach and the 'logical' approach, and the approach that you probably learned in your comp.sci class that told you you can assign your variable, change its value and do all sorts of weird and wonderful thing you do to variables that have no correspondence to actual mathematics.
int x = 5;
x = x + 1;
What is x now?
'Well, 6, geophf, obviously,' you say.
Oh, really? Let's look at this again, mathematically:
x = 5
Okay, fine, x is 5. No problems with that.
x = x + 1
Okay, what in the world is that? For:
x = x + 1 (theorem)
-x = -x (reflexive)
0 = 0 + 1 (addition)
0 = 1 (addition)
And now you're left with a statement that 0 = 1.
So either that is true, meaning that x = x + 1 is true, or that is false, meaning that x = x + 1 is senseless, or absurd.
Take your pick: either zero equals one, or you can't, logically, 'increment' a number to 'become' another number.
So why do you think you can get away with that with variables?
Because in your comp.sci. I class you were told a variable is a 'cup' and you can increment it, and you told that stupid girl in the back of the class to shut the hell up after the third time she said, all confused, 'but, I don't get it.'
That actually happened in an intro to comp.sci class.
That 'stupid' girl in the back actually isn't all that stupid. She didn't 'get it' because there was nothing, logical, to get. It's an absurdity taught in comp.sci. classes (that aren't comp.sci. at all, I'll reiterate) that you all just buy because you were told this, like everything else you were told, and you're gonna get that 'A' from teach for the class, arencha?
But that's how most programming language model variables: something that can change, extralogically, too, at that, so why am I making a big stink about this, and about other extralogical features, such as (shudder) assert?
Because when you introduce things outside your logical domain, then you have a hole in your proof, and a hole, no matter how small, means that you can no longer say anything with certainty about the correctness of your system.
So, how should variables behave then, if they were logical?
'Constants aren't [that's your problem, bud]; variables don't.'
Variables in computer programs shouldn't vary. In the context of their computation, once bound, they should remain bound to the binding value while in that computational context.
(Please, let's not talk about lexical scope verses dynamic scoping of variables. That conversation died with the invention of Scheme.)
x = 5
But what if you need that variable to change? You ask.
Why? I ask back. Let's think this through. Why would you need to have something change during the course of a computation? Because one value didn't work and you want to try another value?
That's easily solved, simply restart the computation in that case, then you rebind the variable with the new trial case.
Is x 1? Obviously not, so just keep calling that function with a new x until you get your greater-than-100-factorial value from your trial number. But x, inside the computation is that value, and not some other value.
By the way, I had this as an interview question: write a function that returns a factorial of a number greater than X.
... as a fault-tolerant web-service.
The questions of 'Okay, why?' and 'Who would want this, anyway?' were not part of the conversation.
This is all very comonadic ('W' is for comonad ... fer realz, yo! That'll be my next post) because here you control the value in the computational context as well as the computational context, itself.
Variables are comonadic as the title of of one of my '... are comonadic' articles? Why not?
The same thing, in a very different way, happens in Prolog. Once a logical variable is bound (that is, once it's not longer 'free') it remains bound in the logical context, and you either complete the proof, exiting the context, or you fail back up through the proof and in so doing restart somewhere upstream from the variable binding, which allows you to bind a new value to the logic variable.
A logic variable is variable insofar that it is either in a bound state (has a value) or in a free state (and is waiting to be bound to a value), and this happens through some kind of unification ('U' is for Unification).
Variable-binding in prolog is purely logical.
'Variables that don't change, geophf? What use are they? That totally doesn't model the real world!'
Uh, it does model the real world, and much better than your imperative-stateful variable-state changes. I mean, once a thing is a thing, it remains that thing forever more. You ever try to try to 'change the state' of an electron to a proton? You ever change a hydrogen atom into helium?
Actually a 19-year-old kid built a fusion reactor in the toolshed in his back yard. People kept telling him that he 'couldn't' do that. He loved that when he was told that over and over again.
And then submitted his working fusion reactor to the google science fair.
Do people get attention for listening to nay-sayers? No, they get beaten down to become a nay-sayer.
Did this young laddie get attention at the google fair?
... and beyond?
Yes. Oh, yes, he did.
Where were we? Oh, yes: variables. How did we get here? Oh, yes: changing something to be something else.
You 'can't' do that. So don't bother, sayeth the nay-sayer.
And, if you absolutely, positively mustchange a variable to become something else, well, I got something for ya! It's called a State variable.
data State a s = s -> (a, s)
What's going on here?
State isn't a (mutable) variable, actually. It's a function.
Functions rock, by the way.
This function takes a state-of-the-world, whatever you deem that to be, and returns a value from that state as well as the new state-of-the-world that it sees.
So, what you can do is string this state-'variable' from one state to the next and get yourself an approximation of a mutable variable, just like the ones you hold so dearly in your 'ordinary' programming languages, so your x = 5 example now works:
do put 5
x <- get
return $ x + 1
Where 'put' is your assignment and 'get' is getting the value of x
And those two statements are strung together, computationally, even though not explicitly so in the above example.
Here, I'll make it explicit:
put(5) >>= get >>= \x -> return $ x + 1
The monadic-bind operation (>>=) strings the computation together and you have a logical trace of the computational state-domain from its initial state (put(5)) to its retrieval (get) to it's updated state (return $ x + 1) there is not one place where a variable actually changes its value and the entire computation is logically sound from beginning to end.
The above is a statement of truth and is provable and fully verifiable.
The below statements, however:
x = 5
x = x + 1
Are, indeed, statements, but I've shown one of them is false, so the whole system crumbles into absurdity from that one falsehood.
And people wonder why computer programs are so hard to write and to get right.
It's only because of something so simple, and so pervasive, as mutable variables.