Newest at the top
| 2025-02-24 11:49:33 +0100 | <ncf> | i don't understand the question but see https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory |
| 2025-02-24 11:48:57 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50e1932e8352fc3c3c.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-02-24 11:46:14 +0100 | <euouae> | I vaguely have heard of something about cartesian-closed categories, but I'm not sure if they capture all the salient points. What is the idea then? How are functors to be understood in type theory if there is no categorical formulation of it? Or am I missing something? |
| 2025-02-24 11:45:17 +0100 | <euouae> | From my studies on type theory, e.g. the lambda cube, I can't seem to figure out how type theory (theories) is formalized on category theory. I'm not sure if it is known or not. |
| 2025-02-24 11:44:40 +0100 | <euouae> | Hello I've been thinking about statements such as 'monads are just ... in the category of endofunctors' (fill in blank for me because I don't know it exactly) |
| 2025-02-24 11:44:18 +0100 | euouae | (~euouae@user/euouae) euouae |
| 2025-02-24 11:43:57 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-02-24 11:42:50 +0100 | euleritian | (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-02-24 11:38:32 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Remote host closed the connection) |
| 2025-02-24 11:38:28 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 11:36:52 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 11:32:31 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 11:22:32 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-02-24 11:16:44 +0100 | kuribas | (~user@2a02:1810:2825:6000:f4c8:b5d5:3a82:9bab) kuribas |
| 2025-02-24 11:13:19 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-02-24 11:12:47 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-02-24 11:01:59 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 10:53:27 +0100 | fp | (~Thunderbi@130.233.70.89) fp |
| 2025-02-24 10:51:36 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.1) |
| 2025-02-24 10:51:29 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-02-24 10:50:21 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2025-02-24 10:48:33 +0100 | harveypwca | (~harveypwc@2601:246:d080:f6e0:34b5:bbb2:c6c:1ef6) (Quit: Leaving) |
| 2025-02-24 10:46:46 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 10:46:27 +0100 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 276 seconds) |
| 2025-02-24 10:42:40 +0100 | zmt01 | (~zmt00@user/zmt00) zmt00 |
| 2025-02-24 10:42:11 +0100 | <Athas> | I suppose. I really don't want to be in the business of building abstractions, however. |
| 2025-02-24 10:41:25 +0100 | <tomsmeding> | you could always roll your own 2-dimensional array with manual divMod indexing |
| 2025-02-24 10:41:01 +0100 | <tomsmeding> | ah, that's how you got into this. :) |
| 2025-02-24 10:40:39 +0100 | <Athas> | I may just end up with vectors-of-vectors, even though it's not very efficient. |
| 2025-02-24 10:40:29 +0100 | <Athas> | I got started on porting your GMM implementation to 'vector', but it is really tedious. |
| 2025-02-24 10:39:26 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50e1932e8352fc3c3c.dip0.t-ipconnect.de) acidjnk |
| 2025-02-24 10:37:00 +0100 | <tomsmeding> | that is to say, if Accelerate had a bespoke syntax with syntax for types that encouraged rank polymorphism, perhaps people would have less problems with it |
| 2025-02-24 10:36:44 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-02-24 10:36:25 +0100 | <tomsmeding> | perhaps difficulty with Accelerate's model is also engendered a bit by the typing of the embedded language |
| 2025-02-24 10:35:49 +0100 | <tomsmeding> | Athas: that's true |
| 2025-02-24 10:35:32 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50b85661171ead7665.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2025-02-24 10:32:57 +0100 | <Athas> | tomsmeding: but on the other hand, you can efficiently and sanely express multi-dimensional things. |
| 2025-02-24 10:31:47 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 10:30:34 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 10:27:56 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-02-24 10:18:46 +0100 | chele | (~chele@user/chele) chele |
| 2025-02-24 10:16:48 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-02-24 10:15:41 +0100 | unlucy | (sid572875@user/unlucy) unlucy |
| 2025-02-24 10:14:27 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 10:13:49 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) sa |
| 2025-02-24 10:11:55 +0100 | unlucy | (sid572875@user/unlucy) (Ping timeout: 244 seconds) |
| 2025-02-24 10:10:13 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 248 seconds) |
| 2025-02-24 10:05:20 +0100 | euleritian | (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) |
| 2025-02-24 10:05:05 +0100 | <lambdabot> | return x = [x] |
| 2025-02-24 10:05:05 +0100 | <ski> | @src [] return |