pjdorrell

The desire to explore untouched wilderness is something that has been strongly selected for. The world has been colonized by those who had the greatest inclination to explore the unknown.

Non-human animals also, eventually, colonize areas beyond their point of origin, and this is no doubt driven partly by a desire to "explore". But humans, perhaps more than any other animal, are capable of having the idea of "exploring" as something that they can be obsessed by. And humans are less constrained by the need to constantly satisfy the basic necessities of life, which makes it possible for the dedicated explorer to go on extended exploring trips, exploring the world for its own sake.

Also, it is part of human nature that different people in a social group develop different interests, which benefits the tribe via division of labour. So not everyone needs to be a committed explorer - it is enough for one mad explorer to go out exploring, and then come back to the tribe to report if they found something worth reporting.

If the number of lives saved by making best use of partial information exceeds the number of lives lost because of people who fail to understand the concept, then that's a net benefit.

What do you mean by “many things that some would not consider music”? Is there some group of people who would consider all “organized sounds” to be music? Are you one of those people?

Theoretically NULL means "unknown" value. As it happens, most business applications do not have any requirement to deal with "unknown" values. These applications are only interested in acting on requests where all the required data are provided by the person responsible for entering the data. For example, when I transfer money from one bank account to another, the amount of the transfer can't be "unknown", the sending account can't be "unknown", and the receiving account can't be "unknown".

These same applications do have requirements to deal with empty values. Sometimes an empty value means "I haven't yet entered this value in the to the UI". But in that case the UI won't let you submit the form until you have supplied a valid value.

In other cases an empty value is a valid value. For example, "who is your spouse?" and the answer is "I'm not married".

Sometimes NULL represents "irrelevant", like for "who is your spouse?", where some of the records in the table represent people who can have spouses, and some of the records represent other person-like entities that aren't actually people and therefore they can't have spouses.

Given that NULL is _not_ being used to represent "unknown" values, and there is a requirement to represent empty values, and you don't want to have a whole extra column just to represent "emptiness", the most straightforward way to implement empty values is to use NULL. So that is what happens.

And you have to remember to use "is" instead of "=" when you want to test your empty NULL values for equality with other empty NULL values - because your SQL database is pretending that NULL really means "unknown", and it doesn't want to say that one unknown value is equal to another unknown value, because that would be theoretically incorrect.

In Python

type(type) is type

evaluates to True. And that is not permitted in mathematical type theory that the Curry-Howard correspondence applies to.

The best way to understand about war chants is, firstly, to imagine what it would be like to be a warrior in some prehistoric tribe that is about to go to war. Imagine possible scenarios in your future - the beginning of the war, where you and your fellow warriors carefully but deliberately proceed towards the enemy (who might be a neighbouring tribe who don't yet realise they are the enemy), the actual fighting, where you are in a constant state of "kill or be killed", and, finally, the world as it will be after the war has finished. If victorious, you will have greater status in your tribe, more possessions, more territory, possibly more women. Even if your tribe does win the war, probably some of your colleagues will have died, and it won't be the same living without them. Whatever the result, life after the war will be significantly different to life before the war.

Then, after thinking these thoughts, find a piece of music that strongly intensifies the emotions which arise from thinking them. This music won't be an actual prehistoric war chant, because most of us living in the modern world have musical tastes that have been shaped by exposure to modern commercially produced music. So you will be thinking about a prehistoric war scenario, while listening to twentieth or twenty first century music.

Then, I think, you will understand, albeit subjectively, what it is that war chants are about.

The boring answer is that the initial origin of life depends on a sequence of extremely improbable chemical reactions (even given the prior existence of the most favourable possible “organic soup”), and there is no other life of any kind in the observable universe.

“Hot” and “cold” are not, as far as I know, feelings that music can express.

An imagined perception is a perception that depends on the perceiver making some effort to suppose that something is true. It could be a daydream, or it could be when you watch a fictional film, which requires you to imagine that it is real, even though you know that actually it is not real. Real perception is when you are perceiving something that you know is real.

This is quite similar in some ways to my own theory that I posted recently at https://whatismusic.info/blog/HypothesisMusicWasALanguageSys..., because it postulates a sudden transition from non-recursive language to recursive language. The one difference in my theory is that I assume that the original non-recursive language was musical (with one tune equals one meaning). And musical language could not evolve into a more efficient and expressive recursive form of language - it had to be replaced.

I always click on anything on the front page where I don’t understand the headline. If it’s good enough to get votes _and_ I don’t know what it is, then it’s likely to be a good opportunity for me to learn something new.

Coming soon to your favourite login page: “Select all squares with neatly folded laundry. If there are none, click skip”

Binaries almost never form from stars “wandering” and “encountering” other stars. Current scientific understanding is that almost all stars are formed as binaries in the first place.

http://thinkinghard.com/blog/IdentityTheft.html (2005)

"Mathematics" does not predict a mass extinction. Someone has a theory which predicts a mass extinction, and that theory has mathematics in it.

Surely some borrowers and lenders make decisions about making and taking loans based on the actual interest rates on the actual loans? In which case it doesn't matter so much if the rates are calculated based on a fictional assumption about something. At the end of the day every borrower or lender in the market makes their own decision about which lending contracts they take part in.

The diagram appears to be missing Dependently Typed programming languages.

Does this really use advanced features of Homotopic Type Theory? Does it really require the Univalence Axiom? (Caveat: I don't yet properly understand either of those two things.)

It seems to me that the representation of cardinalities as "Univalent Types" could just as easily be done using Decidable Setoids (eg the number 3 is represented by a Setoid with a decidable equivalence relationship that divides its members into 3 equivalence classes).

There are only four things in this system that require a notion of equality and/or equivalence: tuples, cardinalities, relations (as functions from tuples to cardinalities) and queries (as functions from relations to relations).

I think this could all be done with in ordinary plain dependent type theory, without any HOTT or Univalence Axiom (for example, in Idris, which is apparently incompatible with the Univalence Axiom). Each of the four notions of equivalence would be represented by a corresponding type function.

Have I missed something?

If Luna is dependently typed, can it be used to do theorem proving, eg like Idris?

Music is not language and it is not "a language". It is something that _seems_ like language.

This is because music has evolved as a mutated copy of part of the human language acquisition instinct. The mood change caused by music is a mutated copy of the mood change that accompanies initial language acquisition, and it serves a different purpose.

The mood change that accompanies initial language acquisition helps to focus the infant's mind on language as a separate important thing that has its own (somewhat arbitrary) rules that need to be understood separately from everything else.

The mood change that accompanies music serves to intensify emotions that accompany daydreaming - this helps us to "better" daydream, in a manner that does not cause us to confuse daydreamed emotions with real emotions (because we are always consciously aware that the mood change is directly caused by listening to music).

(More details at http://whatismusic.info/.)

In North Korea, browser history deletes you!

My understanding of the promise of Idris is that anything you _want_ to put into the type definitions for your application, you _can_ put into the type definitions.

Also: http://thinkinghard.com/domkol/main.html

This interactive visualization lets you see that the number of times the polynomial function "winds" around the circumference of the circle is equal to the number of zeroes inside the same circle.

(Caveat: the interaction to move the zeroes around requires a mouse.)

I believe I might have been the first person to correctly analyse the thermodynamics of evolution by natural selection: http://thinkinghard.com/evolution/2ndlaw.html (originally http://web.archive.org/web/19961221074218/http://www.xmissio...).

By "locally" I think they mean something like "entropy will decrease within what looks like a closed system, and it might not be immediately obvious where else in the universe the corresponding increase in entropy is occurring".

So not actually "free energy", but perhaps it could be used to stage a convincing demo to potential investors.

You are looking for a "theory of music", as opposed to "music theory", ie an explanatory or scientific theory.

I offer my own efforts in this direction at http://whatismusic.info/.

My own thesis is that when modern humans and Neanderthals co-existed, they would have appeared uglier to our ancestors than they do to us - because we are no longer subject to selective pressure to avoid mating with Neanderthals.

http://thinkinghard.com/blog/WereTheNeanderthalsUgly.html (2006)

Also, the word "reported" got left out of the headline.

Ie 93% of professionals _claim_ they are more productive somewhere other than their office.

Headline says: "docker _in_ GitHub repo names"

Story detail says: "using the registered trademark Docker as the _first part_ of a repo name"

So imaginative name replacements like "wharfee" not necessarily required.