Newest at the top
| 2024-05-16 10:41:05 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-05-16 10:40:45 +0200 | _bo | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) (Quit: Leaving) |
| 2024-05-16 10:37:04 +0200 | frumon | (~Frumon@user/Frumon) (Leaving) |
| 2024-05-16 10:32:39 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) |
| 2024-05-16 10:25:53 +0200 | <ski> | (i may be missing some detail, or getting some details wrong, but that's my impression, from reading some papers about it, semi-recently .. still need to play around more in the implementation, though) |
| 2024-05-16 10:24:19 +0200 | <ski> | (they have unification of lambda terms, up to alpha-, beta-, and eta- conversion. but lambda terms are rather weak, can't compute on sum types, and no recursion. you do computation not with functions, but with predicates/relations, iow logic programming, searching for proofs/values of propositions/types) |
| 2024-05-16 10:22:36 +0200 | <ski> | aiui, this is because (a) they purposely want a rather weak theory, to not assume too much, when representing object systems (logics, type systems, operational semantics, &c.); but also (b) in order to keep unification and type checking decidable |
| 2024-05-16 10:20:54 +0200 | <ski> | yep |
| 2024-05-16 10:20:24 +0200 | <kuribas`> | right, no type 1, type 2, ... as in idris2 |
| 2024-05-16 10:20:15 +0200 | <ski> | it's a fairly conservative/restrictive theory |
| 2024-05-16 10:19:44 +0200 | <ski> | bu there's no infinite tower of sorts |
| 2024-05-16 10:19:35 +0200 | <ski> | no, LF is dependently typed to begin with |
| 2024-05-16 10:19:22 +0200 | <kuribas`> | Twelf is dependently typed Elf? |
| 2024-05-16 10:19:01 +0200 | <ski> | (in LF, the Logical Framework system, that Elf is based on, and of which Twelf is an implementation of) |
| 2024-05-16 10:18:19 +0200 | <ski> | there are three levels, values, types, and kinds |
| 2024-05-16 10:17:40 +0200 | <kuribas`> | ski: so types are not values then? |
| 2024-05-16 10:16:46 +0200 | <ski> | kuribas` : aiui, no parametric polymorphism, types only depend on values, not types; iirc, in original implementation, they had that, but they didn't include it in the reworked implementation (yet at least), because the theory for it was unclear |
| 2024-05-16 10:15:27 +0200 | danza | (~francesco@an-19-164-164.service.infuturo.it) (Remote host closed the connection) |
| 2024-05-16 10:03:14 +0200 | danza | (~francesco@an-19-164-164.service.infuturo.it) |
| 2024-05-16 10:02:54 +0200 | titibandit | (~user@user/titibandit) |
| 2024-05-16 10:02:03 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-05-16 09:56:54 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-05-16 09:49:30 +0200 | <kuribas`> | https://twelf.org/wiki/equality/ |
| 2024-05-16 09:46:51 +0200 | <kuribas`> | perhaps offtopic, but I looked at twelf, and I am surprised you need to reinvent equality (refl, cong, ...) for each datatype. |
| 2024-05-16 09:44:11 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 09:42:21 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 2024-05-16 09:36:41 +0200 | bilegeek | (~bilegeek@2600:1008:b010:1cfe:3776:17b8:1dc2:3fdf) (Quit: Leaving) |
| 2024-05-16 09:33:31 +0200 | <tomsmeding> | but true |
| 2024-05-16 09:33:02 +0200 | <tomsmeding> | with slightly more overhead |
| 2024-05-16 09:32:35 +0200 | <c_wraith> | and a TVar-based approach lets you write much more obviously-correct code that works under the write-light conditions. |
| 2024-05-16 09:30:55 +0200 | bo_ | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) (Ping timeout: 256 seconds) |
| 2024-05-16 09:30:46 +0200 | <tomsmeding> | hence the "write-light" observed above |
| 2024-05-16 09:30:38 +0200 | <tomsmeding> | of course |
| 2024-05-16 09:30:31 +0200 | <c_wraith> | in practice, an MVar-based implementation will perform way better with heavy writes. |
| 2024-05-16 09:29:30 +0200 | <tomsmeding> | and observing that this cleverer implementation does not have stronger preconditions than the MVar-based one |
| 2024-05-16 09:29:28 +0200 | kuribas` | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-05-16 09:29:12 +0200 | <tomsmeding> | I'm looking at an idealised implementation in terms of `MVar (Map Key Value)` |
| 2024-05-16 09:28:37 +0200 | <c_wraith> | You're adding extra semantics. I'm looking at the type. :P |
| 2024-05-16 09:28:09 +0200 | <tomsmeding> | I that would be a requirement from the interface of getRefForKey anyway, regardless of the implementation |
| 2024-05-16 09:27:45 +0200 | _bo | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) |
| 2024-05-16 09:27:07 +0200 | <c_wraith> | Ok, it works on the assumption that the value you want to insert doesn't depend on whether there was already a key there or not (or depends trivially, with some sort of commutative operation) |
| 2024-05-16 09:23:57 +0200 | frumon | (~Frumon@user/Frumon) |
| 2024-05-16 09:22:25 +0200 | <tomsmeding> | write-light, then |
| 2024-05-16 09:22:17 +0200 | <tomsmeding> | :D |
| 2024-05-16 09:21:41 +0200 | <Axman6> | actually that's not true, since things were only read when a uses used the webservice, which no one ever did =) |
| 2024-05-16 09:21:39 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-05-16 09:21:05 +0200 | <Axman6> | yeah - which my one use case for this particular design was =) |
| 2024-05-16 09:20:44 +0200 | <tomsmeding> | also needs a read-heavy workload |
| 2024-05-16 09:20:31 +0200 | <tomsmeding> | but if that's enough, it's nice |
| 2024-05-16 09:20:27 +0200 | <tomsmeding> | gets you a limited interface though, to the map |