Logs: liberachat/#haskell
| 2025-12-01 20:46:37 | <EvanR> | visually a think of substitution as some term coming in and overwriting the x |
| 2025-12-01 20:46:38 | <RMSBach> | I guess interpretation flies in the face of the intelligibility of the mark even when we escape natural language |
| 2025-12-01 20:47:11 | <ski> | but i'm sure someone would hold the other interpretation, just to confuse things |
| 2025-12-01 20:52:01 | × | ouilemur quits (~jgmerritt@user/ouilemur) (Quit: WeeChat 4.7.0) |
| 2025-12-01 20:53:20 | <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 20:53:33 | <merijn> | What does ghcup base it's recommend versions on? |
| 2025-12-01 20:53:35 | × | karenw quits (~karenw@user/karenw) (Ping timeout: 240 seconds) |
| 2025-12-01 20:54:26 | <mauke> | vibes? |
| 2025-12-01 20:55:01 | <ski> | [r] x = t if r(x) defined and t = r(x) |
| 2025-12-01 20:55:08 | <ski> | [r] x = x if r(x) undefined |
| 2025-12-01 20:55:17 | <ski> | [r] (t u) = ([r] t) ([r] u) |
| 2025-12-01 20:55:18 | <geekosaur> | mostly on widest compatibility/lack of bugs |
| 2025-12-01 20:55:19 | <ski> | ... |
| 2025-12-01 20:55:51 | <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 20:56:16 | <geekosaur> | ghcc was held back to 9.4 until 9.6.7 fixed a key bug |
| 2025-12-01 20:56:50 | <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 20:57:08 | <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 20:57:51 | <EvanR> | ski, I'm not understanding your definitions above. What's r(x) |
| 2025-12-01 20:59:08 | <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 20:59:37 | <geekosaur> | *ghc |
| 2025-12-01 21:00:18 | <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:01:25 | <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 21:02:10 | <tomsmeding> | [exa]: [x,y) is the standard one, it's [x,y[ that I was complaining about |
| 2025-12-01 21:04:17 | <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 21:05:02 | <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 21:06:17 | <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 21:06:44 | <ski> | fgarcia : how do you mean ? |
| 2025-12-01 21:08:34 | <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 21:08:57 | <tomsmeding> | possibly, yes |
| 2025-12-01 21:09:06 | <tomsmeding> | though here in the netherlands we do [x,y) too |
| 2025-12-01 21:09:39 | <ski> | (here it's `[x,y[') |
| 2025-12-01 21:09:54 | <tomsmeding> | "here" is sweden? |
| 2025-12-01 21:10:09 | <ski> | aye |
| 2025-12-01 21:10:28 | × | Googulator60 quits (~Googulato@2a01-036d-0106-4ad8-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-12-01 21:10:44 | → | Googulator60 joins (~Googulato@2a01-036d-0106-4ad8-d9ec-010d-f188-ffcb.pool6.digikabel.hu) |
| 2025-12-01 21:11:44 | <merijn> | hmmm |
| 2025-12-01 21:11:56 | <merijn> | cabal 3.16 seems to have a stupid bug >.> |
| 2025-12-01 21:11:59 | <merijn> | "[Info] . already exists. Backing up old version in ..save0" |
| 2025-12-01 21:12:03 | <merijn> | yeah...no shit |
| 2025-12-01 21:12:11 | <tomsmeding> | ski: Wikipedia claims that ]a,b[ was introduced by Bourbaki https://en.wikipedia.org/wiki/Interval_(mathematics)#Notations_for_intervals |
| 2025-12-01 21:12:23 | <ski> | ah, interesting |
| 2025-12-01 21:12:24 | <tomsmeding> | merijn: what are you trying to do |
| 2025-12-01 21:12:31 | <merijn> | tomsmeding: Just "cabal init" |
| 2025-12-01 21:12:34 | <tomsmeding> | lol |
| 2025-12-01 21:12:48 | <merijn> | tomsmeding: To set up my AoC repo |
| 2025-12-01 21:13:25 | <tomsmeding> | merijn: I do not get that if I run 'cabal init' in an empty dir |
| 2025-12-01 21:13:48 | <merijn> | tomsmeding: Do you have it set to interactive? |
| 2025-12-01 21:14:00 | <tomsmeding> | I had to press enter like a 100 times, so I presume yes |
| 2025-12-01 21:14:21 | <merijn> | My directory just has a bunch of other directories in it from previous years |
| 2025-12-01 21:14:42 | <tomsmeding> | but doesn't `cabal init` start a new package in the _current_ directory? |
| 2025-12-01 21:14:51 | <merijn> | It should, yes |
| 2025-12-01 21:15:09 | <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 21:15:46 | <tomsmeding> | merijn: if I `mkdir a` `mkdir b` `cabal init` then I still don't get your message |
| 2025-12-01 21:16:01 | <tomsmeding> | ski: long live ambiguous notation in mathematics |
| 2025-12-01 21:16:18 | <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 21:16:27 | <tomsmeding> | ah |
| 2025-12-01 21:16:28 | <merijn> | And that breaking in recent cabal |
| 2025-12-01 21:16:38 | <tomsmeding> | possibly, yes, I haven't changed those defaults |
| 2025-12-01 21:16:48 | <tomsmeding> | bug report time? |
| 2025-12-01 21:17:44 | <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 21:17:44 | <jreicher> | "type". Of course I don't get to say how people use a word though. |
| 2025-12-01 21:18:00 | <jreicher> | ...anything with types at runtime... |
| 2025-12-01 21:18:59 | <tomsmeding> | it seems the theme of today is "words mean different things to different people" |
| 2025-12-01 21:19:15 | <jreicher> | OMG. That never happens. |
| 2025-12-01 21:21:16 | <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 21:22:58 | <jreicher> | tomsmeding: [exa]: regarding Haskell syntax in vim, it's not using treesitter? Maybe it's only neovim... |
| 2025-12-01 21:23:12 | <merijn> | jreicher: treesitter is only neovim |
| 2025-12-01 21:23:37 | <jreicher> | Ah. I wonder why vim hasn't started supporting it. |
| 2025-12-01 21:23:54 | <merijn> | it's one of the main reasons I switched to neovim |
| 2025-12-01 21:23:54 | × | simplystuart quits (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-12-01 21:24:00 | <tomsmeding> | and also, even though neovim supports tree-sitter, it doesn't bundle a Haskell grammar by default, it seems |
| 2025-12-01 21:24:13 | <merijn> | That being said, the haskell treesitter grammar is kinda ugly as sin |
| 2025-12-01 21:24:16 | <jreicher> | Emacs doesn't either. I think the grammars are still moving targets. |
| 2025-12-01 21:24:21 | <merijn> | tomsmeding: It doesn't bundle any grammars at all by default |
| 2025-12-01 21:24:28 | <merijn> | You gotta "TSInstall haskell" |
| 2025-12-01 21:24:36 | <tomsmeding> | merijn: :help treesitter |
| 2025-12-01 21:24:49 | <tomsmeding> | "Nvim includes these parsers: C, Lua, Markdown, Vimscript, Vimdoc, Treesitter query files" |
| 2025-12-01 21:24:50 | <jreicher> | Building a grammar is quite easy though. |
| 2025-12-01 21:24:57 | <tomsmeding> | ever tried properly parsing haskell? |
| 2025-12-01 21:24:57 | → | simplystuart joins (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-12-01 21:25:06 | <merijn> | tomsmeding: Yes |
| 2025-12-01 21:25:24 | <tomsmeding> | (I was saying that to jreicher) |
| 2025-12-01 21:25:36 | <jreicher> | I just mean building the treesitter grammar. I didn't mean writing one. :) |
| 2025-12-01 21:25:40 | <tomsmeding> | right :) |
| 2025-12-01 21:26:02 | <tomsmeding> | it's not that building a haskell parser is impossible -- not at all. Properly dealing with the indentation-sensitive layout is just non-trivial |
| 2025-12-01 21:26:27 | <merijn> | tomsmeding: Sure |
| 2025-12-01 21:26:29 | <ski> | fgarcia : do you have an example of "use those terms in functions" ? |
| 2025-12-01 21:26:37 | <merijn> | tomsmeding: But humor me and open the haskell tree sitter grammar :) |
| 2025-12-01 21:26:58 | <tomsmeding> | merijn: any part in particular you want me to look at |
| 2025-12-01 21:27:00 | <ski> | (not quite getting the context) |
| 2025-12-01 21:27:10 | <merijn> | tomsmeding: It really doesn't matter :p |
| 2025-12-01 21:27:22 | <tomsmeding> | merijn: I looked before and couldn't quite make heads or tails of what I was seeing (mind I haven't looked at TS grammars before) |
| 2025-12-01 21:27:34 | <merijn> | tomsmeding: That's not because it's TS grammar |
| 2025-12-01 21:27:56 | <jreicher> | https://github.com/tree-sitter/tree-sitter-haskell/blob/master/src/grammar.json |
| 2025-12-01 21:27:58 | <merijn> | tomsmeding: I'm writing my own for sqlite, the haskell one is just convoluted and ununderstandable |
| 2025-12-01 21:27:58 | <jreicher> | You mean that, right? |
| 2025-12-01 21:28:20 | <tomsmeding> | surely merijn means the source, not the compiled result https://github.com/tree-sitter/tree-sitter-haskell/tree/master/grammar |
| 2025-12-01 21:28:27 | <jreicher> | Which is the json |
| 2025-12-01 21:28:30 | <jreicher> | The C is generated |
| 2025-12-01 21:28:36 | <merijn> | jreicher: The json isn't the grammar |
All times are in UTC.