Newest at the top
| 2025-12-01 22:21:16 +0100 | <fgarcia> | ski: i am not much of a proof writer. but in english, variables of interest could be written as two different symbols. while some people will not like it, the substition can be written "For the above functions, replace variable x with y. This would include f(x) being replaced with f(y)." |
| 2025-12-01 22:19:15 +0100 | <jreicher> | OMG. That never happens. |
| 2025-12-01 22:18:59 +0100 | <tomsmeding> | it seems the theme of today is "words mean different things to different people" |
| 2025-12-01 22:18:00 +0100 | <jreicher> | ...anything with types at runtime... |
| 2025-12-01 22:17:44 +0100 | <jreicher> | "type". Of course I don't get to say how people use a word though. |
| 2025-12-01 22:17:44 +0100 | <jreicher> | lortabac: yeah I was always meaning what dminuoso ended up saying, but I was making a bit of a joke. When people talk about doing anything with types they really mean runtime tag checking, i.e. some kind of metadata-based control. And this is probably why you say it provides a meaning to raw bytes. You can smuggle some kind of pseudo-semantics into any kind of generic metadata. The joke I'm making is that this shouldn't be called a |
| 2025-12-01 22:16:48 +0100 | <tomsmeding> | bug report time? |
| 2025-12-01 22:16:38 +0100 | <tomsmeding> | possibly, yes, I haven't changed those defaults |
| 2025-12-01 22:16:28 +0100 | <merijn> | And that breaking in recent cabal |
| 2025-12-01 22:16:27 +0100 | <tomsmeding> | ah |
| 2025-12-01 22:16:18 +0100 | <merijn> | tomsmeding: I think it's because my cabal.config has "application-dir: ." (i.e. source should be in root of the directory, not a subdir) |
| 2025-12-01 22:16:01 +0100 | <tomsmeding> | ski: long live ambiguous notation in mathematics |
| 2025-12-01 22:15:46 +0100 | <tomsmeding> | merijn: if I `mkdir a` `mkdir b` `cabal init` then I still don't get your message |
| 2025-12-01 22:15:09 +0100 | <ski> | "Some authors such as Yves Tillé use ]a, b[ to denote the complement of the interval (a, b); namely, the set of all real numbers that are either less than or equal to a, or greater than or equal to b." |
| 2025-12-01 22:14:51 +0100 | <merijn> | It should, yes |
| 2025-12-01 22:14:42 +0100 | <tomsmeding> | but doesn't `cabal init` start a new package in the _current_ directory? |
| 2025-12-01 22:14:21 +0100 | <merijn> | My directory just has a bunch of other directories in it from previous years |
| 2025-12-01 22:14:00 +0100 | <tomsmeding> | I had to press enter like a 100 times, so I presume yes |
| 2025-12-01 22:13:48 +0100 | <merijn> | tomsmeding: Do you have it set to interactive? |
| 2025-12-01 22:13:25 +0100 | <tomsmeding> | merijn: I do not get that if I run 'cabal init' in an empty dir |
| 2025-12-01 22:12:48 +0100 | <merijn> | tomsmeding: To set up my AoC repo |
| 2025-12-01 22:12:34 +0100 | <tomsmeding> | lol |
| 2025-12-01 22:12:31 +0100 | <merijn> | tomsmeding: Just "cabal init" |
| 2025-12-01 22:12:24 +0100 | <tomsmeding> | merijn: what are you trying to do |
| 2025-12-01 22:12:23 +0100 | <ski> | ah, interesting |
| 2025-12-01 22:12:11 +0100 | <tomsmeding> | ski: Wikipedia claims that ]a,b[ was introduced by Bourbaki https://en.wikipedia.org/wiki/Interval_(mathematics)#Notations_for_intervals |
| 2025-12-01 22:12:03 +0100 | <merijn> | yeah...no shit |
| 2025-12-01 22:11:59 +0100 | <merijn> | "[Info] . already exists. Backing up old version in ..save0" |
| 2025-12-01 22:11:56 +0100 | <merijn> | cabal 3.16 seems to have a stupid bug >.> |
| 2025-12-01 22:11:44 +0100 | <merijn> | hmmm |
| 2025-12-01 22:10:44 +0100 | Googulator60 | (~Googulato@2a01-036d-0106-4ad8-d9ec-010d-f188-ffcb.pool6.digikabel.hu) |
| 2025-12-01 22:10:28 +0100 | Googulator60 | (~Googulato@2a01-036d-0106-4ad8-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-12-01 22:10:09 +0100 | <ski> | aye |
| 2025-12-01 22:09:54 +0100 | <tomsmeding> | "here" is sweden? |
| 2025-12-01 22:09:39 +0100 | <ski> | (here it's `[x,y[') |
| 2025-12-01 22:09:06 +0100 | <tomsmeding> | though here in the netherlands we do [x,y) too |
| 2025-12-01 22:08:57 +0100 | <tomsmeding> | possibly, yes |
| 2025-12-01 22:08:34 +0100 | <ski> | tomsmeding : i believe `[x,y)' is in english-influenced, and `[x,y[' in german-influenced. not sure about french nor russian |
| 2025-12-01 22:06:44 +0100 | <ski> | fgarcia : how do you mean ? |
| 2025-12-01 22:06:17 +0100 | <ski> | (of course, for Haskell, the "if ... undefined" would have to be modelled by `Maybe', or (making all substitutions total) by constructing the `y |-> x' substitution by overriding from the identity substitution) |
| 2025-12-01 22:05:02 +0100 | <tomsmeding> | merijn: the opinion of maerwald, which is iirc based on various things including known bugs and HLS support; I recall him saying at some point that he was refusing to move the 'recommended' flag to push GHC developers to fix some installation issue on FreeBSD (iirc) |
| 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 |