00:55:02 -!- myname has quit (Ping timeout: 258 seconds).
00:56:38 -!- myname has joined.
01:02:14 -!- Lord_of_Life_ has joined.
01:03:00 -!- Lord_of_Life has quit (Ping timeout: 255 seconds).
01:03:35 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
02:45:21 <esolangs> [[Sharp]] M https://esolangs.org/w/index.php?diff=118424&oldid=103545 * PythonshellDebugwindow * (+17) /* Concepts */ Nowiki
03:06:34 -!- ais523 has quit (Quit: quit).
05:00:21 -!- wpa has quit (Quit: Connection closed for inactivity).
05:03:01 <zzo38> I had mention before about "scalar monad" of category of matrices, which would be a identity matrix multiplied and divided by the nonzero scalar number (unless, it is a mistake), and that the Kleisli category is just as good as the original, and that it could also be a comonad just as good as the monad.
05:04:01 <zzo38> But, I guess that identity monad of any category is a kind of scalar monad, and that a scalar monad is also possible by multiplying any category by any abelian group (such as a group of only one element). Is it?
05:24:58 -!- b_jonas has quit (Ping timeout: 260 seconds).
05:25:38 <esolangs> [[Four]] M https://esolangs.org/w/index.php?diff=118425&oldid=77876 * PythonshellDebugwindow * (+118) Categories
05:26:39 -!- b_jonas has joined.
05:30:26 <zzo38> Sometimes a bold 2 is used in category theory to mean a category with two objects and the arrow only one way. But, I think it would be consistent with usual mathematical notation for non-bold numbers to denote discrete categories.
05:31:56 <zzo38> What is your opinion?
06:46:49 -!- tromp has joined.
08:05:06 -!- __monty__ has joined.
08:19:54 -!- Sgeo has quit (Read error: Connection reset by peer).
09:24:03 -!- arseniiv has joined.
10:55:24 <esolangs> [[3 Bits, 3 Bytes]] https://esolangs.org/w/index.php?diff=118426&oldid=118367 * None1 * (+124) Added Python interpreter and implemented category tag
11:00:22 <esolangs> [[Drawfuck]] https://esolangs.org/w/index.php?diff=118427&oldid=105205 * None1 * (+50)
11:00:39 <esolangs> [[Drawfuck]] M https://esolangs.org/w/index.php?diff=118428&oldid=118427 * None1 * (+1)
11:02:01 <esolangs> [[3 Bits, 3 Bytes]] https://esolangs.org/w/index.php?diff=118429&oldid=118426 * None1 * (+23) /* See also */
11:03:09 <esolangs> [[2 Bits, 1 Byte]] https://esolangs.org/w/index.php?diff=118430&oldid=118297 * None1 * (+58)
12:28:21 <esolangs> [[Drawfuck]] https://esolangs.org/w/index.php?diff=118431&oldid=118428 * None1 * (+214)
12:30:51 <esolangs> [[Drawfuck]] M https://esolangs.org/w/index.php?diff=118432&oldid=118431 * None1 * (-1)
12:31:45 <esolangs> [[Drawfuck]] M https://esolangs.org/w/index.php?diff=118433&oldid=118432 * None1 * (-2)
12:34:36 <esolangs> [[User:None1]] https://esolangs.org/w/index.php?diff=118434&oldid=118377 * None1 * (+28) /* My Implementations */
12:46:13 -!- b_jonas has quit (Ping timeout: 255 seconds).
12:48:00 -!- b_jonas has joined.
13:50:37 <esolangs> [[Special:Log/newusers]] create * Huywall * New user account
14:28:52 -!- cpressey has joined.
14:37:48 <cpressey> zzo38: my opinion is that you could probably make it consistent, but I don't see that it gets you anything really interesting
14:38:16 <cpressey> 5+9=14 except 5, 9, and 14 are categories and + is some special operation that takes pairs of categories and yields another category
14:39:17 <cpressey> Other than forcing you to come up with the definition of + in this context that handles the extra structure
14:40:38 <cpressey> But then, I'm heavily biased away from category theory, so don't trust anything I say about it.
14:49:05 <cpressey> For that matter, don't trust anything I say about anything.
14:54:39 -!- Sgeo has joined.
14:58:13 <cpressey> I'm trying to get my brain to do something productive but I'm having no luck.
15:06:41 <tromp> there seems to be no decent statement of the halting problem for lambda calculus online....
15:08:27 <tromp> but several wrong one, that ask if there is a function that given argument x will produce true or false depending on whether x has a normal form
15:08:40 <int-e> try "weak normalization"
15:09:38 <int-e> (There's also solvability which is related and important for semantics (it characterizes non-bottom values) but quite different.)
15:10:32 <tromp> a decent statement would ask for a function that is given a *description* of a term, rather than just the term
15:10:46 <int-e> The "normalization" terminology is a bit overloaded though.
15:11:25 <int-e> tromp: How's that different as long as you don't do infinitary lambda calculus?
15:11:30 <cpressey> The untyped lambda calculus isn't even weakly normalizing
15:11:42 <cpressey> Some terms don't have a normal form
15:12:17 <tromp> if you're just given the term, then the function would have to be strict, and obviously can't yield true or false when given omega
15:12:49 <tromp> but given a description of omega, it could at least recognize that
15:13:01 <int-e> cpressey: Those notions have a term-level meaning too. A term can be weakly normalizing and if you use left-most outermost reduction then that will reach a normal form.
15:14:12 <tromp> e.g. here's a bad statement : https://boarders.github.io/posts/halting1.html
15:15:02 <int-e> Well I think omega is non-terminating, even though it kind of never makes any progress when reducing it.
15:15:05 <cpressey> "Halting problem" feels like "There is no effective algorithm to say whether or not a given term has a normal form"
15:15:29 <tromp> but you must be given a *description* of the term
15:16:12 <int-e> Sorry, I was focussed on defining halting.
15:16:29 <int-e> Sure, you need an encoding of terms to use them as inputs to something else.
15:16:46 <esolangs> [[User:PaxtonPenguin/Sandbox]] https://esolangs.org/w/index.php?diff=118435&oldid=118417 * PaxtonPenguin * (+16)
15:17:01 <tromp> but i couldn't find any such proper statement of the lambda calculus halting problem
15:17:11 <cpressey> Encoding TM's on TM tapes is old hat, encoding lambda terms in lambda terms is less well trodden
15:17:25 <int-e> Which is the kind of thing computability theory is usually very sketchy on, because the details are interchangeable.
15:17:51 <int-e> Whether you use BLC-like lists of bools, or an actual tree type... they can be transcoded.
15:18:53 <esolangs> [[User:PaxtonPenguin/Sandbox]] https://esolangs.org/w/index.php?diff=118436&oldid=118435 * PaxtonPenguin * (+74)
15:19:03 <int-e> And yeah that definition is bad because it foregoes the encoding step.
15:19:15 <esolangs> [[User:PaxtonPenguin/Sandbox]] https://esolangs.org/w/index.php?diff=118437&oldid=118436 * PaxtonPenguin * (+4)
15:20:04 <cpressey> I've seen attempts to add quoting to the lambda calculus, and thought that I'm sure you can also do that with Church-type encodings of some kind, so the quoting doesn't really add anything except convenience.
15:20:06 <int-e> . o O ( Maybe the last person who was precise about encodings was Gödel. ;-) )
15:20:41 <int-e> (I know that to be false but I think it makes a nice piece of shittalk)
15:20:57 <esolangs> [[User:PaxtonPenguin/Sandbox]] https://esolangs.org/w/index.php?diff=118438&oldid=118437 * PaxtonPenguin * (+80)
15:22:32 <esolangs> [[User:PaxtonPenguin/Sandbox]] https://esolangs.org/w/index.php?diff=118439&oldid=118438 * PaxtonPenguin * (+51)
15:22:45 <esolangs> [[User:PaxtonPenguin/Sandbox]] M https://esolangs.org/w/index.php?diff=118440&oldid=118439 * PaxtonPenguin * (+2)
15:23:03 <int-e> tromp: In any case, for you (and also me) BLC is the natural choice I think. You just have to decide whether to use bare lambda terms or the full convention with input.
15:23:44 <tromp> here's a proper proof of impossibility of halting probnlem in lambda calcu;us:
15:24:06 <tromp> Denote by "T" some encoding of lambda term T,
15:24:06 <tromp> and let decode be a corresponding decoder, i.e.
15:24:06 <tromp> Suppose there exist a lambda term hasNF which,
15:24:06 <tromp> when applied to "T" for some lambda term T,
15:24:06 <tromp> results in True when T has a normal form,
15:24:07 <tromp> and in False when T has none.
15:24:07 <tromp> Let P = \p. hasNF (decode p p) Omega Id
15:24:08 <tromp> P "P" = hasNF (int "P" "P") Omega Id
15:24:08 <tromp> = hasNF ( P "P") Omega Id
15:24:08 <tromp> = Omega iff P "P" has a normal form
15:25:02 <tromp> sorry for spamming:(
15:25:04 <int-e> . o O ( s/decode/uni/ )
15:26:51 <int-e> tromp: Per the previous discussion you should pass a description of P "P" to `hasNF`. So more of a hasNF (apply p (quote p))
15:28:30 <esolangs> [[User:PaxtonPenguin/ExtremelyLongNameThatNoOneWillGuess]] N https://esolangs.org/w/index.php?oldid=118441 * PaxtonPenguin * (+4) Created page with "Test"
15:28:49 <tromp> ah, right. thanks for noticing! this is subtle indeed
15:28:52 -!- razetime has joined.
15:35:10 <int-e> Hmm. Something like quote [] = "010110", quote (0:xs) = "01000010010110" ++ quote xs, quote (1:xs) = "010000100101110" ++ quote xs, and apply xs ys = "01" ++ xs ++ ys.
15:35:32 <int-e> BLC is too simple ;-)
15:36:20 <int-e> (The most likely mistake here is that I may have swapped the 0 and 1 in the input of quote)
15:37:08 <int-e> (and of course those two digits are bools)
15:39:09 <arseniiv> <cpressey> Other than forcing you to come up with the definition of + in this context that handles the extra structure => I think disjoint union suffices: objects(C + D) = objects(C) ⊔ objects(D); morphisms are copied as well. No new ones are added
15:40:06 <int-e> Err, and of course `apply` should be using "00" instead of "01". Tsk.
15:41:38 <arseniiv> such a + should ideally satisfy the coproduct definition if taken to a suitable category of categories (e. g. Cat, of all small categories). Probably works for 2-categories and so on, I don’t see anything that needs to be added in those cases
15:43:43 <tromp> so my proof should have these lines instead:
15:43:45 <tromp> Given "T", we can compute the encoding of T applied to "T", denoted "T "T" ".
15:43:51 <tromp> Let P "T" = hasNF "T "T" " Omega Id
15:47:26 <cpressey> arseniiv: I'm slightly suspicious of this "disjoint union" of which you speak. But I don't remember my reasons for that suspicion. Anyway, what you say seems plausible.
15:47:35 <int-e> Sadly that looks ugly in the fixed font. But that notation can actually be nested :)
15:49:52 <arseniiv> zzo38: I think what I saw denoted as 0, 1, 2, 3, … somewhere was indeed discrete categories. Though one could easily see why ordinals as preorder categories can be useful to many people. This is essentially cardinal arithmetic vs. ordinal arithmetic, I suspect at 95%
15:51:27 <arseniiv> cpressey: I’d be interested to know if you remember what it was!
15:51:50 <arseniiv> btw I think disjoint union doesn’t have enough love in math popularization and even just in some math courses
15:52:30 <arseniiv> it’s always cartesian this cartesian that
15:53:04 <int-e> . o O ( Do they also give out cartesian hats? )
15:53:25 <arseniiv> also I embraced universal properties with all my heart when I finally started cracking them one after another
15:53:46 <cpressey> arseniiv: something about how algebraic data types are a luxury; you can do it all with pairs and Either; and Either could be replaced by Kuratowski pairs...?
15:55:27 <cpressey> Of course I guess disjoint union is disjoint union even if you do it with something like Kuratowski pairs
15:56:02 <arseniiv> cpressey: in lambda calculus, sure it all can be encoded, by Scott, some other guy or them jointly, I forget which way is which but it differs in what we recurse to
15:56:21 <arseniiv> I mean more generally, it has so much use in e. g. even examples of structures
15:57:17 <cpressey> Wikipedia is making me think there is no such thing as a Kuratowski pair now. Have I got the name wrong or have I ASCII-ized the letters in it or something
15:57:58 <arseniiv> anecdote: I think I even saw disjoint union in disguise, encoded in its usual way via (0, x) and (1, x), with no calling it by its name. I guess that can be warranted if one doesn’t want to add distractions to the reader but still
15:58:16 <cpressey> Oh I was accidentally searching wiktionary. OK then!
15:58:33 <arseniiv> cpressey: it should be. At first I didn’t remember about them but then I remembered it’s {{x}, {x, y}}
15:58:59 <arseniiv> initially I thought it somehow relates to λ heehee
16:02:39 <cpressey> I guess my suspicion was more about tags -- was trying to see if it's possible to escape that concept. 0 and 1 would still be tags. Kuratowski pair isn't quite right, but it's close. Something like {x} and {{x}}, with the union being {x, {x}}? The "tag" is still there I guess, it's just represented by an extra level of nesting
16:06:26 -!- cpressey has quit (Quit: Client closed).
16:14:38 <arseniiv> cpressey: yeah, I don’t know any representation with no tags, that is if we define disjoint union by concrete implementation
16:15:04 <arseniiv> and don’t have any equivalent concept before that
16:15:55 <arseniiv> like Either and algebraic data types you mentioned
16:22:55 -!- sprout_ has joined.
16:23:42 <arseniiv> one can say implementation with tags is due to A + A ≅ 2 × A and similar equations. Though that requires union to be here because otherwise we can’t inject different operands of + into the same A on rhs not having disjoint union beforehand. So I guess that’s why type theories tend to have disjoint union as a primitive (or algebraic types or inductive types)
16:24:26 <arseniiv> because union as a primitive might not be ideal
16:26:32 -!- sprout has quit (Ping timeout: 258 seconds).
16:28:15 -!- sprout_ has changed nick to sprout.
16:28:50 <arseniiv> because union has universal property based on subtyping A <: B and not functions A → B, in a type system with no explicit subtyping involved, especially no user-definable one, it’s somewhat unhinged; that’s how I get it
16:29:18 <arseniiv> disjoint union has the same property but wrt A → B
16:29:46 <arseniiv> . o O ( set theory with subtyping )
16:29:59 <arseniiv> hm wait it’s the usual one probably
16:33:34 <esolangs> [[Wise]] https://esolangs.org/w/index.php?diff=118442&oldid=118330 * DivergentClouds * (+119) changed branching operators to only check <code>C</code> digits
16:52:16 <esolangs> [[Special:Log/newusers]] create * Philiquaz * New user account
16:57:00 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=118443&oldid=118410 * Philiquaz * (+179)
16:57:15 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
16:57:33 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=118444&oldid=118443 * Philiquaz * (-9)
17:09:20 -!- razetime has quit (Ping timeout: 255 seconds).
17:25:28 -!- tromp has joined.
17:40:59 -!- Wryl-o-the-wisp has quit.
17:41:17 -!- Wryl-o-the-wisp has joined.
18:36:37 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
18:39:18 <esolangs> [[A-SCP-M]] N https://esolangs.org/w/index.php?oldid=118445 * Philiquaz * (+6013) Created page with "'''A-SCP-M''' is an assembly language in the same vein as the SCP project. As a result, it must be contained to being an esoteric joke language, and must not under any circumstances actually be implemented or used. If you feel the vague urge to implement it, or you se
18:55:35 <b_jonas> “algebraic data types are a luxury; you can do it all with pairs and Either” => standard ML goes halfway there: you can define your own algebraic data types, that gives you a disjoint union, but each variant constructor can take only zero or one arguments, so you need tuples to make a product
18:56:11 <b_jonas> though I might be misremembering this
18:58:24 -!- tromp has joined.
19:13:24 <esolangs> [[A-SCP-M]] M https://esolangs.org/w/index.php?diff=118446&oldid=118445 * PythonshellDebugwindow * (+52) Categories
19:15:31 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=118447&oldid=118375 * PythonshellDebugwindow * (+14) /* A */ add
20:26:41 <arseniiv> b_jonas: yeah I saw that in code though haven’t read exactly ML docs/definitions. I think each constructor takes exactly one argument and you use `unit` (IIRC) in case there are effectively none, like Haskell’s ()
20:27:09 <arseniiv> having 0 or 1 looks unsystematic enough to be eschewed
20:32:04 <b_jonas> arseniiv: might be unsysthematic but no argument constructor is real, see the fieldnum type in view-source:http://math.bme.hu/~ambrus/pu/olvashato/aknakereso.sml for exmaple
20:32:54 <arseniiv> b_jonas: quirky. Then I don’t know how it happened to ML
20:33:57 <b_jonas> but of course that doesn't prove that there aren't curry-style multi-argument constructors too, even if I don't have them in my code
20:35:38 <arseniiv> though in all examples I have seen in articles and such, I never encountered that either
20:36:41 <arseniiv> it looks like a feature of ML languages but maybe some of them added syntax?
20:39:30 -!- arseniiv has quit (Quit: gone too far).
21:07:59 -!- __monty__ has quit (Quit: leaving).
21:36:01 -!- tromp has quit (Read error: Connection reset by peer).
22:54:30 -!- ais523 has joined.