Newest at the top
| 2024-05-13 14:39:26 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-13 14:38:52 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-13 14:32:52 +0200 | sandbag | (~syscall@user/sandbag) |
| 2024-05-13 14:29:15 +0200 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 2024-05-13 14:10:23 +0200 | yin | (~yin@user/zero) (Remote host closed the connection) |
| 2024-05-13 14:07:20 +0200 | drdo | (~drdo@bl5-29-74.dsl.telepac.pt) |
| 2024-05-13 14:07:19 +0200 | billchenchina | (~billchenc@103.152.35.21) |
| 2024-05-13 14:06:55 +0200 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Max SendQ exceeded) |
| 2024-05-13 14:06:03 +0200 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) |
| 2024-05-13 14:05:22 +0200 | <ncf> | and then if you wanted to somehow compose that with _head then that would turn into P(s) → P(over _head f s) |
| 2024-05-13 14:04:05 +0200 | <ncf> | like, in order to set (f : String → String) over the first component of Σ (s : String) P(s) you'd have to also provide a proof that P(s) → P(f(s))... but then you're not gaining anything from the lens interface |
| 2024-05-13 13:59:31 +0200 | <int-e> | . o O ( back to the BASICs ) |
| 2024-05-13 13:58:09 +0200 | syscall1 | (~syscall@2409:40c1:500a:3a4f:1bf3:ed53:e9f:88f4) (Quit: WeeChat 4.2.2) |
| 2024-05-13 13:57:54 +0200 | <syscall1> | LIST |
| 2024-05-13 13:54:32 +0200 | danse-nr3 | (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 2024-05-13 13:54:10 +0200 | danse-nr3 | (~danse-nr3@an-19-162-214.service.infuturo.it) (Ping timeout: 255 seconds) |
| 2024-05-13 13:54:03 +0200 | <ncf> | hmm this is probably not what dependent lenses actually achieve though |
| 2024-05-13 13:51:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-13 13:49:23 +0200 | danse-nr3 | (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 2024-05-13 13:49:23 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) |
| 2024-05-13 13:47:07 +0200 | <ncf> | (https://www.twanvl.nl/blog/haskell/isomorphism-lenses) |
| 2024-05-13 13:46:37 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-05-13 13:46:12 +0200 | <ncf> | just like a regular Lens a b is some type c with an isomorphism a ≃ b × c |
| 2024-05-13 13:45:54 +0200 | <ncf> | sure, the type is not very interesting on its own, it's just part of the definition of the lens |
| 2024-05-13 13:44:52 +0200 | <kuribas> | Just use Int then. |
| 2024-05-13 13:44:48 +0200 | <kuribas> | But a string that is "isomorphic" to Int is not very useful. |
| 2024-05-13 13:44:09 +0200 | <ncf> | oh, so that's what i wrote then |
| 2024-05-13 13:44:00 +0200 | <kuribas> | ncf: idris dependent pair operator |
| 2024-05-13 13:43:02 +0200 | <ncf> | i don't think you can do this in haskell |
| 2024-05-13 13:42:48 +0200 | <ncf> | the point is to have a dependent lens that lets you modify the first component of the sigma type that is "isomorphic" to Int |
| 2024-05-13 13:41:31 +0200 | <ncf> | what's ** ? |
| 2024-05-13 13:41:14 +0200 | <kuribas> | But then why not just use Int? |
| 2024-05-13 13:40:44 +0200 | <kuribas> | Or (s ** IsJust (readMaybe s : Maybe Int)) |
| 2024-05-13 13:39:55 +0200 | <kuribas> | ncf: IsJust (readMaybe s : Maybe Int) |
| 2024-05-13 13:39:51 +0200 | syscall1 | (~syscall@2409:40c1:500a:3a4f:1bf3:ed53:e9f:88f4) |
| 2024-05-13 13:30:17 +0200 | <[exa]> | like, I'll try to do that in free time over the summer. Guess will post it here in case anything materializes |
| 2024-05-13 13:29:58 +0200 | <[exa]> | dmj`: re the MicroHs, I've got a tiny assembly graph reducing machine here and it looks like it could evaluate the combinators just as well. Which would be great because the footprint of microhs would basically lose the C compiler requirement, and there are a few other funny ways to make it portable |
| 2024-05-13 13:24:40 +0200 | gehmehgeh | gmg |
| 2024-05-13 13:24:31 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 2024-05-13 13:19:43 +0200 | syscall1 | (~syscall@2409:40c1:500a:3a4f:edc2:acd4:e500:7824) (Ping timeout: 256 seconds) |
| 2024-05-13 13:19:37 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-13 13:19:10 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 264 seconds) |
| 2024-05-13 13:17:27 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2024-05-13 13:16:38 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2024-05-13 13:10:54 +0200 | hammond | (proscan@gateway02.insomnia247.nl) (Remote host closed the connection) |
| 2024-05-13 13:09:49 +0200 | <ncf> | Σ (s : String) "s parses as an Int" |
| 2024-05-13 13:09:29 +0200 | <ncf> | approximating Int as a subtype of String |
| 2024-05-13 13:08:46 +0200 | <ncf> | maybe you could achieve something like this lawfully in a dependently typed language, with dependent lenses (https://www.cse.chalmers.se/~nad/publications/danielsson-dependent-lenses.pdf) |
| 2024-05-13 13:01:59 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2024-05-13 13:00:35 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 264 seconds) |