sassa_nf

Отак щоранку згадував рускіх. Тепер додались ще.

Liberals in the English-speaking tradition call for negative liberty, meaning a realm of private autonomy from which the state is legally excluded. In contrast French liberals ever since the French Revolution more often promote "positive liberty" – that is, liberty insofar as it is tethered to collectively defined ends. They praise the state as an essential tool to emancipate the people.

Basically, "negative liberty" is what people are free from, and "positive liberty" is what they are free to do.

Positive liberty as a concept introduced by Isaiah Berlin. There's a bunch of his lectures on this topic, interesting stuff.

From the post here.

Given F x = (x→p)→q for some fixed p and q, can we show that it is or isn't a monad?

---

We have to assume the existence of function k: p→q for pure to exist, and we have to assume the existence of function h: q→p for (>>=) to exist.

pure x = k . ($ x)

- there is no other way to construct a value of type q from a function of type x→p, you have to have a k: p→q.

Then:

m >>= f = m . (h .) . flip f

- there is no other way to construct a function of type (x→p) from a function of type x→(y→p)→q, you have to have an h: q→p.

Associativity of (>>=) follows from associativity of composition. How about the unit laws?

pure x >>= f = f x -- unit-1

pure x >>= f = k . ($ x) . (h .) . flip f = k . (h .) . f x = (k . h) . f x

- this should be f x if k . h = id.

So k is a surjection.

m >>= pure = m -- unit-2

m >>= pure = m . (h .) . (k .) $ flip ($) = m . ((h . k) .) $ id = m . (h . k)

- this should be m if h . k = id.

So k is an injection at the same time - p and q must be isomorphic.

http://go.dev/ref/mem#advice

Don't be clever.

Who do they think they are?

This is what we are reading these days

Yes, I've done facebook online problems once, just because I like problems like that.

So, like here: https://malyj-gorgan.dreamwidth.org/187069.html

N ∈ [2, 5×10⁵]; i,j ∈ [1, N]; d_i, h_i ∈ [1, 10⁹];
maximize:
d_i h_i + d_j h_j + max(d_i h_j, d_j h_i)

That's the mathematical notation. The statement is really about various warriors with damage D and health H fighting a "boss", and you've got to choose the best pair. The fighting arrangement is such that while the first warrior is receiving damage from the "boss" (health declines), both warriors can damage the boss. This explanation is here simply to explain the terminology I use in my solution.

I don't know whether there is a better solution, but here's my approach that worked well enough.

It is obvious that comparing each with each finds a solution, but given the possible magnitude of inputs it becomes intractable. So if we sort the warriors in some way, this would become tractable. We can also afford( ...spoiler )

We had a little discussion here

Basic question: if lists are Church-encoded, how do you zip two at the same time? There seems to be a difficulty in commuting list construction (new list) and list destruction (two input lists).

Initially I thought of a way to preserve the state of list destructor routine. So on each step of construction you can progress the iterator of the destructor one step at a time. But a good question chaource raised is: how can we generalise this to trees?

And then from the dark recesses of my memory the shadows of Varmo Vene's thesis whispered.

Hylo morphism to the rescue!

Wink-wink, nudge-nudge, ( say no more! )
Obvious extension for church-encoded trees:
( Read more... )
Of course, we could do church-encoding of pairs as well, but I reckon we don't have to do that even for Option. The original problem was driven by the quest of expressing recursive data structures in the language that doesn't support it (to prove that the structures and types are finite). Finite non-recursive types like Maybe and Pair are not problematic.

---

After some more discussion:
( here is more )

https://youtu.be/0ApTcHQMtq0 - як козаки зброю добували

The proof: https://math.stackexchange.com/a/4250143

It's kind of funny how the proof becomes trivial, if you express the types the right way.