Newest at the top
| 2025-12-01 22:04:17 +0100 | <ski> | EvanR : `r' is a substitution, a (value) environment, a (partial) function from variables to terms. so, if `r' is the (partial) function `y |-> x' (think `\Y -> X', in Haskell notation), and `t' is `f y x', then `[r] t' is `[y |-> x] (f y x)' (`subst (\Y -> X) (App (App F Y) X)') becomes `f x x' (`App (App F X) X') |
| 2025-12-01 22:02:10 +0100 | <tomsmeding> | [exa]: [x,y) is the standard one, it's [x,y[ that I was complaining about |
| 2025-12-01 22:01:25 +0100 | <haskellbridge> | <doc> okay that's a relief, all this is what i'd say too, but realized that the other direction (esp with |->) also has some sort of rationale |
| 2025-12-01 22:00:18 +0100 | <ski> | doc : think of `[y:=x]' as `x' is assigned into mutable slot `y', or as `y' is now defined as being `x' |
| 2025-12-01 21:59:37 +0100 | <geekosaur> | *ghc |
| 2025-12-01 21:59:08 +0100 | <ski> | doc : for `[y:=x]', it's "y is replaced by x" (i've not seen anyone use the opposite interpretation here, thankfully). for `[y |-> x]', it also (imho) ought to be "y is replaced by x", but i'm pretty sure i've seen at least somewhere the opposite interpretation |
| 2025-12-01 21:57:51 +0100 | <EvanR> | ski, I'm not understanding your definitions above. What's r(x) |
| 2025-12-01 21:57:08 +0100 | <fgarcia> | would it be possible to use those terms in functions? then f(y) could be written as a substitution for f(x) |
| 2025-12-01 21:56:50 +0100 | <ski> | this is similar to defining a linear transformation, from a based vector space, by specifying where it maps the basis vectors, and then extending it by linearity |
| 2025-12-01 21:56:16 +0100 | <geekosaur> | ghcc was held back to 9.4 until 9.6.7 fixed a key bug |
| 2025-12-01 21:55:51 +0100 | <geekosaur> | for example, cabal was for a long time held back to an old version due to a windows bug that only got fixed when a windows dev found some time to work on it |
| 2025-12-01 21:55:19 +0100 | <ski> | ... |
| 2025-12-01 21:55:18 +0100 | <geekosaur> | mostly on widest compatibility/lack of bugs |
| 2025-12-01 21:55:17 +0100 | <ski> | [r] (t u) = ([r] t) ([r] u) |
| 2025-12-01 21:55:08 +0100 | <ski> | [r] x = x if r(x) undefined |
| 2025-12-01 21:55:01 +0100 | <ski> | [r] x = t if r(x) defined and t = r(x) |
| 2025-12-01 21:54:26 +0100 | <mauke> | vibes? |
| 2025-12-01 21:53:35 +0100 | karenw | (~karenw@user/karenw) (Ping timeout: 240 seconds) |
| 2025-12-01 21:53:33 +0100 | <merijn> | What does ghcup base it's recommend versions on? |
| 2025-12-01 21:53:20 +0100 | <haskellbridge> | <doc> well now I'm confused too.. is [y:=x] and [y |-> x] "x is replaced by y" or "y is replaced by x", because the former can be interpreted as "y gets plugged into wherever x occurs", and the latter is "y gets expanded into x" |
| 2025-12-01 21:52:01 +0100 | ouilemur | (~jgmerritt@user/ouilemur) (Quit: WeeChat 4.7.0) |
| 2025-12-01 21:47:11 +0100 | <ski> | but i'm sure someone would hold the other interpretation, just to confuse things |
| 2025-12-01 21:46:38 +0100 | <RMSBach> | I guess interpretation flies in the face of the intelligibility of the mark even when we escape natural language |
| 2025-12-01 21:46:37 +0100 | <EvanR> | visually a think of substitution as some term coming in and overwriting the x |
| 2025-12-01 21:46:02 +0100 | <RMSBach> | That's how I read it too |
| 2025-12-01 21:45:54 +0100 | <ski> | the latter (is what i would say) |
| 2025-12-01 21:45:35 +0100 | <EvanR> | or is it y transforms to x |
| 2025-12-01 21:45:33 +0100 | <ski> | (the idea being that you have a mapping from variables to terms, and then you (monadically) extend that to also apply to arbitrary term inputs) |
| 2025-12-01 21:45:17 +0100 | <EvanR> | x gets replaced with y, got it |
| 2025-12-01 21:44:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-01 21:44:02 +0100 | <ski> | there's also `[y |-> x]' |
| 2025-12-01 21:43:48 +0100 | <RMSBach> | I think the majority of lambda calculus materials I have read used that notation for beta reduction |
| 2025-12-01 21:41:43 +0100 | <RMSBach> | I vote for `[y:=x]` fwiw] |
| 2025-12-01 21:41:08 +0100 | <ski> | [exa] : which middle value ? |
| 2025-12-01 21:40:27 +0100 | <ski> | (also, if you respond like that, it looks like you're quoting me, which looks confusing) |
| 2025-12-01 21:40:00 +0100 | <ski> | RMSBach : yea, i'm not really much familiar with the phrase, in a colloquial sense, either |
| 2025-12-01 21:39:49 +0100 | <RMSBach> | exa: Prepositions are often confusing without full command of a foreign language. `por` and `para` present problems for English speakers learning English. But point taken. |
| 2025-12-01 21:37:08 +0100 | <[exa]> | RMSBach: tbh for non-english people the meaning of `for` is completely inexplicable in the phrase |
| 2025-12-01 21:36:22 +0100 | <[exa]> | ski: yeah I sometimes use that too if I've got the middle value to write |
| 2025-12-01 21:35:42 +0100 | <RMSBach> | I will admit that if we change the preposition to "with" then the order of the nominal phrases can be switched at least colloquially. |
| 2025-12-01 21:35:09 +0100 | <ski> | [exa] : mayhaps ⌜{x ≤ < y}⌝, or something along those lines .. |
| 2025-12-01 21:33:42 +0100 | <RMSBach> | <ski> I won't fault anyone for needing a moment to think about it, but it follows standard English, ex "substitute cornstarch for AP flower if necessary" |
| 2025-12-01 21:33:28 +0100 | <ski> | mm |
| 2025-12-01 21:33:14 +0100 | <EvanR> | maybe the issue is with english |
| 2025-12-01 21:33:04 +0100 | <EvanR> | substitute x, does this phrase mean x is going in, or being replaced |
| 2025-12-01 21:32:47 +0100 | <ski> | (my immediate reading, when first encountering it, was the opposite reading of the intended one) |
| 2025-12-01 21:32:27 +0100 | <[exa]> | what's the better way to write [x,y) interval btw? (I thought that one is pretty much standard) |
| 2025-12-01 21:31:40 +0100 | <ski> | for a long time i had to second-think, reminding myself that `y' was being replaced by `x', rather than the other way around, in that "substitute .. for .. in .." phrase |
| 2025-12-01 21:31:29 +0100 | peterbecich | (~Thunderbi@172.222.148.214) (Ping timeout: 260 seconds) |
| 2025-12-01 21:31:21 +0100 | <[exa]> | if someone's syntax looks like a stupid joke in #haskell, you know there's an issue |