Logs: freenode/#haskell
| 2020-10-21 20:52:27 | <hololeap> | ski: so how would this look using the Logic monad? |
| 2020-10-21 20:52:44 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-21 20:53:19 | <ski> | well |
| 2020-10-21 20:53:26 | <ski> | first a little detour |
| 2020-10-21 20:53:51 | <ski> | consider how ordinary functions or procedures, in a strict programming language (like e.g. C) can be implemented |
| 2020-10-21 20:54:18 | <ski> | when calling a function, we will need to tell it where execution is to continue, after it has done its work |
| 2020-10-21 20:55:10 | × | texasmynsted quits (~texasmyns@104.140.52.83) (Ping timeout: 246 seconds) |
| 2020-10-21 20:55:38 | <ski> | in assembler, there's commonly an `rts' instruction, for returning, and a `jsr' or `call' instruction, for calling. the latter will e.g. put the address of the next instruction in a register, or on the stack. and the former will jump to that address, resuming control to the caller |
| 2020-10-21 20:55:40 | × | z0 quits (~z0@bl15-167-204.dsl.telepac.pt) (Quit: leaving) |
| 2020-10-21 20:55:51 | <ski> | the return address is a continuation |
| 2020-10-21 20:56:35 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Quit: Lost terminal) |
| 2020-10-21 20:56:51 | → | z0 joins (~z0@bl15-167-204.dsl.telepac.pt) |
| 2020-10-21 20:56:52 | × | knupfer quits (~Thunderbi@200116b82c30ba0001bfef634072ae05.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 2020-10-21 20:56:54 | <ski> | conceptually, it's an extra parameter that we pass, when calling a "function" (really, jumping to a memory address, with the expectation that parameters are passed in some standard locations, usually either in registers, or at some position relative to a current stack pointer) |
| 2020-10-21 20:57:34 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-10-21 20:57:50 | × | z0 quits (~z0@bl15-167-204.dsl.telepac.pt) (Client Quit) |
| 2020-10-21 20:58:25 | <ski> | in Haskell, a type `T' is equivalent to `forall o. (T -> o) -> o' (aka `forall o. Cont o T'). here the callback argument of type `T -> o' plays the same role as "what to do after" |
| 2020-10-21 20:59:15 | <ski> | but, to (efficiently) implement the Prolog execution, we need some way to be able to resume execution inside a call, e.g. to between/3, after it has already returned successfully ! |
| 2020-10-21 21:00:02 | × | zigapeda1 quits (~zigapeda@195.140.213.38) () |
| 2020-10-21 21:00:19 | <ski> | so, when between/3 returns, having succeeded in finding a solution, it will tell us a "redo" address, which we can jump to, if/when we're not satisfied with the current solution, would like the call to try to find another one, the next one |
| 2020-10-21 21:01:13 | <ski> | similarly, since a call may fail to have any solutions, and we may also run out of all the solutions it has, we need some way to tell it what to do (where to jump), if case it fails to find any (more) solutions. this is the "failure continuation" |
| 2020-10-21 21:01:28 | → | texasmyn_ joins (~texasmyns@104.140.52.83) |
| 2020-10-21 21:01:54 | <ski> | so, instead of passing a single "return address", when calling a function, we're to pass two addresses. one being a "success continuation", and one being a "failure continuation" |
| 2020-10-21 21:02:18 | <ski> | in case there's no (more) solutions, it'll continue using the latter |
| 2020-10-21 21:02:18 | × | ixlun quits (~matthew@213.205.241.94) (Read error: Connection reset by peer) |
| 2020-10-21 21:02:36 | × | nineonin_ quits (~textual@216.81.48.202) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2020-10-21 21:03:14 | <ski> | in case there's one (more) solution, it'll continue, using the former. also passing to the former the "redo", which is what we'll pass as "failure continuation" to the next call, so it knows where to "backtrack to", if it fails (runs out of solutions) |
| 2020-10-21 21:03:23 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-21 21:03:36 | <ski> | so, consider a function of type `T -> [] U' |
| 2020-10-21 21:03:52 | <ski> | we'll replace `[] U' by continuation-passing |
| 2020-10-21 21:04:42 | <ski> | first we'll say `T -> (U -> ...) -> ...', where `U -> ...' is the (type of the) success continuation, that will be passed an `U' result/solution (if any is found) |
| 2020-10-21 21:05:20 | <ski> | but we also need a failure continuation, a separate parameter, so `T -> (U -> ...) -> (...) -> (...)' |
| 2020-10-21 21:05:58 | <ski> | if we were in a strict language, we'd need to model the failure continuation as a function (to delay computation of it) |
| 2020-10-21 21:06:08 | × | kori quits (~kori@arrowheads/kori) (Read error: Connection reset by peer) |
| 2020-10-21 21:06:25 | <ski> | we'd have `T -> (U -> ...) -> (() -> o) -> o' |
| 2020-10-21 21:07:52 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2020-10-21 21:07:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2020-10-21 21:08:00 | <ski> | e.g. consider a definition of `between :: Integer -> Integer -> Logic Integer', where `Logic a' means something like `(a -> ...) -> (() -> o) -> o' |
| 2020-10-21 21:08:04 | <ski> | base case is |
| 2020-10-21 21:08:37 | <ski> | between lo hi succeess failure | lo > hi = failure () |
| 2020-10-21 21:08:50 | × | thir_ quits (~thir@p200300f27f19de00eca173dc7e5d6773.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2020-10-21 21:09:22 | <ski> | so, if there's no integers within the given bounds, we (tail-)call the failure continuation |
| 2020-10-21 21:09:50 | <ski> | (and this forces the return type of the failure continuation to be the same as the overall return type. the "final result/answer" type `o') |
| 2020-10-21 21:10:20 | <ski> | next, we need to elaborate the type of the success continuation |
| 2020-10-21 21:10:55 | → | hekkaidekapus} joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 2020-10-21 21:10:55 | <ski> | i said that it should be passed (by `between', in this case), a "redo", where to continue, if we want to search for more solutions |
| 2020-10-21 21:11:10 | × | noteness_ quits (noteness@unaffiliated/nessessary129) (Quit: I'LL BE BACK) |
| 2020-10-21 21:11:35 | → | noteness joins (noteness@unaffiliated/nessessary129) |
| 2020-10-21 21:11:43 | <ski> | and i mentioned that that "redo" is actually also a failure continuation (which could be passed to further calls, down the line, to let them know where to go (back, where to backtrack to), if they fail to find any solution) |
| 2020-10-21 21:12:23 | × | hekkaidekapus{ quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds) |
| 2020-10-21 21:12:41 | <ski> | so, we refine `T -> (U -> ...) -> (() -> o) -> o' further to `T -> (U -> (() -> o) -> o) -> (() -> o) -> o' (so `Logic a' is `(a -> (() -> o) -> o) -> (() -> o) -> o', or actually `forall o. (a -> (() -> o) -> o) -> (() -> o) -> o') |
| 2020-10-21 21:13:01 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 2020-10-21 21:13:08 | <ski> | so, the successful case of `between' now becomes |
| 2020-10-21 21:13:17 | × | jud quits (~jud@unaffiliated/jud) (Read error: Connection reset by peer) |
| 2020-10-21 21:13:20 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-21 21:13:34 | × | tnm quits (~tnm@dslb-084-056-234-071.084.056.pools.vodafone-ip.de) (Quit: leaving) |
| 2020-10-21 21:13:52 | × | ph88 quits (~ph88@2a02:8109:9e40:2704:4db:e8f1:c91e:6140) (Quit: Leaving) |
| 2020-10-21 21:13:54 | <ski> | between lo hi success failure = success lo redo |
| 2020-10-21 21:13:56 | <ski> | where |
| 2020-10-21 21:14:14 | <ski> | redo () = between (lo + 1) hi success failure |
| 2020-10-21 21:14:45 | <ski> | however, in a non-strict language, we can drop the `()' argument types, so we have just |
| 2020-10-21 21:15:13 | <ski> | between :: Integer -> Integer -> ((Integer -> o -> o) -> o -> o) |
| 2020-10-21 21:16:37 | <ski> | hololeap : so .. this is more or less what `Logic' does. next, you'd go on to define conjunction (which is basically `(>>=)'), and also disjunction |
| 2020-10-21 21:17:35 | × | coot quits (~coot@37.30.51.94.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2020-10-21 21:17:36 | <ski> | what the CPS does, in Haskell, is it makes the "list of successes/solutions" virtual, passed directly to consumers |
| 2020-10-21 21:17:53 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-10-21 21:18:22 | → | falafel joins (~falafel@71-34-132-121.clsp.qwest.net) |
| 2020-10-21 21:22:16 | → | borne joins (~fritjof@200116b864c00d0000dd0a7f6ac41015.dip.versatel-1u1.de) |
| 2020-10-21 21:22:27 | → | irc_user joins (uid423822@gateway/web/irccloud.com/x-ozudxpdqqqotmvjh) |
| 2020-10-21 21:23:47 | → | Pitaya joins (~mdomin45@cpe-24-211-129-187.nc.res.rr.com) |
| 2020-10-21 21:24:18 | × | Plantain quits (~mdomin45@cpe-24-211-129-187.nc.res.rr.com) (Ping timeout: 260 seconds) |
| 2020-10-21 21:24:32 | → | christo joins (~chris@81.96.113.213) |
| 2020-10-21 21:25:16 | <hololeap> | but we also need a continuation of sorts, that ignores its argument, to be used in the case of failure |
| 2020-10-21 21:25:21 | <hololeap> | i'm with you so far |
| 2020-10-21 21:26:31 | <ski> | (some of that may have been a bit unclear. do yell if you wonder about something) |
| 2020-10-21 21:27:13 | × | jsynacek quits (~jsynacek@ip-185-149-130-112.kmenet.cz) (Ping timeout: 260 seconds) |
| 2020-10-21 21:28:11 | <ski> | (btw, `between' is just a version of `enumFromTo', which is what `\lo hi -> [lo .. hi]' amounts to) |
| 2020-10-21 21:28:22 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Ping timeout: 260 seconds) |
| 2020-10-21 21:29:24 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-21 21:30:12 | × | notnatebtw quits (~nate@110.138.18.157) (Quit: WeeChat 2.9) |
| 2020-10-21 21:30:39 | <tomsmeding> | this is a new one: 'variance introduced by outliers: -9223372036854775808% (severely inflated)' |
| 2020-10-21 21:30:46 | → | notnatebtw joins (~nate@110.138.18.157) |
| 2020-10-21 21:31:15 | → | wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 2020-10-21 21:31:34 | → | nexya joins (2eef64c3@marwin.brg.sgsnet.se) |
| 2020-10-21 21:31:35 | <koz_> | Uhh... |
| 2020-10-21 21:31:47 | <koz_> | That's an oddly specific number there. |
| 2020-10-21 21:31:51 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2020-10-21 21:32:00 | <ski> | negative variance ? |
| 2020-10-21 21:32:07 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-21 21:32:24 | <tomsmeding> | unsure |
| 2020-10-21 21:32:30 | <tomsmeding> | it _is_ an oddly specific number |
| 2020-10-21 21:32:57 | <ski> | criterion ? |
| 2020-10-21 21:33:01 | <tomsmeding> | yeah |
| 2020-10-21 21:33:21 | <tomsmeding> | > printf "%x" 9223372036854775808 |
| 2020-10-21 21:33:23 | <lambdabot> | error: |
| 2020-10-21 21:33:23 | <lambdabot> | • Ambiguous type variable ‘a0’ arising from a use of ‘show_M315352001722... |
| 2020-10-21 21:33:23 | <lambdabot> | prevents the constraint ‘(Show a0)’ from being solved. |
| 2020-10-21 21:33:30 | <tomsmeding> | > printf "%x" (9223372036854775808 :: Integer) |
| 2020-10-21 21:33:32 | <lambdabot> | error: |
| 2020-10-21 21:33:32 | <lambdabot> | • Ambiguous type variable ‘a0’ arising from a use of ‘show_M830512809473... |
All times are in UTC.