| 2024-12-29 00:05:02 +0100 | cowboy8625 | (~cowboy@2605-4A80-7405-640-B51A-FA7D-9084-E360-dynamic.midco.net) |
| 2024-12-29 00:09:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 00:10:10 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-12-29 00:11:07 +0100 | Xe | (~Xe@perl/impostor/xe) Xe |
| 2024-12-29 00:12:54 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 2024-12-29 00:13:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-29 00:23:44 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm, anyone has some insight about why the indexed monad's "bind" has that type? |
| 2024-12-29 00:24:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> "(a -> m j k b) -> m i j a -> m i k b", the two last types makes sense, but the first type "(a -> m j k b)" I'm not too sure about |
| 2024-12-29 00:25:44 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 00:26:13 +0100 | housemate | (~housemate@pa49-185-30-217.pa.vic.optusnet.com.au) (Ping timeout: 248 seconds) |
| 2024-12-29 00:26:21 +0100 | <haskellbridge> | <thirdofmay18081814goya> I'm reading "m i j a" as, the monad indexed by "i", such that "j" depends on "i" |
| 2024-12-29 00:26:37 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-12-29 00:30:17 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 00:30:30 +0100 | <geekosaur> | looks like a straightforward generalization of (a -> m b) -> m a -> m b, with an assumption that the action produces both a new value type and a new index type to go with it, and the result type encodes the initial and final index types while discarding the intermediate one (j) because it becomes k when the action is run |
| 2024-12-29 00:32:01 +0100 | <geekosaur> | the initial state encodes i->j, then the action gives you j->k, meaning the result is i->k |
| 2024-12-29 00:32:41 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm I'll think about the idea of discarding the intermediate index type, ty |
| 2024-12-29 00:33:10 +0100 | <haskellbridge> | <thirdofmay18081814goya> right ok |
| 2024-12-29 00:33:13 +0100 | <haskellbridge> | <thirdofmay18081814goya> that makes more sense, ok ty |
| 2024-12-29 00:33:21 +0100 | <geekosaur> | there isn't much to think about, any more than it's worth thinking about 2+3+4 giving you an intermediate 5 |
| 2024-12-29 00:33:42 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 00:35:40 +0100 | <geekosaur> | AIUI the whole point is that the indexed monad tracks an initial and a final index. individual actions within it produce new "final" indexes which aren't the final index of the entire computation because the next action maps from the first "final" index to a new one |
| 2024-12-29 00:39:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> ok right, I wasn't quite getting that in "m i j a", both "i" and "j" are indextypes |
| 2024-12-29 00:43:50 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 00:45:37 +0100 | foul_owl | (~kerry@193.42.0.124) (Ping timeout: 252 seconds) |
| 2024-12-29 00:46:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> they are from the same indexing type* |
| 2024-12-29 00:47:36 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 2024-12-29 00:47:51 +0100 | <haskellbridge> | <thirdofmay18081814goya> was reading that wrong |
| 2024-12-29 00:48:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 00:52:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> next question is... why two indexes? |
| 2024-12-29 00:53:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> the usage of one index is understandable, e.g. the type of lists with a given length |
| 2024-12-29 00:54:10 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm but maybe you'll two indexes if you're mapping from lists of length n to lists of length m? |
| 2024-12-29 00:54:22 +0100 | <haskellbridge> | <thirdofmay18081814goya> you'll want two indexed* |
| 2024-12-29 00:55:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 00:56:00 +0100 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2024-12-29 00:59:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 00:59:55 +0100 | <geekosaur> | think a and b having different Ord instances |
| 2024-12-29 01:00:21 +0100 | <geekosaur> | so it tracks the original and final Ord instances |
| 2024-12-29 01:00:36 +0100 | foul_owl | (~kerry@174-21-81-201.tukw.qwest.net) foul_owl |
| 2024-12-29 01:01:27 +0100 | lol_ | jcarpenter2 |
| 2024-12-29 01:01:59 +0100 | gentauro | (~gentauro@user/gentauro) gentauro |
| 2024-12-29 01:02:18 +0100 | <geekosaur> | (since one of the uses of indexed monads is to allow things like an indexed monad instance for Set, which normally isn't possible because changing the key type alters the structure to reflect a different Ord instance. AIUI at least) |
| 2024-12-29 01:02:54 +0100 | <geekosaur> | (meaning i, j, k are the key types since those specify the Ord instances, again AIUI) |
| 2024-12-29 01:05:17 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm right |
| 2024-12-29 01:06:39 +0100 | iteratee | (~kyle@162.218.222.207) (Remote host closed the connection) |
| 2024-12-29 01:07:45 +0100 | <geekosaur> | more generally, a would be Map k v, b would be Map k' v', i is k and j is k' |
| 2024-12-29 01:08:22 +0100 | <geekosaur> | and I think mathematically (but sadly not in Haskell's type system) if i == j then it should reduce to a normal non-indexed monad |
| 2024-12-29 01:09:58 +0100 | todi1 | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-12-29 01:10:48 +0100 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-12-29 01:11:01 +0100 | alp | (~alp@128-79-174-146.hfc.dyn.abo.bbox.fr) (Ping timeout: 248 seconds) |
| 2024-12-29 01:12:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 01:15:16 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-12-29 01:15:48 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-12-29 01:16:18 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 2024-12-29 01:18:37 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2024-12-29 01:18:37 +0100 | ljdarj1 | ljdarj |
| 2024-12-29 01:19:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-29 01:25:43 +0100 | <hololeap> | it reminds me of (.|) :: Monad m => ConduitT a b m () -> ConduitT b c m r -> ConduitT a c m r |
| 2024-12-29 01:27:21 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: pillow time) |
| 2024-12-29 01:32:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 01:36:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 01:37:53 +0100 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) (Remote host closed the connection) |
| 2024-12-29 01:38:30 +0100 | <ncf> | geekosaur: i don't think Set is an indexed monad? |
| 2024-12-29 01:40:15 +0100 | <geekosaur> | maybe I'm completely confused, that was what I thought (part of) the point of it was |
| 2024-12-29 01:40:41 +0100 | <ncf> | are you thinking of exofunctors or something |
| 2024-12-29 01:42:05 +0100 | <ncf> | there's some motivation here https://stackoverflow.com/questions/28690448/what-is-indexed-monad |
| 2024-12-29 01:42:11 +0100 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) |
| 2024-12-29 01:42:13 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-12-29 01:43:41 +0100 | Everything | (~Everythin@195.138.86.118) (Quit: leaving) |
| 2024-12-29 01:49:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 01:53:49 +0100 | foul_owl | (~kerry@174-21-81-201.tukw.qwest.net) (Ping timeout: 252 seconds) |
| 2024-12-29 01:54:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 02:01:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 02:06:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-29 02:08:03 +0100 | foul_owl | (~kerry@193.42.0.124) foul_owl |
| 2024-12-29 02:17:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 02:18:58 +0100 | sprotte24 | (~sprotte24@p200300d16f0bfe00711e65c2b30202f1.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2024-12-29 02:22:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-29 02:23:31 +0100 | <ncf> | i guess the one-sentence definition of an indexed monad is "category enriched in the monoidal category of endofunctors with composition" |
| 2024-12-29 02:23:42 +0100 | <ncf> | (the one that monads are just monoids in) |
| 2024-12-29 02:25:55 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-12-29 02:26:37 +0100 | <hololeap> | "with composition" seems like it would be redundant. isn't that implied by it being a category? |
| 2024-12-29 02:27:14 +0100 | <ncf> | with composition as the monoidal product |
| 2024-12-29 02:27:24 +0100 | <ncf> | composition of endofunctors |
| 2024-12-29 02:28:29 +0100 | <ncf> | i.e. the endomorphism monoidal category on Set in the bicategory of categories |
| 2024-12-29 02:30:10 +0100 | <hololeap> | isn't that usually just referred to as "the category of endofunctors" |
| 2024-12-29 02:31:29 +0100 | <hololeap> | (I barely understand this stuff so don't take me too seriously) |
| 2024-12-29 02:31:34 +0100 | <ncf> | well that doesn't tell you which monoidal structure you put on it |
| 2024-12-29 02:32:11 +0100 | <ncf> | i.e. applicative functors are monoids in the category of endofunctors *with Day convolution as the monoidal product* |
| 2024-12-29 02:35:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 02:36:55 +0100 | <hololeap> | ok I think I see what you mean |
| 2024-12-29 02:37:53 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f42bc4ebb891d7561a4.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2024-12-29 02:39:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 02:44:58 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-29 02:47:33 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 2024-12-29 02:52:22 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2024-12-29 02:53:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 02:54:03 +0100 | comonad | (~comonad@p200300d0270bcb00d2bd35ff80c069c9.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2024-12-29 02:54:07 +0100 | Square | (~Square@user/square) (Ping timeout: 264 seconds) |
| 2024-12-29 02:55:47 +0100 | comonad | (~comonad@p200300d027182d00bcfd40be9d94d2dc.dip0.t-ipconnect.de) |
| 2024-12-29 03:00:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-29 03:03:11 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 03:04:56 +0100 | thatonelutenist | (8216c46202@2a03:6000:1812:100::fb3) thatonelutenist |
| 2024-12-29 03:06:24 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-12-29 03:11:40 +0100 | <Leary> | @tell prsteele https://play.haskell.org/saved/J7bdQ5zn |
| 2024-12-29 03:11:41 +0100 | <lambdabot> | Consider it noted. |
| 2024-12-29 03:12:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 03:16:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-29 03:24:00 +0100 | <Leary> | thirdofmay: The Atkey indexed monad has two indices for the same reason `Category` arrows do; its bind performs a kind of composition. Simple examples include the indexed writer monad, which writes category arrows rather than monoids, and the indexed state monad which has distinct types for the initial and final state. |
| 2024-12-29 03:27:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 03:27:53 +0100 | <Leary> | This is clearer when looking at a corresponding indexed applicative: `unit :: f i i (); fuse :: f i j a -> f j k b -> f i k (a, b)` |
| 2024-12-29 03:32:16 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 03:44:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 03:45:04 +0100 | notzmv | (~umar@user/notzmv) (Ping timeout: 265 seconds) |
| 2024-12-29 03:52:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 03:59:50 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm |
| 2024-12-29 04:00:07 +0100 | <haskellbridge> | <thirdofmay18081814goya> we want there to be a strict ordering in the indexing type/sort right? |
| 2024-12-29 04:00:27 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2024-12-29 04:02:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:05:03 +0100 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2024-12-29 04:05:34 +0100 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2024-12-29 04:07:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 04:07:23 +0100 | <haskellbridge> | <thirdofmay18081814goya> thinking about specifically the case where the indexes are given by "Finite n" |
| 2024-12-29 04:07:49 +0100 | <haskellbridge> | <thirdofmay18081814goya> well |
| 2024-12-29 04:08:25 +0100 | <haskellbridge> | <thirdofmay18081814goya> there is no type that can carry more information that either "Finite n" or "Nat", so I think it is a good starting point |
| 2024-12-29 04:08:43 +0100 | <haskellbridge> | <thirdofmay18081814goya> there is no type that can carry more information as an indexing type*** |
| 2024-12-29 04:10:30 +0100 | prasad | (~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net) (Ping timeout: 260 seconds) |
| 2024-12-29 04:11:00 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e. any work that can done by a type, as an indexing type, will be the same as can be done by either "Finite n" or the type of natural numbers |
| 2024-12-29 04:13:37 +0100 | <haskellbridge> | <thirdofmay18081814goya> simply because the work of an indexing type is delimited simply by how many ways you can pattern match on it. i.e. this completely specifies the extent of the work an indexing type can do |
| 2024-12-29 04:14:23 +0100 | <haskellbridge> | <thirdofmay18081814goya> pattern matching, that is |
| 2024-12-29 04:16:00 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2024-12-29 04:17:05 +0100 | <haskellbridge> | <Bowuigi> Wait how? |
| 2024-12-29 04:18:13 +0100 | <Leary> | I don't see what an ordering on the index kind has to do with anything. |
| 2024-12-29 04:18:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: the extent of the work that can be done by an indexing type is that of specifying another type, so it has type "IndexType -> Type", where "IndexType : Type" |
| 2024-12-29 04:19:15 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh |
| 2024-12-29 04:19:18 +0100 | <haskellbridge> | <thirdofmay18081814goya> wait |
| 2024-12-29 04:20:08 +0100 | <haskellbridge> | <thirdofmay18081814goya> that's not the type it has, the choice function in which it serves as the indexing type has that type |
| 2024-12-29 04:20:32 +0100 | <haskellbridge> | <thirdofmay18081814goya> "choiceFunction :: IndexType -> Type", where "IndexType :: Type" |
| 2024-12-29 04:20:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:21:17 +0100 | <haskellbridge> | <thirdofmay18081814goya> Leary: not sure either, just threw that out there to make the problem more concrete |
| 2024-12-29 04:21:19 +0100 | dsrt^ | (dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-29 04:22:24 +0100 | <haskellbridge> | <Bowuigi> I still don't understand how does that limit you to Nat/Fin |
| 2024-12-29 04:25:11 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 04:28:58 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: well, there is nothing in "IndexType :: Type" that can be used to make a value of "Type". so it can only allow you to choose a value. i.e., the term that will result from applying "choiceFunction :: IndexType -> Type" will not contain any term from "IndexType" |
| 2024-12-29 04:29:25 +0100 | <haskellbridge> | <thirdofmay18081814goya> the argument also follows from considering that any term (e.g. in System F) has finitely many symbols and therefore can only have finitely many differences with any other term |
| 2024-12-29 04:30:28 +0100 | <haskellbridge> | <thirdofmay18081814goya> so if you have "someTerm :: Type", it has at most finitely many differences with "anotherTerm :: Type", which means these can be indexed by a function on the naturals |
| 2024-12-29 04:30:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> these differences* |
| 2024-12-29 04:31:21 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Ping timeout: 276 seconds) |
| 2024-12-29 04:34:35 +0100 | td_ | (~td@i5387093F.versanet.de) (Ping timeout: 244 seconds) |
| 2024-12-29 04:35:02 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-12-29 04:35:22 +0100 | <haskellbridge> | <thirdofmay18081814goya> not sure if the same argument could be used for dependent types. for non-dependent types I think it is enough |
| 2024-12-29 04:36:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:36:43 +0100 | td_ | (~td@i5387092B.versanet.de) td_ |
| 2024-12-29 04:37:52 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e. we use the fact that "choiceFunction :: IndexType -> Type" applied to "index :: IndexType" will produce a term "resultingTerm :: Type" which has no subterms like "someSubterm :: IndexType" |
| 2024-12-29 04:38:09 +0100 | <haskellbridge> | <thirdofmay18081814goya> because of non-dependent types |
| 2024-12-29 04:39:01 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-29 04:39:04 +0100 | Typedfern | (~Typedfern@106.red-83-37-34.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2024-12-29 04:39:04 +0100 | typedfern_ | (~Typedfern@106.red-83-37-34.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2024-12-29 04:41:38 +0100 | Typedfern | (~Typedfern@106.red-83-37-34.dynamicip.rima-tde.net) typedfern |
| 2024-12-29 04:43:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 04:46:01 +0100 | <haskellbridge> | <thirdofmay18081814goya> so that means the only "value" or only "worth" of "IndexType" is how many ways it can be different, i.e., its cardinality |
| 2024-12-29 04:46:08 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 04:46:49 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 04:47:46 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 04:48:13 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 04:51:06 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 04:51:31 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 04:56:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:59:16 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 05:01:22 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 05:08:41 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) (Ping timeout: 265 seconds) |
| 2024-12-29 05:13:23 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 05:14:26 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) euandreh |
| 2024-12-29 05:17:56 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 05:29:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 05:29:24 +0100 | <haskellbridge> | <Bowuigi> That makes sense I guess |
| 2024-12-29 05:30:48 +0100 | <haskellbridge> | <Bowuigi> Tho Nat may not be enough, unsure if larger infinities can be represented without dependent types |
| 2024-12-29 05:32:09 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: this is probably taken care of if the alphabet is assumed to be countable. cannot have uncountably-many terms arising from countable alphabet |
| 2024-12-29 05:33:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 05:35:51 +0100 | <haskellbridge> | <Bowuigi> Dedekind/Cauchy reals don't seem to require infinite alphabets |
| 2024-12-29 05:47:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 05:51:01 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 248 seconds) |
| 2024-12-29 05:51:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-29 06:03:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 06:04:16 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Ping timeout: 265 seconds) |
| 2024-12-29 06:05:04 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) Raito_Bezarius |
| 2024-12-29 06:06:46 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Max SendQ exceeded) |
| 2024-12-29 06:08:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-29 06:18:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 06:23:26 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) Raito_Bezarius |
| 2024-12-29 06:24:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-29 06:37:58 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 06:42:41 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-29 06:53:23 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 06:54:48 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) (Remote host closed the connection) |
| 2024-12-29 06:55:08 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) euandreh |
| 2024-12-29 06:55:57 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Quit: leaving) |
| 2024-12-29 06:57:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 07:09:31 +0100 | notzmv | (~umar@user/notzmv) (Ping timeout: 265 seconds) |
| 2024-12-29 07:10:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 07:14:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-29 07:20:04 +0100 | alp | (~alp@2001:861:8ca0:4940:cce8:4f56:ac90:1a49) |
| 2024-12-29 07:28:22 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) (Ping timeout: 265 seconds) |
| 2024-12-29 07:28:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 07:29:35 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) euandreh |
| 2024-12-29 07:35:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 07:41:42 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2024-12-29 07:42:06 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) stiell |
| 2024-12-29 07:44:36 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-12-29 07:48:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 07:51:39 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-12-29 07:53:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-29 07:54:41 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2024-12-29 07:58:19 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2024-12-29 07:59:28 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-29 07:59:28 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 08:03:50 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-29 08:08:06 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-12-29 08:10:40 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-12-29 08:16:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 08:17:29 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-12-29 08:21:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-29 08:32:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 08:33:39 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-12-29 08:37:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 08:39:53 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2024-12-29 08:40:48 +0100 | CiaoSen | (~Jura@2a05:5800:2df:5d00:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-12-29 08:48:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 08:53:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 09:00:02 +0100 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: The Lounge - https://thelounge.chat) |
| 2024-12-29 09:00:02 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-12-29 09:00:39 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2024-12-29 09:04:00 +0100 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) tt1231 |
| 2024-12-29 09:05:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 09:12:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 09:18:46 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2024-12-29 09:18:56 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 09:20:50 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 09:23:51 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 09:25:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 09:27:34 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 09:29:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |