Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
starting something, to go alongside necessity and possibility
(will adjust page name in a second)
not much here yet, though, under construction
Added reference
Concerning the nonlinear case, why not take a case from everyday life and see how we’d speak about it. So letting the type of variation, , be days of the week, we might take the type of hours in the day, , numbered from 1 to 24. Base change takes to a copy of over each day.
In the (co)unit maps pass from the type, , of hours in the week to and from to , the type of assignments of an hour to each day.
(15:00, Thursday) is sent to 15:00, which in turn is sent to 15:00 any day.
provides definite times to meet.
Perhaps we might say of that it is as yet only potential. “What time shall we meet? 15:00. Yes, but which day?”
How would we speak of , an element of which would be ((13:00, Monday), (09:00, Tuesday), (22:00, Wednesday),…)? All of the information is there, but we don’t have the time fixed yet as we don’t know the day.
seems the most natural one, worthy of a simple term, such as ’definite’ or ’determined’.
Okay, let’s get to the bottom of this linguistic riddle.
On the one hand, it is true that once we have a term in the coreader comonad, it is “definitely any” of the types , , where here for all .
This is what i used to be building my linguistic intuition on, too.
But putting the emphasis on the collection of all such terms, it reads more like being “definitely any” of these types.
Namely, the coproduct produced by the coreader comonad inevitably behaves much like that produced by a maybe monad or exception monad, and their interpretation is decidedly as non-definite.
So I come to think that is not really to be addressed as a “definite typing” unless regarded after the fact as in “we now have a definite term ”, which however is not the meaning we are after.
It might indeed be better if we try to stick to speaking as functional programmers, in order to figure out the right linguistic value of the coreader.
For instance, in a case like the maybe-monad, the functional-programming terminology is linguistically rather straightforward: To say that is almost literally to say in ordinary language that “the term may be of type ”.
We should ask from this perspective how to pronounce the “coreader” . Then it seems to be more something like this:
So maybe – thinking out aloud here – the correct modal adjective is – “anyways” – which is really close to what we need if we read it as: “in any event” or “in one way or another”(!)
Then our modal transform would be:
What do you think?
Ok, good. So the operator acts on the type. But then why the difference with where the paraphrase of speaks of , and yet the paraphrase of doesn’t speak of ? And is it really any? That sounds to me more like a functional assignment.
Instead of
isn’t it more
is ’some (copy of) ’.
Then
I’m reminded of that intricate treatment of each, every, any, all and some by Vendler:
They line up in somewhat surprising ways. Sometimes it has a linear logic feel of available resources:
Sometimes it refers to whose choice it is, again linear logic-like:
These in turn aren’t
And here ’each’ sounds odd, unless one adds something like ’…in turn for you to inspect’.
and yet the paraphrase of doesn’t speak of ?
Oh, it does: If we agree, we would write and read it (following the thesaurus) as:
“The term is of type — in one way or another — anyway — somehow or other.
Seems to make good sense to me.
Also, it’s not really different from your suggestion: “some (or other)”, is it? But we need a shorter version of that as a name for a modality.
Ok. I prefer ’some’ featuring in the expression than ’any’. Not in the truncated existential quantifier sense - some, I don’t know which. But in the specifying sense.
has the feel of . Then maybe ’how’ stands in for , and we have . Or .
All right, I like that!
So then our sentence reads
“”.
This looks good. Now the weakest spot seems to actually be “indefinitely”. It feels more clunky than the other two now and also it tends to be read with a temporal connotation that we don’t want here.
I am undecided, but maybe “randomly” wasn’t that bad, after all?
If we pronounce the reader as “randomly”, then “random access memory” would formally be the modality of ” randomly somehow “.
or ?
’Everyhow’ is archaic: in all ways; in every manner; however; by whatever means.
’Anyhow’: in any way whatever; in any case; at all events; in a careless manner; haphazardly
Perhaps, then.
I see. That’s good.
But then “potentially” in
“”
does not sound right, after all, does it: One wouldn’t want to say that something holds “anyways” as soon as it holds “potentially”.
The adjective in the middle should express truth without reference to the “how” in “somehow”, “anyhow”.
Indeed, the composite implication “” sounds wrong.
The problem is that on in-dependent type we can’t really say “how”, at all, because that would involve referring to the context.
So instead of “somehow” it is more like “alternatively”: We pick some alternative, but without really saying how.
This leads me to suggest something like:
“”
These middle terms in a sense should be doing nothing, no? After all the is , so that is .
Unless we imitate modal logic and see actualisation as an operator which takes a modal proposition to a plain proposition, which we might take to be pullback along the map which singles out the actual world, . After this pullback we have (for all worlds this world some world ).
But then in the in-dependent setting there isn’t anything like this actualisation to be done. Whatever we have as the middle term can’t do anything to the type.
Yes, the middle adjective is not for an operator, it indicates the context that we are in.
It’s becoming a bit of a goose chase, but let’s just keep going while we have the momentum:
One observation is that and ought to be about the same kind of randomness, just that the first is about specific random inputs (namely to coKleisli morphisms of the coreader comonad) while the latter is about unspecific random outputs (produced by Kleisli morphisms for the reader monad):
If we think of both reader and co-reader as dependent on a potentially unspecified global parameter , then
a coreader coKleisli program reads in random but fixed data and it proceeds with that fixed data,
a reader Kleisli program outputs random and unspecified output data , preemptively prepared for all possibilities.
If we read “randomly” in this sense as “random but fixed” input, then this goes to the beginning of our modal sentence, while “indefinitely” can stay on the right:
“”
This is beginning to make more sense: If something definitely holds, but in a random way, then at the very least we deduce that it can potentially hold at all. If then we don’t even recall the definite random data, we remain with something random and indefinite.
Seems a little odd to extract “randomly” from just one of “random but fixed” and “random and indefinite”, but I think maybe I’m missing something about what the end result should look like.
I’m in the process of putting a grant proposal together and in conversations with colleagues promoting the (your) line that with the mathematics right and the logic right for quantum physics, there’s really little “interpretative” work left to do. This met with some scepticism. Think of the twin-slits experiment, they said, how can that not be something odd, demanding interpretation?
So back to the task here, is that the idea that phrasing quantum physics in the right logic, the right modal HoTT, then with a good gloss of natural language words for modalities, the physics becomes plainer? Then we’d better first get the nonlinear case as best we can?
To narrow in on the “correct” linguistic pronounciation of these monads, we can also ask: “What is it that a -algebra handles?”, in the sense of monad-algebras as being “effect handlers” in programming (as Uustalu – and maybe only he – usefully highlights at the beginning of his Lecture 2).
Now, a -algebra is a gadget that knows how to take a list of data dependent on an unspecified parameter and turn it into definite data. So it “handles indefiniteness”, in a useful sense.
What language does one use for the dual?
“What is it that a -coalgebra co-handles”? A -coalgebra is a gadget that takes a list of data and returns data plus a specified parameter.
Surprisingly, aside from some article titles at graded modality, the only reference to ’coeffect’ we only have is at graded monad:
In computer science, monads model effects and comonads coeffects.
I believe the language for co-monads as co-effects should be like so:
Where a Kleisli morphism is a program that causes an external effect
a co-Kleisli morphism is a program subject to an external effect.
For instance
the reader monad causes the effect of producing indeterminate data,
while the coreader comonad is effected by a random choice of data.
So
where a monad algebra handles (and so makes disappear) effects that were caused by programs
a co-monad co-algebra produces an effect that programs get subjected to.
Specifically for the co-reader:
All those coreader coKleisli programs are sitting there waiting for the dice to fall and them to run on the resultuing value. The coreader coalgebra is the kind of black box that produces the actual value all these programs are waiting for.
In particular, a coreader coalebra could produce a random element in the sense of random number generators. Or it could ask the user to produce such an element. Or it could compute such an element by some procedure that it happens to know about . In any case, the result will be random as in “random access memory” from the point of view all those coreader coKleislis waiting to be provided with such input.
Maybe one should speak of cause and effect.
Where a monad encodes a kind of effect of programs
a comonad encodes a kind of cause for programs.
In the case of (co-)readers we’d be speaking of the types of
and
Let’s see if I get this via the pair state monad and store comonad.
The state monad causes indeterminate data on an unknown state and a way to update these states. (This generates a form of randomness, as here.) An algebra makes this effect disappear.
The store comonad is effected by a random choice of state and a way to produce indeterminate data. A coalgebra produces such an effect, and is a kind of lens (as here).
There must be ways to write this more clearly.
[ it’s me, Urs, the system signed me out while I was editing ]
Incidentally, one sees that computer scientists on the web used to be debating how to really think of what the costate comonad does:
On Nov 29 in 2010 on r/haskell here, Russel O’Connor (if I am second-guessing the handle correctly?) polled for opinions on how to best think of the costate comonad. He received a fair number of suggestions. His own suggestion (here) was “selector comonad”.
Curiously, if the time stamps are to be trusted, on the next day, Nov 30 (2010), the same O’Connor (if I am interpreting correctly how he is referred to here?) announces his finding (here) that costate coalgebras are equivalently “lenses” (rather: “very well-behaved lenses”, I gather).
Not sure if this insight was ever fed back into the question of how to think of the costate monad: If “lenses” is the worthwhile paradigm, shouldn’t it be called something like the “lens reader”, providing programs the context of a lens on their input data?
Curious here that even the data structure of “lenses” was advertised to capture situations that “computing is full of” and which are a “classical topic in the database literature” (according to the original 2007 article, p. 2).
So computing has been full of costate coalgebras, all along, and nobody noticed until 2010! Maybe the computing community could have cut some corners had people done their category theory? :-)
Interesting to try to make sense of Aristotle’s Physics as a whole. Thomas Kuhn describes how he could make no sense of it by working backwards from Newtonian physics, say, to see how much Aristotle had anticipated. If you do it this way, Aristotle just seems like a bad scientist. Instead you have to see the total picture and how the parts relate.
So, Aristotle’s idea of motion is very different, including not only locomotion, but the growth of a plant, the changing intensity of a quality, and so on. Change occurs by changing qualities at a place in the substrate, not through the motion of particles. Bodies just are the substrate sufficiently impregnated with qualities.
This feeds into Kuhn’s argument against science converging on the real. It seems to him that in the path from Aristotle to Newton to Einstein that in some respects the outer two are quite similar, field-theoretic.
This raises some interesting questions for us. By invoking Aristotle’s terms in the context of quantum physics, are we agreeing with Kuhn about that similarity?
Probably, instead of reading “Aristotle” it would have been more illuminating to read the notes on Physics made by the builders of the Atikythera mechanism; or those made by the builders of the Pyramids, or those from whoever it was who created the Baalbek megaliths. All lost to time – and what we are left with from all those civilizations now barely serves to provide justification for a good pun in naming a monad.
Well, Ok, but then including fragments of Aristotle is just for amusement.
Maybe I am not following your train of thought.
I would love for us to have a decent entry to which I could point people as a reference for what Aristotle said about potentiality+actuality and what Heisenberg made of it.
I tried to add a minimum given what I could glean from what I found in stolen minutes. I know you have argued (here) against writing on the Lab about philosophical subjects, and please feel free not to, but maybe somebody else reading here could be inspired to join in.
I wouldn’t call that an argument against writing on the nLab about philosophical subjects.
Writing on the history of philosophical thought is of course completely unproblematic. What Aristotle says about potentiality+actuality is a fine topic, though as I was pointing out in #26 it’s by no means a straightforward business, and really it would need to be embedded in a wider discussion of Aristotle’s Physics. We’d be looking for something like SEP: Aristotle’s Natural Philosophy. (But let’s not let the perfect be the enemy of the good.)
The issue I was raising on that other thread is whether it’s right to have any entries which treat some or other philosophical topic timelessly, i.e., not as a series of thoughts particular philosophers have had on it, but as a topic in itself. So when in, say, electromagnetism we can start timelessly
The electromagnetic field is is a gauge field which unifies the electric field and the magnetic field,
Hacker’s argument is that philosophy doesn’t deliver such timeless statements. History, on the other hand, (including the history of philosophy) does deliver timeless statements – Aristotle thought X, Descartes thought Y, etc.
The electromagnetic field will likely always be taken to be a gauge field. Physics has delivered us such a concept. We don’t need a great long back story. For Hacker, it isn’t philosophy’s job to do likewise. What the philosopher can do is enter into a dialogue with a practitioner of some other field to help with the process of conceptual clarification, but they don’t come with some special domain knowledge.
Even amongst those who do see a role for philosophical theorising, just about any SEP article on a topic has little to say of the form ’X is…’, and lots to say about how X has been thought about in many ways, it’s all still highly debated what we should mean by X, etc.
So an article on agency has an intro paragraph on the kind of scope of ’agency’ and then
Debates about the nature of agency have flourished over the past few decades in philosophy…
and off we go with loads of different conceptions and theories.
added pointer to:
1 to 31 of 31