Logs: liberachat/#haskell
| 2026-02-07 09:35:15 | → | trickard_ joins (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-07 09:40:22 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 09:43:19 | → | Enrico63 joins (~Enrico63@host-79-27-153-69.retail.telecomitalia.it) |
| 2026-02-07 09:45:03 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2026-02-07 09:56:00 | <gentauro> | I'm wondering how this (very Lisp'y) https://en.wikipedia.org/wiki/Z3_Theorem_Prover#Examples become like this https://github.com/IagoAbal/haskell-z3?tab=readme-ov-file#example |
| 2026-02-07 09:56:09 | × | trickard_ quits (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-07 09:56:10 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 09:56:21 | → | trickard_ joins (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-07 09:57:40 | <jreicher> | What do you mean? Lisp is not great for stuff like this. |
| 2026-02-07 10:01:57 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-02-07 10:02:33 | <probie> | gentauro: There's very little lispy-ness in the SMTLIB2 format. It might as well be JSON, YAML or something entirely bespoke |
| 2026-02-07 10:03:12 | <probie> | They just chose S-expressions, because "everyone" in AI at the time was familiar with them |
| 2026-02-07 10:03:52 | <probie> | The Z3 monad is really just a codegen monad |
| 2026-02-07 10:04:53 | <jreicher> | Yes I think that's probably my point too. sexpr != lisp despite what everyone thinks |
| 2026-02-07 10:05:58 | <jreicher> | I think the defining characteristic of Lisp is "no code, everything is data" which is why it gets confused with the presentation of sexprs |
| 2026-02-07 10:07:33 | <jreicher> | Codegen helps muddy the waters even further. |
| 2026-02-07 10:09:04 | trickard_ | is now known as trickard |
| 2026-02-07 10:12:47 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 10:12:58 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 246 seconds) |
| 2026-02-07 10:16:42 | <gentauro> | `mkFreshIntVar` <- Hungarian notation for the win? Nah |
| 2026-02-07 10:17:59 | gentauro | feels like: `AbstractAnimalThatLivesInWaterAndHasGillsAndFins.class` |
| 2026-02-07 10:18:01 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-07 10:19:55 | → | AlexNoo_ joins (~AlexNoo@85.174.182.86) |
| 2026-02-07 10:20:41 | → | AlexNoo__ joins (~AlexNoo@85.174.182.86) |
| 2026-02-07 10:21:55 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-02-07 10:22:46 | <probie> | gentauro: What's wrong with it? |
| 2026-02-07 10:22:50 | × | AlexZenon quits (~alzenon@85.174.181.199) (Ping timeout: 245 seconds) |
| 2026-02-07 10:23:22 | <probie> | `Fresh` promises no name collisions, `Int` tells you the type, and `Var` tells you that it's a variable |
| 2026-02-07 10:23:28 | × | AlexNoo quits (~AlexNoo@85.174.181.199) (Ping timeout: 246 seconds) |
| 2026-02-07 10:23:38 | × | Alex_delenda_est quits (~al_test@85.174.181.199) (Ping timeout: 256 seconds) |
| 2026-02-07 10:24:19 | × | AlexNoo_ quits (~AlexNoo@85.174.182.86) (Ping timeout: 260 seconds) |
| 2026-02-07 10:24:42 | → | AlexNoo joins (~AlexNoo@85.174.182.86) |
| 2026-02-07 10:25:03 | <gentauro> | probie: to verbose (at least for me) |
| 2026-02-07 10:25:06 | <jreicher> | gentauro: "Hungarian notation"? |
| 2026-02-07 10:25:20 | <jreicher> | Oh, I think I know what you mean |
| 2026-02-07 10:25:29 | × | AlexNoo__ quits (~AlexNoo@85.174.182.86) (Ping timeout: 260 seconds) |
| 2026-02-07 10:26:27 | <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 10:27:06 | <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 10:28:16 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 2026-02-07 10:28:34 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 10:30:21 | × | p3n quits (~p3n@217.198.124.246) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-02-07 10:30:48 | × | Enrico63 quits (~Enrico63@host-79-27-153-69.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-02-07 10:31:17 | <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 10:31:40 | → | p3n joins (~p3n@217.198.124.246) |
| 2026-02-07 10:33:03 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 260 seconds) |
| 2026-02-07 10:33:57 | → | AlexZenon joins (~alzenon@85.174.182.86) |
| 2026-02-07 10:35:05 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-07 10:37:00 | <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 10:37:24 | × | trickard quits (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-07 10:37:35 | <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 10:37:37 | → | trickard_ joins (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-07 10:37:45 | <int-e> | (managing your own names is probably suboptimal) |
| 2026-02-07 10:37:54 | <gentauro> | very succint |
| 2026-02-07 10:38:07 | × | AlexZenon quits (~alzenon@85.174.182.86) (Ping timeout: 240 seconds) |
| 2026-02-07 10:38:50 | gentauro | I want to remove the string variables and just rely on the languages value binding |
| 2026-02-07 10:40:09 | <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 10:40:14 | gentauro | less is more |
| 2026-02-07 10:41:22 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 10:42:00 | × | qqq quits (~qqq@185.54.22.56) (Quit: Lost terminal) |
| 2026-02-07 10:42:27 | <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 10:42:51 | → | AlexZenon joins (~alzenon@85.174.182.86) |
| 2026-02-07 10:45:22 | <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 10:46:10 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-02-07 10:46:35 | <int-e> | Oh also I think terms are first-order, so there are no binders that could capture variables. |
| 2026-02-07 10:48:33 | <int-e> | jreicher: So basically, it's a different flavor of name clashes than variable capture. |
| 2026-02-07 10:57:07 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 10:58:24 | <ski> | i suppose sometimes you'd like to generate fresh variables (perhaps in a loop, or in a recursive computation) .. |
| 2026-02-07 10:58:53 | <ski> | .. presumable that F# binding can do that, as well ? |
| 2026-02-07 11:02:10 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 11:03:07 | <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 11:03:13 | <ski> | provides) |
| 2026-02-07 11:04:22 | <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 11:09:26 | 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 11:12:56 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 11:13:30 | <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 11:16:07 | <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 11:17:32 | <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 11:17:43 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-07 11:19:19 | <ski> | in the case of the functional programming (Delphin), they choose to instead allow you to add patterns for "parameters" of (LF) types, in your `case'-`of' expressions (and then you'd often also pass some kind of accumulating substitution function, or similar, to the traversal function, initializing it to the empty function at the top call) |
| 2026-02-07 11:19:36 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-02-07 11:22:25 | × | _JusSx_ quits (~jussx@78.210.148.66) (Ping timeout: 245 seconds) |
| 2026-02-07 11:23:24 | <ski> | (ooc, they also had effectively a monad, in the language, for computations which will result in a value term of an LF type. the type `<T>' is short for `T * unit', which is short for `exists _ : T. unit'. in `T * U', `U' is not allowed to be an LF type, but `T' is. the reason is that they want all expressions of LF type to not have any computational (Delphin-level) subexpressions, only an LF-term, with some |
| 2026-02-07 11:23:30 | <ski> | schematic variables to fill in with other LF terms) |
| 2026-02-07 11:24:11 | → | _JusSx_ joins (~jussx@78.211.193.248) |
| 2026-02-07 11:28:43 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 11:32:37 | <ski> | one of the interesting things you can do in Twelf, is to encode a proof as a relation. to actually check that the proof is valid, you then need to check that for each possible input for some designated input parameters to the relation/predicate, there is a related output asssigned to the output parameter(s), such that the (dependently typed) relation holds. from a logic programming standpoint, this is a |
| 2026-02-07 11:32:43 | <ski> | mode&determinism declaration on the predicate (if you will, ensuring that the relation is functional) |
| 2026-02-07 11:33:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-07 11:34:27 | <ski> | so, the system has facilities to do this (meta-proof) checking of modes, in order to ensure that the predicate whose definition encodes your proof actually proves the intended thing (e.g. that if an (object-language) term has some type, and you reduce the term one step, then it still has that type) |
| 2026-02-07 11:35:26 | <ski> | it also has facilities to be able to state such theorems, and let a theorem-prover (in the language implementation) search for a proof (and realize it as a recursive predicate) |
| 2026-02-07 11:42:22 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-07 11:44:18 | × | jreicher quits (~joelr@user/jreicher) (Quit: In transit) |
| 2026-02-07 11:46:32 | × | Beowulf quits (florian@2a01:4f9:3b:2d56::2) (Quit: = "") |
| 2026-02-07 11:47:06 | <ski> | one of the reasons they stated for developing Delphin (rather than Twelf), was a claim of having trouble with some kinda of higher-order programming. afaict, what they mean by this is not lack of support for higher-order predicates, per se, but rather lack of adequate support for the static mode&determinism *checking* (which is optional (from a computational standpoint), but essential for when you want to do |
| 2026-02-07 11:47:13 | <ski> | said above (meta-)proof checking) |
| 2026-02-07 11:47:30 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 11:49:25 | <ski> | the issue being limitations in reasoning about local parameters (data constructors), and local assumptions, for the mode-checking. and, perhaps, also some limitations in doing (effectively) anonymous predicates, e.g. extending an accumulator predicate parameter -- and associated reasoning about mode for such higher-order predicates |
| 2026-02-07 11:50:36 | → | Beowulf joins (florian@2a01:4f9:3b:2d56::2) |
| 2026-02-07 11:50:53 | <ski> | .. i can't keep from feeling like there ought to be a way to address those concerns more directly .. rather than resorting to going to a different (functional) computational model. Twelf is the only dependently typed logic programming language i'm aware of, and it would seem to be a shame to not further develop that |
| 2026-02-07 11:53:45 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
All times are in UTC.