IRCBrowse

2026/02/07

Newest at the top

2026-02-07 12:04:22 +0100 <ski> (.. in some cases, one might be able to get away with generating something like `\[a,b,c,...,z] -> ...' for an indefinite number of elements in the list pattern, but still keep the simple static types)
2026-02-07 12:03:13 +0100 <ski> provides)
2026-02-07 12:03:07 +0100 <ski> (depending on what one'd want to do ?) i think one could possibly do that kind of thing, in MetaML or MetaOCaml, with their quasiquoted code expressions. one'd need to introduce local (quoted) binders for them, though. and, i guess, might need to either resort to dynamically typed code expressions (which at least MetaML provides, i forget about MetaOcaml), or else to dependent typing (which neither of them
2026-02-07 12:02:10 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2026-02-07 11:58:53 +0100 <ski> .. presumable that F# binding can do that, as well ?
2026-02-07 11:58:24 +0100 <ski> i suppose sometimes you'd like to generate fresh variables (perhaps in a loop, or in a recursive computation) ..
2026-02-07 11:57:07 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-02-07 11:48:33 +0100 <int-e> jreicher: So basically, it's a different flavor of name clashes than variable capture.
2026-02-07 11:46:35 +0100 <int-e> Oh also I think terms are first-order, so there are no binders that could capture variables.
2026-02-07 11:46:10 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-02-07 11:45:22 +0100 <int-e> No, there's no substitution taking place. There's a global namespace. But users may want to generate auxiliary variables without clashing with other auxiliary variables, so as a convenience, fresh name generation is provided by the SMT solver. (At no real cost; the SMT solver will need that functionality internally anyway.)
2026-02-07 11:42:51 +0100AlexZenon(~alzenon@85.174.182.86)
2026-02-07 11:42:27 +0100 <jreicher> int-e: I'm not familiar with Z3, but is the generation of fresh names a crappy implementation of capture-avoiding substitution?
2026-02-07 11:42:00 +0100qqq(~qqq@185.54.22.56) (Quit: Lost terminal)
2026-02-07 11:41:22 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-02-07 11:40:14 +0100gentauroless is more
2026-02-07 11:40:09 +0100 <gentauro> but I guess if we can do something like that in OCaml for .NET, we should probably be able to mimic that in Haskell right?
2026-02-07 11:38:50 +0100gentauroI want to remove the string variables and just rely on the languages value binding
2026-02-07 11:38:07 +0100AlexZenon(~alzenon@85.174.182.86) (Ping timeout: 240 seconds)
2026-02-07 11:37:54 +0100 <gentauro> very succint
2026-02-07 11:37:45 +0100 <int-e> (managing your own names is probably suboptimal)
2026-02-07 11:37:37 +0100trickard_(~trickard@cpe-61-98-47-163.wireline.com.au)
2026-02-07 11:37:35 +0100 <gentauro> probie: I tried to use Code Quotations and Computation Expressions in F# and I end up with this -> https://paste.tomsmeding.com/bi5MGjco
2026-02-07 11:37:24 +0100trickard(~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2026-02-07 11:37:00 +0100 <int-e> probie: Well, in the Z3 API, generating fresh names is tied to function declarations, https://z3prover.github.io/api/html/group__capi.html#ga76d673b3b3f53c1044fd59621b1b8b68 (nice anchor I'm sure it's very stable)
2026-02-07 11:35:05 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-02-07 11:33:57 +0100AlexZenon(~alzenon@85.174.182.86)
2026-02-07 11:33:03 +0100chromoblob(~chromoblo@user/chromob1ot1c) (Ping timeout: 260 seconds)
2026-02-07 11:31:40 +0100p3n(~p3n@217.198.124.246) p3n
2026-02-07 11:31:17 +0100 <probie> I mean you certainly could do something like `do { name <- freshName "q1"; mkVar intType name }`, but I don't think you really gain much
2026-02-07 11:30:48 +0100Enrico63(~Enrico63@host-79-27-153-69.retail.telecomitalia.it) (Quit: Client closed)
2026-02-07 11:30:21 +0100p3n(~p3n@217.198.124.246) (Quit: ZNC 1.10.1 - https://znc.in)
2026-02-07 11:28:34 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-02-07 11:28:16 +0100chromoblob(~chromoblo@user/chromob1ot1c) chromoblob\0
2026-02-07 11:27:06 +0100 <probie> I guess you could have have a `make` function which takes various kinds of records as arguments, but in practice that's not ergonomic, and it also deviates heavily from the C API, which is why most of the documentation you'll find online is
2026-02-07 11:26:27 +0100 <probie> gentauro: how would you shrink it, short of abbreviating things. You need to convey 4 things; "it's new", "the name can't be anything already generated", "it's an int" and "it's a var"?
2026-02-07 11:25:29 +0100AlexNoo__(~AlexNoo@85.174.182.86) (Ping timeout: 260 seconds)
2026-02-07 11:25:20 +0100 <jreicher> Oh, I think I know what you mean
2026-02-07 11:25:06 +0100 <jreicher> gentauro: "Hungarian notation"?
2026-02-07 11:25:03 +0100 <gentauro> probie: to verbose (at least for me)
2026-02-07 11:24:42 +0100AlexNoo(~AlexNoo@85.174.182.86)
2026-02-07 11:24:19 +0100AlexNoo_(~AlexNoo@85.174.182.86) (Ping timeout: 260 seconds)
2026-02-07 11:23:38 +0100Alex_delenda_est(~al_test@85.174.181.199) (Ping timeout: 256 seconds)
2026-02-07 11:23:28 +0100AlexNoo(~AlexNoo@85.174.181.199) (Ping timeout: 246 seconds)
2026-02-07 11:23:22 +0100 <probie> `Fresh` promises no name collisions, `Int` tells you the type, and `Var` tells you that it's a variable
2026-02-07 11:22:50 +0100AlexZenon(~alzenon@85.174.181.199) (Ping timeout: 245 seconds)
2026-02-07 11:22:46 +0100 <probie> gentauro: What's wrong with it?
2026-02-07 11:21:55 +0100peterbecich(~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds)
2026-02-07 11:20:41 +0100AlexNoo__(~AlexNoo@85.174.182.86)
2026-02-07 11:19:55 +0100AlexNoo_(~AlexNoo@85.174.182.86)