Newest at the top
2025-02-03 11:48:43 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
2025-02-03 11:48:02 +0100 | monochrm | (trebla@216.138.220.146) |
2025-02-03 11:47:27 +0100 | sreaming | (~screaming@37.48.95.216) |
2025-02-03 11:47:12 +0100 | sreaming | (~screaming@37.48.95.216) (Quit: Ping timeout (120 seconds)) |
2025-02-03 11:46:45 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
2025-02-03 11:42:35 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-03 11:40:49 +0100 | CiaoSen | (~Jura@2a05:5800:26f:a800:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
2025-02-03 11:28:14 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 260 seconds) |
2025-02-03 11:16:22 +0100 | merijn | (~merijn@77.242.116.146) merijn |
2025-02-03 11:15:05 +0100 | gehmehgeh | (~user@user/gehmehgeh) gehmehgeh |
2025-02-03 11:13:02 +0100 | sprotte24 | (~sprotte24@p200300d16f26a80008f1d39836015ac5.dip0.t-ipconnect.de) |
2025-02-03 11:04:07 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
2025-02-03 11:01:32 +0100 | alp | (~alp@2001:861:8ca0:4940:c78a:20e1:b983:926e) |
2025-02-03 10:58:41 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
2025-02-03 10:56:07 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f21dc911a675e4b1045.dip0.t-ipconnect.de) acidjnk |
2025-02-03 10:55:42 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f21dc911a675e4b1045.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
2025-02-03 10:54:30 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-03 10:40:47 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f21dc911a675e4b1045.dip0.t-ipconnect.de) acidjnk |
2025-02-03 10:39:01 +0100 | fp1 | (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 248 seconds) |
2025-02-03 10:34:08 +0100 | xstill_ | (xstill@fimu/xstill) xstill |
2025-02-03 10:28:53 +0100 | xstill_ | (xstill@fimu/xstill) (Ping timeout: 248 seconds) |
2025-02-03 10:18:13 +0100 | xstill_ | (xstill@fimu/xstill) xstill |
2025-02-03 10:13:18 +0100 | xacktm | (xacktm@user/xacktm) xacktm |
2025-02-03 10:12:52 +0100 | xacktm | (xacktm@user/xacktm) (Quit: fBNC - https://bnc4free.com) |
2025-02-03 10:11:52 +0100 | fp1 | (~Thunderbi@2001:708:20:1406::10c5) fp |
2025-02-03 10:10:42 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-03 10:09:11 +0100 | __monty__ | (~toonn@user/toonn) toonn |
2025-02-03 10:06:25 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-03 10:03:04 +0100 | xstill_ | (xstill@fimu/xstill) (Ping timeout: 260 seconds) |
2025-02-03 10:00:33 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2025-02-03 09:56:24 +0100 | alp | (~alp@2001:861:8ca0:4940:c78a:20e1:b983:926e) (Remote host closed the connection) |
2025-02-03 09:48:57 +0100 | kuribas | (~user@ptr-17d51emyzmm4mq8sbfo.18120a2.ip6.access.telenet.be) kuribas |
2025-02-03 09:48:54 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
2025-02-03 09:48:43 +0100 | kuribas | (~user@ptr-17d51emyzmm4mq8sbfo.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
2025-02-03 09:48:43 +0100 | <kuribas> | Maybe using a "merge" relation to merge contexts. |
2025-02-03 09:48:43 +0100 | <kuribas> | Right, but then the context is part of the relation. |
2025-02-03 09:48:36 +0100 | euleritian | (~euleritia@dynamic-176-001-212-124.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
2025-02-03 09:48:06 +0100 | <tomsmeding> | (if you want to see the whole type system: Fig 2 + Fig 3 from https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=24c850390fba27fc6f3241cb34ce7bc6f37… ) |
2025-02-03 09:47:05 +0100 | <tomsmeding> | on the other hand, perhaps this just works perfectly fine in a logic system |
2025-02-03 09:46:32 +0100 | <tomsmeding> | and you're allowed to (implicitly in the rule) reorder the environment arbitrarily before said partitioning |
2025-02-03 09:46:13 +0100 | <tomsmeding> | this types function application; the point is that you need to partition the environment over the two subexpressions |
2025-02-03 09:45:53 +0100 | <tomsmeding> | indicating the horizontal bar with '/' |
2025-02-03 09:45:43 +0100 | <tomsmeding> | also it depends a little bit on what type system you're implementing, I think. If you look at a resource-linear type system, you have rules like: {A |- t1 : a -> b B |- t2 : a} / {A, B |- t1 t2 : b} |
2025-02-03 09:45:33 +0100 | <kuribas> | oh, there is even kanren in rust. |
2025-02-03 09:44:41 +0100 | <kuribas> | Right :) If I use minikanren or core.logic, then the occurs check is on by default. |
2025-02-03 09:44:12 +0100 | <tomsmeding> | you were already worrying about the occurs check above |
2025-02-03 09:44:11 +0100 | <kuribas> | Just basic logic relations, I don't see what more I will need. |
2025-02-03 09:44:00 +0100 | <kuribas> | tomsmeding: it seems quite straigtforward. |
2025-02-03 09:43:46 +0100 | drdo6 | drdo |
2025-02-03 09:43:45 +0100 | drdo | (~drdo@bl9-110-63.dsl.telepac.pt) (Ping timeout: 252 seconds) |