somewhereoutth

96 ms·

1291.
by somewhereoutth 7y ago
(cont'd) ... and I see it now, the damage that has been wrought. I imagine Church never dreamed that his approach of unitary type assignment would lead people to believe that types actually exist, and that programs should do different
1292.
by somewhereoutth 7y ago
The crucial difference between Church and Curry is that Curry allows each term to be ascribed a set of types - perhaps 0, 1 or many - whereas Church insists on each term having exactly one (often annotated). Both are systems for proving typ
1293.
by somewhereoutth 7y ago
I'm sorry but this is wrong: "The assertion that beta reduction (i.e. evaluation) does not rely on type information and types are overlaid on top is precisely the heart of Curry semantics." Beta reduction is not affected
1294.
by somewhereoutth 7y ago
Thankyou for your reply (and apologies for deleting the comment). I am not sure that the distinction between Curry and Church semantics is so critical - after all we have but a single 'engine of computation': beta reduction, appli
1295.
by somewhereoutth 7y ago
but (for the simply typed LC anyway) the 'mechanism of action' is just the untyped LC under beta reduction surely? I mean, the type annotations don't actually do anything when the program is run/reduced?
1296.
by somewhereoutth 7y ago
Would I be correct to say that System F, and thus Haskell, has been effectively built on the untyped lambda calculus? If so there are many (very many!) statements in the LC that are illegal under System F. Certainly whole classes of patholo
1297.
by somewhereoutth 7y ago
That is the point - perhaps you can't, in the same way there are true statements in Peano arithmetic that cannot be proved (if my understanding is correct). The concern is that these statements may still be useful and elegant, and ruli
1298.
by somewhereoutth 7y ago
Indeed, a type system is a great tool for producing correct code, and I cannot advocate doing away with type safety. However, my counter-argument would be that important failures often occur due to unforeseen interactions in complex systems
1299.
by somewhereoutth 7y ago
Following Godel:- my intuition suggests to me that for a sufficiently powerful programming language (Turing complete?), any type system will preclude otherwise valid statements in the language. Such illegal but valid statements will be mu
1300.
by somewhereoutth 7y ago
Agreed. I think a way through this may be to emphasize the notion of 'performance rights' over 'copyrights'. So distributing a work digitally, for consumption on a personal device, would be free of encumbrances. But perf
1301.
by somewhereoutth 7y ago
Absolutely this. Someday we need to have interest rates somewhat sticky at ~5% (or whatever the sensible figure is), and lean more on fiscal policy to control the economy. Whether there is a viable path to that point is unclear. Perhaps the
1302.
by somewhereoutth 7y ago
One way to see the difference is to consider a loop on the sphere or torus. On a sphere, any loop can always be drawn tighter until it is a point. On a torus, there will be some loops that cannot be drawn tight, as they go 'through the
1303.
by somewhereoutth 7y ago
This feels like the end of an era - an era that ran from the fall of the Berlin Wall up to the appearance of Covid-19. A global era, a largely peaceful era, a profligate era, and an era of growing inequality. Who knows what comes next...
1304.
by somewhereoutth 7y ago
To be honest there are going to be only 3 types of Coronavirus People: 1. Those who didn't catch it, 2. Those who survived, 3. Those who died. The first cases appeared in my city a few days ago...
1305.
by somewhereoutth 7y ago
Ah - but though a subset (bestsellers/halting programs) may not be computable (recursively enumerable) as you say, this does not preclude all novels/finite programs from being enumerated. Taking the alphabet as just the uppercas
1306.
by somewhereoutth 7y ago
It is? Is this at the quantum level? To be honest my understanding of quantum physics is cursory at best, though I had thought that the notion of a 'clockwork universe' had been otherwise discredited.
1307.
by somewhereoutth 7y ago
Exactly this. To be more precise with your analogy, given a finite alphabet and a finite length for any novel, then in fact the set of all novels is countable (and computable) - but when novels can have (countably) infinite length (or are w
1308.
by somewhereoutth 7y ago
On the subject of shared costs/benefits: The wealth that allows us modern healthcare is not so much the wealth we are producing today, but overwhelmingly more the wealth that the countless generations before us have created. That one p
1309.
by somewhereoutth 7y ago
Agreed. A Turing machine operates in a discrete countable state space, whereas the human brain requires real numbers for a complete state description. Cantor showed (with the diagonal argument) that real numbers are uncountable - so there a
1310.
by somewhereoutth 7y ago
I live in Lisbon, Portugal. I use CityMapper with public transport to get around, and it is very good - I particularly appreciate the 'Get Me Home' button. Residents here can get a monthly pass on ALL public transport in the great
1311.
by somewhereoutth 7y ago
Yes, Food. I spent a couple of years in California and I miss it very much. However, the one thing that I would not have been able to work around, if I were to make my home there, is the food. Not that it tastes bad, but that it is bad, a
1312.
by somewhereoutth 7y ago
Mathematically speaking, current computers run in discrete (integer/countable) space, and the human brain exists in continuous (real/uncountable) space. Cantor showed that continuous space is larger than, and thus cannot be repres
1313.
by somewhereoutth 7y ago
I have been researching cellular automata, with Von Neumann neighbourhoods, with emphasis on their aesthetic qualities for use in technological art and design projects. I present a short write up of my findings, along with a Processing sket
1314.
Show HN: Von Neumann neighbourhood cellular automata(bitbucket.org)
3 points by somewhereoutth 7y ago|1 comments
1315.
by somewhereoutth 7y ago
Reading these comments really brings me back! If I remember correctly, developing a simple project reporting system based on Access, and using forms, was my first foray into professional software development (I had actually trained as a Mec