Newest at the top
| 2024-05-13 15:29:54 +0200 | <mauke> | in that a parse error will implicitly terminate the block |
| 2024-05-13 15:29:33 +0200 | <mauke> | if your lambda calculus uses layout rules for lambda bodies, then it is "right", I think |
| 2024-05-13 15:29:30 +0200 | <int-e> | you can verify that if you replace each \x.( by (\x. then things make sense with a Haskell-like convention. |
| 2024-05-13 15:28:26 +0200 | <mauke> | if your lambda calculus uses BlockArguments, then it is "wrong" |
| 2024-05-13 15:28:26 +0200 | <int-e> | hmm, yes. |
| 2024-05-13 15:28:13 +0200 | <int-e> | hmm, no |
| 2024-05-13 15:27:45 +0200 | <int-e> | apparently they use \x.(...) for a lambda abstraction and it binds stronger than application |
| 2024-05-13 15:27:12 +0200 | <mauke> | depends on what conventions you use |
| 2024-05-13 15:25:42 +0200 | <ski> | not if that's supposed to be a Y combinator, assuming usual precedence rules for application and lambda abstraction |
| 2024-05-13 15:23:21 +0200 | <zzz> | is this parenthesized correctly? https://i.stack.imgur.com/WQtuk.jpg |
| 2024-05-13 15:22:29 +0200 | _bo | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) |
| 2024-05-13 15:22:11 +0200 | danse-nr3 | (~danse-nr3@an-19-162-214.service.infuturo.it) (Ping timeout: 264 seconds) |
| 2024-05-13 15:07:52 +0200 | danse-nr3 | (~danse-nr3@an-19-162-214.service.infuturo.it) |
| 2024-05-13 15:07:23 +0200 | danse-nr3 | (~danse-nr3@an-19-162-214.service.infuturo.it) (Ping timeout: 256 seconds) |
| 2024-05-13 15:05:52 +0200 | zzz | (~yin@user/zero) |
| 2024-05-13 15:02:31 +0200 | <dmj`> | [exa]: very cool, which assembly language |
| 2024-05-13 14:52:21 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 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)) |
