Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 785 786 787 788 789 790 791 792 793 794 795 .. 5022
502,152 events total
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.