Logs: liberachat/#haskell
| 2025-09-07 02:13:23 | <monochrom> | Yeah. |
| 2025-09-07 02:13:26 | <ski> | oh .. and i also use similar naming, for versions of a predicate, or function, specialized to a particular constructor. e.g. `orderedCons' specified by `orderedCons x xs = ordered (x : xs)' (and also having `ordered [] = True'), implemented by `orderedCons _ [] = True; orderedCons x0 (x1 : xs) = x0 <= x1 && orderedCons x1 xs' |
| 2025-09-07 02:13:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 02:14:01 | <ski> | yea .. cuts are rather bad |
| 2025-09-07 02:15:20 | <ski> | and i do use `loop'/`go', or similar, for a local helper or loop, often. but if there's an obvious reasonable name along the lines above, i tend to go with that, possiblly also exporting the operation |
| 2025-09-07 02:16:18 | <ski> | Mercury is nicer than Prolog, in that it has no cuts. also has automatic conjunct reordering, so it can be easier to use multiple modes of a predicate (or function) |
| 2025-09-07 02:17:13 | × | notzmv quits (~umar@user/notzmv) (Remote host closed the connection) |
| 2025-09-07 02:17:52 | <ski> | there are two main reasons for why cut is bad. (a) that it is inherently illogical, non-declarative (and also very easy to accidentally make your predicate "non-steeadfast" (not monotone, in terms of information about the parameters), if you're not careful) |
| 2025-09-07 02:18:01 | <monochrom> | I know how to teach delimited continuation. That is, with an explicit delimiter like "reset" that the programmer is allowed to place anywhere. I would agree to teach cut if it had the same explicit place-anywhere-you-see-fit delimiter rather than "the delimiter is the owning predicate, therefore you must always define a helper predicate". |
| 2025-09-07 02:18:30 | <monochrom> | s/define/contrive/ |
| 2025-09-07 02:18:55 | <monochrom> | Now also cross that with no local definitions. |
| 2025-09-07 02:19:29 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 250 seconds) |
| 2025-09-07 02:19:52 | <ski> | but also (b), that it implicitly refers to the "current clause", just as `return' refers to the current function, and `break',`continue' refers to the current (innermost enclosing) loop (or `switch', for the former), in C. this means that you can't naively factor out (or the reverse) a piece of code (taking care to parameterize on the variables that cross the boundary of the factored-out code) |
| 2025-09-07 02:21:33 | <ski> | you could have (a) without (b). using the conditional, `( Condition -> Consequent ; Alternate )', in Prolog amounts to (a) without (b). many Prologs also have a version of this that does not cut away all but the first solution of `Condition', which behaves better, logically/declaratively. this latter is also what Mercury does |
| 2025-09-07 02:22:14 | <ski> | "would agree to teach cut if it had the same explicit place-anywhere-you-see-fit delimiter" -- exactly |
| 2025-09-07 02:22:27 | <ski> | (a) is "just" a kind of side-effect |
| 2025-09-07 02:22:52 | <ski> | (b) is "syntactic dynamic scope" |
| 2025-09-07 02:23:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-09-07 02:23:54 | <ski> | i really would like a logic programming language, with a convenient and reasonable way to have local definitions |
| 2025-09-07 02:25:06 | <ski> | you can make them, in lambdaProlog (and Twelf) .. but would like some syntactic sugar, and implicit quantification, on top of the basic semantic feature |
| 2025-09-07 02:26:23 | <monochrom> | I have started teaching Curry for the logic programming part of my course. (The FP part is Haskell. This means confusingly I teach one syntax with two different semantics haha.) And I think Verse is even better (semantics is well-balanced between theory and pragmatism). |
| 2025-09-07 02:26:37 | <ski> | traditionally, a logic program is seen as a sequence of clauses, each terminated by a full stop. ideally, the syntax for terminating/separating top-level clauses from each otheer should be the same as for local clauses |
| 2025-09-07 02:27:17 | <ski> | yea, Curry (and Escher) uses a Haskell-like syntax. but they also use `=' rather than implication |
| 2025-09-07 02:27:33 | <ski> | i dunno Verge |
| 2025-09-07 02:30:12 | <ski> | btw, you can reason about, introduce, (b), in Lisp macro system. specifically, in some Scheme systems, you can have it as an opt-in feature. Racket has "syntax parameters", which are "parameters" (dynamic scope), but on the level of "syntax" (macros) |
| 2025-09-07 02:31:23 | <monochrom> | Verse is Tim Sweeney's language. Eventually it will have all paradigms. SPJ joined Epic and published a paper on the functional logic part. |
| 2025-09-07 02:31:52 | <ski> | oh. it's supposed to be usable for parts of game engine stuff ? |
| 2025-09-07 02:33:24 | <monochrom> | It is Fortnight's script language or something like that. |
| 2025-09-07 02:33:45 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 02:33:59 | <monochrom> | Err, or Unreal Engine, yeah. |
| 2025-09-07 02:38:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-09-07 02:40:16 | <monochrom> | This: https://simon.peytonjones.org/verse-calculus/ |
| 2025-09-07 02:47:55 | <ski> | in lambdaProlog, you can write |
| 2025-09-07 02:48:18 | <ski> | reverse Xs0 RevXs0 :- |
| 2025-09-07 02:48:32 | <ski> | pi loop \ |
| 2025-09-07 02:48:54 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 256 seconds) |
| 2025-09-07 02:49:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 02:49:18 | <ski> | ( loop nil RevXs0 |
| 2025-09-07 02:49:52 | <ski> | => ( pi X \ pi Xs \ pi Acc \ |
| 2025-09-07 02:50:07 | <ski> | ( loop (X :: Xs) Acc :- |
| 2025-09-07 02:50:13 | <ski> | loop Xs (X :: Acc) |
| 2025-09-07 02:50:21 | <ski> | ) |
| 2025-09-07 02:50:31 | <ski> | ) |
| 2025-09-07 02:50:39 | <ski> | => loop Xs0 nil |
| 2025-09-07 02:50:41 | <ski> | ). |
| 2025-09-07 02:51:52 | <ski> | here `loop' is a local predicate (also notice how the first clause of `loop' non-locally will instantiate the parameter `RevXs0' of `reverse', when reaching the base case, end of list, so that we don't need to pass up the final result of the accumulator up the recursion chain) |
| 2025-09-07 02:53:16 | <ski> | but, it's annoying to have to explicitly quantify the parameters of the local clauses (not including `RevXs0'), and also to have to locally quantifier `loop'. and syntactically, it's annoying that the local clauses are not terminated with a `.', like the top-level one is |
| 2025-09-07 02:54:30 | <ski> | (oh, and yes, `pi' is universal quantification. its type is `(A -> o) -> o'. `o' is the type of propositions. `loop \ ..loop..', as well as `X \ ..X..', &c. are lambda terms) |
| 2025-09-07 02:55:41 | <ski> | right, Unreal Engine |
| 2025-09-07 02:55:53 | <ski> | ty for the Verse link |
| 2025-09-07 02:56:15 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-09-07 02:57:56 | <ski> | (Twelf is rather similar to lambdaProlog, apart from being dependently typed, and having a bunch of more features and static checking, related to theorem proving, termination checking, a rudimentary mode and determinism system, &c.) |
| 2025-09-07 02:59:04 | × | srandomizer quits (~user@185.159.157.137) (Remote host closed the connection) |
| 2025-09-07 02:59:34 | <ski> | "a new core calculus for deterministic functional logic programming" -- i wonder how this compares to Oz |
| 2025-09-07 02:59:52 | → | srandomizer joins (~user@185.159.157.137) |
| 2025-09-07 03:01:29 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-09-07 03:02:52 | <ski> | btw, with `=>' (implication), you can do a kind of "dynamic scope", namely of predicate clauses. the goal `( <clause> => <goal> )' temporarily assumes (adds/asserts) `<clause>', for the duration of the solving / execution / solution-search of `<goal>'. when (if) that succeeds, the clause is removed. if we backtrack back inside, it is added again. if we fail back to before, it is removed |
| 2025-09-07 03:03:09 | × | mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.9.1+deb2+b3 - https://znc.in) |
| 2025-09-07 03:04:05 | → | arandombit joins (~arandombi@user/arandombit) |
| 2025-09-07 03:06:03 | → | mhatta joins (~mhatta@www21123ui.sakura.ne.jp) |
| 2025-09-07 03:06:03 | <ski> | one can see the presence of goal implications (and also goal universal quantifications) as a kind of "completeness" of features, for effectively being able to reason about and manipulate lambda terms (as data, e.g. for HOAS). however, even without lambda terms, goal implication & universals can be quite handy and nice. iirc there's some "completeness" result that the Hereditary Harrop formulae, which is the |
| 2025-09-07 03:06:09 | <ski> | analogue of Horn clauses for lambdaProlog (and Twelf), which inclused these two kinds of goals, is the largest class of formulae that can serve as an "abstract logic programming language", for intuitionistic logic |
| 2025-09-07 03:06:56 | <ski> | being "abstract logic programming language" amounts to two properties, (a) goal-directedness; and (b) clause-focusing |
| 2025-09-07 03:07:09 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 03:08:47 | <ski> | goal-directedness means that every proof in the given system fragment, if the conclusion formula in the sequent is not atomic (so uses some connective), can be rewritten to an equivalent proof whose last inference rule is a right (introduction) rule for that connective |
| 2025-09-07 03:10:27 | <ski> | clause-focusing means that every proof where the conclusion is atom, can be rewritten in such a way that we successively apply left (introduction) rules (from the root of the proof tree up) to a single chosen / focused clause, until we end up with an atomic clause (which them must unify with the atomic conclusion of the sequent) |
| 2025-09-07 03:11:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-09-07 03:11:54 | <ski> | these two properties means that we can cut away most of the non-determnism in the selection of which inference rules to apply. so that we can read a non-atomic goal as search instructions for how to execute the goal, not needing to consult any clause as long as the goal is non-atomic |
| 2025-09-07 03:13:32 | <ski> | the latter property meaning that once the goal is atomic, it suffices to (non-deterministically) choose one clause to focus on, and then to continue reducing that (generating goals as extra side-conditions along the way), until we can determine that the clause matches the atomic goal (and we can execute the side-condition goals, the bodies of the clause) |
| 2025-09-07 03:14:27 | <ski> | so, the latter means that we can treat predicate call goals as procedure invocations, and treat clauses as (partial) implementations of these |
| 2025-09-07 03:16:04 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 2025-09-07 03:16:13 | <ski> | the remaining non-determinism, in the system, is in the choice of clause to focus on (and in the choice of which conjunct of a clause to focus on, e.g. in `( foo & bar ) :- baz.'), and in the choice of which disjunct in a disjunction goal to attempt to prove |
| 2025-09-07 03:16:35 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-09-07 03:17:24 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2025-09-07 03:18:52 | <ski> | technically, there's also non-determinism in the choice of which term to instantiate logic variables (as in existential goals, and universal clauses) to. but this can be dealt with, in the usual lazy fashion, delaying these choices until we need some equality to hold, by using unification (rather than backtracking or perhaps some other means to implement non-determinism, like some breadth-first or parallel |
| 2025-09-07 03:18:58 | <ski> | exploration) |
| 2025-09-07 03:19:53 | × | srandomizer quits (~user@185.159.157.137) (Quit: Leaving) |
| 2025-09-07 03:20:49 | → | aforemny_ joins (~aforemny@2001:9e8:6cc9:300:3eaa:97ed:8ab3:fe4d) |
| 2025-09-07 03:21:53 | × | aforemny quits (~aforemny@2001:9e8:6cec:2f00:9ea2:47fd:5959:6451) (Ping timeout: 250 seconds) |
| 2025-09-07 03:22:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 03:27:26 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-09-07 03:31:30 | → | srandomizer joins (~user@185.159.157.137) |
| 2025-09-07 03:37:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 03:42:15 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2025-09-07 03:43:59 | × | srandomizer quits (~user@185.159.157.137) (Ping timeout: 250 seconds) |
| 2025-09-07 03:49:39 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 2025-09-07 03:49:59 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-09-07 03:53:17 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 03:54:02 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 2025-09-07 03:58:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-09-07 04:08:11 | × | trickard quits (~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-09-07 04:08:24 | → | trickard_ joins (~trickard@cpe-53-98-47-163.wireline.com.au) |
| 2025-09-07 04:08:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 04:10:26 | → | peterbecich joins (~Thunderbi@syn-172-222-149-049.res.spectrum.com) |
| 2025-09-07 04:13:05 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-09-07 04:15:21 | × | pierrot quits (~pi@user/pierrot) (Quit: ZNC 1.8.2 - http://znc.in) |
| 2025-09-07 04:15:44 | → | pierrot joins (~pi@user/pierrot) |
| 2025-09-07 04:19:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-07 04:23:23 | → | tavare joins (~tavare@user/tavare) |
| 2025-09-07 04:23:37 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
All times are in UTC.