Newest at the top
| 2026-02-07 12:17:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-07 12:17:32 +0100 | <ski> | in the case of logic programming (Twelf), you'll be dynamically (similar to dynamic scope, being the operational interpretation of implicational logic programming goals here) adding clauses to your recursive traversal predicates, as you step under the binders |
| 2026-02-07 12:16:07 +0100 | <ski> | so, `x',`f',`f',`x' (four different variables, the language automatically ensures no clashes, capture-free substitution) here will, in the local contexts, act as new temporary data constructors for the expression data type (with `app' and `lam' as the *only* global data constructors, in this example of pure lambda calculus) |
| 2026-02-07 12:13:30 +0100 | <ski> | if you match on and do recursion on an LF term like `app (lam x\ lam f\ f x) (lam f\ lam x\ f x x)' (representing `(\x. \f. f x) (\f. \x. f x x)', where `app : expr (A -> B) -> (expr A -> expr B)' and `lam : (expr A -> expr B) -> expr (A -> B)'), you'll need to step inside the binders, traversing open terms |
| 2026-02-07 12:12:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:09:26 +0100 | ski | was reading, recently, about a (rather restricted, in various ways) dependently typed functional language (Delphin, meant as a different approach to the logic programming approach Twelf to LF terms) for doing computation over LF (Logical Framework) terms, typically used to represent HOAS (that you can *pattern-match* on !) |
| 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 +0100 | merijn | (~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 +0100 | merijn | (~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 +0100 | merijn | (~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 +0100 | AlexZenon | (~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 +0100 | qqq | (~qqq@185.54.22.56) (Quit: Lost terminal) |
| 2026-02-07 11:41:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 11:40:14 +0100 | gentauro | less 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 +0100 | gentauro | I want to remove the string variables and just rely on the languages value binding |
| 2026-02-07 11:38:07 +0100 | AlexZenon | (~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 +0100 | trickard_ | (~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 +0100 | trickard | (~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 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-07 11:33:57 +0100 | AlexZenon | (~alzenon@85.174.182.86) |
| 2026-02-07 11:33:03 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 260 seconds) |
| 2026-02-07 11:31:40 +0100 | p3n | (~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 +0100 | Enrico63 | (~Enrico63@host-79-27-153-69.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-02-07 11:30:21 +0100 | p3n | (~p3n@217.198.124.246) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-02-07 11:28:34 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 11:28:16 +0100 | chromoblob | (~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 +0100 | AlexNoo__ | (~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 +0100 | AlexNoo | (~AlexNoo@85.174.182.86) |
| 2026-02-07 11:24:19 +0100 | AlexNoo_ | (~AlexNoo@85.174.182.86) (Ping timeout: 260 seconds) |
| 2026-02-07 11:23:38 +0100 | Alex_delenda_est | (~al_test@85.174.181.199) (Ping timeout: 256 seconds) |
| 2026-02-07 11:23:28 +0100 | AlexNoo | (~AlexNoo@85.174.181.199) (Ping timeout: 246 seconds) |