Newest at the top
| 2024-10-28 11:31:04 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-28 11:30:47 +0100 | euleritian | (~euleritia@dynamic-176-003-032-186.176.3.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-28 11:27:42 +0100 | euleritian | (~euleritia@dynamic-176-003-032-186.176.3.pool.telefonica.de) |
| 2024-10-28 11:27:06 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2024-10-28 11:26:08 +0100 | ubert | (~Thunderbi@178.165.189.55.wireless.dyn.drei.com) ubert |
| 2024-10-28 11:25:53 +0100 | <dminuoso> | Instead I was confused by the mixture of language and non-language constructs. :-) |
| 2024-10-28 11:25:06 +0100 | <Leary> | You can mentally replace the type-function expressions with `Kleisli f` and `Tannen f (->)`, I just didn't want to confuse my meta-notation with language constructs. They /are/ Categories in the same sense that many types /are/ Functor: their instance exists and is unique. |
| 2024-10-28 11:24:08 +0100 | <ncf> | well, we're talking about what the notation denotes, not the notation itself |
| 2024-10-28 11:23:43 +0100 | mceresa | (~mceresa@user/mceresa) (Ping timeout: 245 seconds) |
| 2024-10-28 11:22:58 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-28 11:22:56 +0100 | <ncf> | Monad f ⇔ Category (Kleisli f) |
| 2024-10-28 11:22:46 +0100 | <dminuoso> | How can "some abstract mathematical notation" "be a" (instance of?) Category? |
| 2024-10-28 11:22:40 +0100 | <ncf> | (a b ↦ a → f b) is Kleisli f |
| 2024-10-28 11:22:18 +0100 | <dminuoso> | I dont understand what that original statement by Leary means exactly. |
| 2024-10-28 11:22:07 +0100 | <ncf> | lambda abstraction |
| 2024-10-28 11:22:00 +0100 | <ncf> | dminuoso: no, that's just ↦ |
| 2024-10-28 11:21:50 +0100 | <ncf> | but anyway k is the type of objects there, so when you say (λ a b → a → f b) is a Category you mean the type of objects of that category is Type and the morphisms between a and b are functions a → f b |
| 2024-10-28 11:21:23 +0100 | Nixkernal | (~Nixkernal@52.131.63.188.dynamic.cust.swisscom.net) Nixkernal |
| 2024-10-28 11:21:19 +0100 | <dminuoso> | So :-> is meant as an actual type constructor? |
| 2024-10-28 11:21:00 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-10-28 11:20:59 +0100 | <ncf> | hm i guess that's not true any more, the argument to Category can have kind k → k → Type |
| 2024-10-28 11:20:13 +0100 | <ncf> | Haskell's Category is a typeclass for defining a category whose type of objects is Type |
| 2024-10-28 11:16:53 +0100 | habib | (~habib@146.70.119.186) (Ping timeout: 248 seconds) |
| 2024-10-28 11:15:34 +0100 | <dminuoso> | What is the difference between Category and category? |
| 2024-10-28 11:15:26 +0100 | <dminuoso> | Then I'm slightly more confused. |
| 2024-10-28 11:15:15 +0100 | <Leary> | (I wasn't able to study CT in university, and haven't gotten around to studying it since, so I don't really know what they say) |
| 2024-10-28 11:13:48 +0100 | <Leary> | Note that I specifically wrote Category, not category. |
| 2024-10-28 11:12:50 +0100 | <dminuoso> | I'm just surprised because I have not seen it before. |
| 2024-10-28 11:12:33 +0100 | <dminuoso> | Leary: Is the expression: "`a b :-> ...` is a category" something category theorists normally say? |
| 2024-10-28 11:09:32 +0100 | <Leary> | :-> is \mapsTo, it's a mathematician's equivalent of lambda syntax. The closest Haskell equivalent of that type level function being `Kleisli`, and the other being `Tannen`. |
| 2024-10-28 11:09:29 +0100 | <ncf> | a function with type Type → Type → Type |
| 2024-10-28 11:08:50 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2024-10-28 11:07:03 +0100 | <dminuoso> | Leary: What does `a b :-> a -> f b` denote? |
| 2024-10-28 11:05:48 +0100 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 2024-10-28 11:02:34 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2024-10-28 11:01:54 +0100 | Guest13 | (~Guest13@2607:fea8:539d:9a00:51a6:57e6:262a:18cb) (Quit: Client closed) |
| 2024-10-28 11:01:33 +0100 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-28 10:53:01 +0100 | ubert | (~Thunderbi@77.119.173.172.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 2024-10-28 10:43:20 +0100 | rvalue- | rvalue |
| 2024-10-28 10:39:09 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 276 seconds) |
| 2024-10-28 10:37:30 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2024-10-28 10:30:18 +0100 | Guest13 | (~Guest13@2607:fea8:539d:9a00:51a6:57e6:262a:18cb) |
| 2024-10-28 10:29:10 +0100 | <Leary> | f is a Monad iff `a b :-> a -> f b` is a Category; f is an Applicative iff `a b :-> f (a -> b)` is a Category. The standard formulation of their laws is abysmal, and should be eradicated from the documentation. |
| 2024-10-28 10:26:18 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-28 10:25:36 +0100 | acidjnk_new | (~acidjnk@p200300d6e72cfb16704d6a71e163a8ef.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2024-10-28 10:23:42 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-10-28 10:23:02 +0100 | <kaol> | For sure. One look and you go "oh that's just a monoid". Not going to happen with the bind formulation. |
| 2024-10-28 10:21:54 +0100 | <tomsmeding> | *much nicer (sorry for the newline) |
| 2024-10-28 10:21:47 +0100 | <tomsmeding> | also the monad laws get |
| 2024-10-28 10:18:56 +0100 | chele | (~chele@user/chele) chele |