| 2024-05-01 00:01:18 +0200 | <mauke> | ich begreif es auch nicht |
| 2024-05-01 00:04:16 +0200 | Square3 | (~Square4@user/square) |
| 2024-05-01 00:07:15 +0200 | Square | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2024-05-01 00:08:24 +0200 | masterbuilder | (~quassel@user/masterbuilder) (Ping timeout: 260 seconds) |
| 2024-05-01 00:08:34 +0200 | masterbuilder | (~quassel@user/masterbuilder) |
| 2024-05-01 00:10:55 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21) (Quit: WeeChat 4.2.2) |
| 2024-05-01 00:11:08 +0200 | phma | (~phma@2001:5b0:2172:9258:5c6c:8366:4239:d1fd) (Read error: Connection reset by peer) |
| 2024-05-01 00:13:16 +0200 | madeleine-sydney | (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 2024-05-01 00:14:54 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-05-01 00:19:20 +0200 | waldo | (~waldo@user/waldo) |
| 2024-05-01 00:20:49 +0200 | phma | (~phma@host-67-44-208-133.hnremote.net) |
| 2024-05-01 00:46:06 +0200 | Nixkernal | (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch) (Ping timeout: 252 seconds) |
| 2024-05-01 00:46:26 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-01 00:53:35 +0200 | <EvanR> | int-e, i met a guy in seattle recently who is making and selling neon signs |
| 2024-05-01 00:53:51 +0200 | <EvanR> | bars around here still have a lot of em xD |
| 2024-05-01 00:58:50 +0200 | <waldo> | you know what they will do then |
| 2024-05-01 00:58:59 +0200 | <waldo> | nuke the subduction zone |
| 2024-05-01 01:04:42 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-05-01 01:10:16 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-05-01 01:10:28 +0200 | acidjnk | (~acidjnk@p200300d6e714dc3178eb6b7df1157d0e.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2024-05-01 01:11:02 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2024-05-01 01:12:10 +0200 | xff0x | (~xff0x@softbank219059019218.bbtec.net) |
| 2024-05-01 01:19:17 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 240 seconds) |
| 2024-05-01 01:30:19 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-05-01 01:43:07 +0200 | <jackdk> | I'm trying to find a blog post where the author (ab?)used the typeclass system to track the set of "resources" (or was it tables?) that a function needed to do its work. From memory it it involved the use of `Dict` and some evil coercions to satisfy different type classes with empty dictionaries, and may have been posted within the last year or so? Does anyone know what I'm talking about? |
| 2024-05-01 01:47:27 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 268 seconds) |
| 2024-05-01 01:49:48 +0200 | <[Leary]> | jackdk: I don't know it, but I recall the paper 'The Foil: Capture-Avoiding Substitution With No Sharp Edges' describes similar techniques for tracking name freshness. |
| 2024-05-01 01:52:36 +0200 | <geekosaur> | I find https://prophetlabs.de/posts/unsafeCoerceDict.html but doesn't quite sound like the same thing |
| 2024-05-01 01:52:41 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-05-01 01:53:37 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
| 2024-05-01 01:58:08 +0200 | waldo | (~waldo@user/waldo) (Quit: waldo) |
| 2024-05-01 02:03:32 +0200 | lol_ | jcarpenter2 |
| 2024-05-01 02:04:01 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-05-01 02:04:38 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-01 02:08:23 +0200 | <jackdk> | Thanks but it's neither of those. It was more like a typelevel answer to the question "what resources is this function going to touch?" in a way that let you accumulate the names in a constraint and pull them down to the value level to write out a policy or equivalent |
| 2024-05-01 02:14:39 +0200 | mima | (~mmh@aftr-62-216-211-165.dynamic.mnet-online.de) (Ping timeout: 260 seconds) |
| 2024-05-01 02:43:47 +0200 | wroathe | (~wroathe@24-152-179-157.fttp.usinternet.com) |
| 2024-05-01 02:43:47 +0200 | wroathe | (~wroathe@24-152-179-157.fttp.usinternet.com) (Changing host) |
| 2024-05-01 02:43:47 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2024-05-01 02:44:57 +0200 | whatsupdoc | (uid509081@id-509081.hampstead.irccloud.com) |
| 2024-05-01 02:47:05 +0200 | xff0x | (~xff0x@softbank219059019218.bbtec.net) (Ping timeout: 252 seconds) |
| 2024-05-01 02:51:02 +0200 | <jackdk> | It was https://reasonablypolymorphic.com/blog/abusing-constraints/ |
| 2024-05-01 02:53:14 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) |
| 2024-05-01 02:55:23 +0200 | <talismanick> | If a free monad is a tree of expressions, is there a DAG analogue? |
| 2024-05-01 02:57:02 +0200 | <geekosaur> | oh, right, I saw that a few months ago |
| 2024-05-01 03:00:13 +0200 | <geekosaur> | talismanick, isn't it actually a DAG anyway? cycles would severely limit the monads you could use to "interpret" it |
| 2024-05-01 03:02:05 +0200 | pointlessslippe1 | (~pointless@212.82.82.3) (Ping timeout: 240 seconds) |
| 2024-05-01 03:09:19 +0200 | <ski> | hmm .. i guess you could have an operation that requires that its opeands "overlap" (have some common substructures), in some particular fashion. so a recursive decomposition of a problem (corresponding to matching on such a constructor operation) would then naturally allow dynamic programming (iow a DAG, rather than a tree, recursive decomposition/structuring of the original problem), presumably |
| 2024-05-01 03:10:01 +0200 | fryguybob | (~fryguybob@024-094-050-022.inf.spectrum.com) (Quit: leaving) |
| 2024-05-01 03:11:26 +0200 | <c_wraith> | You don't need any special structure for that, though |
| 2024-05-01 03:11:30 +0200 | <c_wraith> | You just need sharing. |
| 2024-05-01 03:14:28 +0200 | <ski> | yea, but how do you detect, or enforce, the sharing, of the iput structure, to justify the sharing of the output computation ? |
| 2024-05-01 03:14:36 +0200 | <ski> | s/iput/input/ |
| 2024-05-01 03:14:50 +0200 | <c_wraith> | pick f carefully. |
| 2024-05-01 03:15:01 +0200 | <c_wraith> | you can embed basically anything you want into f |
| 2024-05-01 03:15:04 +0200 | <ski> | iow, i'm thinking of something like a catamorphism |
| 2024-05-01 03:15:53 +0200 | waldo | (~waldo@user/waldo) |
| 2024-05-01 03:18:29 +0200 | <ski> | given an array/vector with indices from `0' to `n-1' (incl.), we could decompose this into one slice from `0' to `n-2' and one from `1' to `n-1', guaranteed to overlap on the `1' to `n-2' part. eventually, we'd get down to singleton slices, which could be the base case of a dynamic programming, then results percolating back up in a "lattive"-like structure, rather than a tree, proper, thereby taking |
| 2024-05-01 03:18:35 +0200 | <ski> | advantage of the sharing |
| 2024-05-01 03:23:41 +0200 | <talismanick> | I'm feeling a little stupid, then, trying to understand https://hackage.haskell.org/package/zsdd/docs/Data-Diagram.html |
| 2024-05-01 03:24:25 +0200 | <ski> | basically, we have, if `Just (ar01,ar12) = decompose ar012', `Just (ar0,ar1a) = decompose ar01' and `Just (ar1b,ar2) = decompose ar12', then `ar1a = ar1b' |
| 2024-05-01 03:26:03 +0200 | <talismanick> | because, if one can assume "maximal sharing", I feel like I can see in my head how a BDD might be implemented with a (real) free monad |
| 2024-05-01 03:27:48 +0200 | otto_s | (~user@p4ff27e40.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-05-01 03:29:11 +0200 | <ski> | or, in terms of composition, if `Compose (Compose ar0 ar1a) (Compose ar1b ar2) = ar012', then `ar1a = ar1b'. so we have something like `Compose :: (ar0 :: Slice n) -> (ar1 :: Slice n) -> Agree ar0 ar1 => Slice (1+n)', where `Agree (Singleton x) (Singleton y)' as well as `(ar1a = ar1b) => Agree (Compose ar0 ar1a) (Compose ar1b ar2)' (where `Agree :: Slice n -> Slice n -> Constraint') |
| 2024-05-01 03:29:12 +0200 | otto_s | (~user@p4ff27c65.dip0.t-ipconnect.de) |
| 2024-05-01 03:29:18 +0200 | <talismanick> | is it the kind of thing where it becomes obvious when you write it down? |
| 2024-05-01 03:30:28 +0200 | <ski> | hm, is "BDD" Binary Decision Diagram ? |
| 2024-05-01 03:31:09 +0200 | <talismanick> | yeah |
| 2024-05-01 03:31:19 +0200 | ski | doesn't recall what those re |
| 2024-05-01 03:31:22 +0200 | <ski> | s/re/are/ |
| 2024-05-01 03:31:46 +0200 | <talismanick> | https://en.wikipedia.org/wiki/Binary_decision_diagram |
| 2024-05-01 03:32:04 +0200 | <talismanick> | kind of like SAT solving |
| 2024-05-01 03:36:16 +0200 | <talismanick> | Is the problem is that laziness memoizes and shares for you without asking, making every tree equivalent to a DAG but not the one you want? |
| 2024-05-01 03:38:18 +0200 | <c_wraith> | well, no. The problem is sharing only happens when explicitly introduced, and doing that is going to require bookkeeping. And the memory cost of that bookkeeping is ridiculous. |
| 2024-05-01 03:43:11 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Quit: WeeChat 4.1.2) |
| 2024-05-01 03:46:30 +0200 | ski | . o O ( "BDD-Based Deductive Databasee" <https://bddbddb.sourceforge.net/> ; "Soufflé - A Datalog Synthesis Tool for Static Analysis" <https://souffle-lang.github.io> ) |