Logs: freenode/#haskell
| 2021-02-28 21:07:29 | <dolio> | stg isn't runtime, either, though. |
| 2021-02-28 21:07:40 | <Cale> | true |
| 2021-02-28 21:08:00 | <rednaZ[m]> | There is also the indicator that they can form a lambda that kills sharing. |
| 2021-02-28 21:08:01 | <dolio> | Isn't stg still possible to type check? |
| 2021-02-28 21:08:02 | <edwardk> | beyond that you start hitting things like linking out to imgui and wrapping vulkan/opengl/directx as a shallow interaction layer, but none of those except qt-quick looks very native |
| 2021-02-28 21:08:03 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 2021-02-28 21:08:40 | <Cale> | dolio: It's imperative-ish code, but... maybe? |
| 2021-02-28 21:08:43 | <rednaZ[m]> | dolio: type arguments are not in stg |
| 2021-02-28 21:08:44 | <edwardk> | dolio: i thought we'd started adding those branch coalescing moves where it takes Left a -> Left a -- even when the types don't match, etc. to STG |
| 2021-02-28 21:08:54 | → | xff0x joins (~xff0x@2001:1a81:5349:9200:2806:fad1:e222:a1c8) |
| 2021-02-28 21:09:16 | <dolio> | Ah, perhaps. |
| 2021-02-28 21:09:27 | <rednaZ[m]> | If I have `binder = \ coercion -> f x`, f x is not memoized. |
| 2021-02-28 21:09:37 | <rednaZ[m]> | So this tells me that the coercion argument either exists at run time or there is a crazy bug in GHC. |
| 2021-02-28 21:10:18 | <dolio> | Just because sharing is lost doesn't mean coercions are explicitly represented at runtime. |
| 2021-02-28 21:10:31 | <rednaZ[m]> | ? |
| 2021-02-28 21:10:51 | <Cale> | Causing things to be shared when they otherwise wouldn't be, would itself be regarded as a bug, I think |
| 2021-02-28 21:11:03 | <edwardk> | rednaz[m]: i can make things that take a 0-width argument and still turn the result into call-by-name. |
| 2021-02-28 21:11:20 | <edwardk> | e.g. (##) -> Int# |
| 2021-02-28 21:11:37 | <edwardk> | so even if the argument is erased it can affect 'memoization' |
| 2021-02-28 21:11:49 | <rednaZ[m]> | Why would you want that though? |
| 2021-02-28 21:11:54 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 2021-02-28 21:12:06 | <edwardk> | rednaZ[m]: funny you should ask. i actually _have_ to use it in code i'm writing now ;) |
| 2021-02-28 21:12:08 | <Cale> | Because sharing things can result in exponentially increasing the amount of memory required |
| 2021-02-28 21:12:23 | <edwardk> | i use type Lev (a :: TYPE r) = (()~()) => a -- in practice |
| 2021-02-28 21:12:46 | <edwardk> | ifThenElse :: Bool -> Lev a -> Lev a -> a; ifThenElse True a _ = a; ifThenElse False _ b = b |
| 2021-02-28 21:12:50 | <dolio> | There are probably situations where code needs to be emitted for an infinite loop that involves carrying around formal 0-width parameters that are only eliminated at a sufficiently low level for everything to already be sequential. |
| 2021-02-28 21:13:04 | <edwardk> | gives me a levity polymorphic if then else in RebindableSyntax that works for all runtimereps with one implementation that is properly laze |
| 2021-02-28 21:13:21 | <edwardk> | er lazy |
| 2021-02-28 21:13:45 | <Cale> | Here's an example (though I don't have one with a zero-width argument off-hand): permutations [] = [[]]; permutations (x:xs) = permutations xs ++ map (x:) (permutations xs) |
| 2021-02-28 21:13:50 | <Cale> | oops |
| 2021-02-28 21:13:55 | <Cale> | that should be combinations |
| 2021-02-28 21:13:56 | <edwardk> | so e.g. if you ifThenElse True 1# undefined -- it evaluates to 1# not undefined, like you'd get if you magically passed arguments 'a' at the right runtimerep. |
| 2021-02-28 21:13:57 | <Cale> | of course |
| 2021-02-28 21:14:14 | <dolio> | Because otherwise an equation that gets proved by an infinite loop might be 'optimized' to and unsound function. |
| 2021-02-28 21:14:34 | <Cale> | If we change it to share: combinations (x:xs) = let cs = combinations xs in cs ++ map (x:) cs |
| 2021-02-28 21:14:36 | <edwardk> | yeah dolio demonstrated this to me when i was trying to do a similar batch of tricks back when we worked together |
| 2021-02-28 21:15:01 | <edwardk> | now i make my newtype based versions of these things using evil pattern synonym tricks to regenerate the ~''s |
| 2021-02-28 21:15:34 | <Cale> | Then we have a space leak, where we have to hang on to cs at least until halfway through the list (and sublists of cs until much later) |
| 2021-02-28 21:15:37 | → | fendor_ joins (~fendor@178.165.129.154.wireless.dyn.drei.com) |
| 2021-02-28 21:15:57 | <rednaZ[m]> | Unfortunately I have a case where I wish the equality constraint would not destroy sharing. |
| 2021-02-28 21:16:03 | <rednaZ[m]> | Is there a way to tell GHC that? |
| 2021-02-28 21:16:08 | × | Codaraxis quits (Codaraxis@gateway/vpn/mullvad/codaraxis) (Remote host closed the connection) |
| 2021-02-28 21:16:29 | → | Codaraxis joins (Codaraxis@gateway/vpn/mullvad/codaraxis) |
| 2021-02-28 21:17:57 | × | fendor quits (~fendor@178.115.128.216.wireless.dyn.drei.com) (Ping timeout: 264 seconds) |
| 2021-02-28 21:17:58 | <edwardk> | rednaZ[m]: the pattern i'd probably use is to do something like capture the f x outside of the lambda that is taking the equality witness by computing y = f (unsafeCoerce x) or whatever. then inside the lambda prove the type of x matches the type of f's arguments using your equality then return y, otherwise leave it alone |
| 2021-02-28 21:17:59 | <Cale> | Maybe, though it seems like it would be tricky in practice -- if you can somehow define the body outside the coercion lambda |
| 2021-02-28 21:18:13 | <edwardk> | its a thunk with an invalid type but you never force it except when the types line up |
| 2021-02-28 21:18:19 | × | tanuki quits (~quassel@173.168.154.189) (Ping timeout: 260 seconds) |
| 2021-02-28 21:18:22 | <Cale> | Ah yeah |
| 2021-02-28 21:18:30 | → | elliott__ joins (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) |
| 2021-02-28 21:19:00 | <edwardk> | that should restore sharing |
| 2021-02-28 21:20:26 | → | tanuki joins (~quassel@173.168.154.189) |
| 2021-02-28 21:21:10 | <rednaZ[m]> | I have to think about whether I can apply that to my case. I have just uploaded my case too if you are curious, https://github.com/prednaz/open-sum/blob/type_equality/app/Main.hs#L38 . |
| 2021-02-28 21:21:44 | <rednaZ[m]> | It is about checked exceptions and what happens if you evaluate a computation twice catching the exceptions in different order. |
| 2021-02-28 21:22:06 | <rednaZ[m]> | Than you would want sharing. |
| 2021-02-28 21:22:37 | × | xlei quits (znc@unaffiliated/xlei) (Ping timeout: 256 seconds) |
| 2021-02-28 21:22:37 | <rednaZ[m]> | The type variable of OpenSum is a phantom type. |
| 2021-02-28 21:23:11 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:256c:b3b1:f90:ff2a) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-02-28 21:23:15 | → | nullniverse joins (~null@unaffiliated/nullniverse) |
| 2021-02-28 21:23:47 | → | elfets joins (~elfets@37.201.23.96) |
| 2021-02-28 21:24:20 | × | sparsity quits (5eae2591@gateway/web/cgi-irc/kiwiirc.com/ip.94.174.37.145) (Quit: Connection closed) |
| 2021-02-28 21:24:29 | <edwardk> | OpenSum = Dynamic? |
| 2021-02-28 21:25:25 | <edwardk> | oh, no, there's a list argument |
| 2021-02-28 21:25:34 | edwardk | goes and reads |
| 2021-02-28 21:25:41 | <rednaZ[m]> | data OpenSum list = forall value. Typeable value => OpenSum value |
| 2021-02-28 21:26:07 | <rednaZ[m]> | `list` is a phantom type-level list |
| 2021-02-28 21:26:10 | <edwardk> | why do you need the Typeable btw, rather than just the list index? |
| 2021-02-28 21:26:29 | <rednaZ[m]> | Because then the run-time representation is different |
| 2021-02-28 21:26:43 | <rednaZ[m]> | for different list orders |
| 2021-02-28 21:26:59 | <rednaZ[m]> | and the list order has to be determined by the order of catching |
| 2021-02-28 21:27:04 | <edwardk> | fair |
| 2021-02-28 21:27:10 | <rednaZ[m]> | because it cannot stay undetermined |
| 2021-02-28 21:27:29 | <rednaZ[m]> | which is kind of funny |
| 2021-02-28 21:28:09 | <rednaZ[m]> | there is no other reason why I can only catch the type at the head of the list |
| 2021-02-28 21:28:43 | → | bergey joins (~user@pool-74-108-99-127.nycmny.fios.verizon.net) |
| 2021-02-28 21:29:05 | × | gienah quits (~mwright@gentoo/developer/gienah) (Quit: Lost terminal) |
| 2021-02-28 21:29:15 | <rednaZ[m]> | I am still in the process of trying your idea out but I am afraid, it is probably only effective if I apply it to user code. |
| 2021-02-28 21:33:33 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 264 seconds) |
| 2021-02-28 21:34:03 | × | nf quits (~n@monade.li) (Ping timeout: 260 seconds) |
| 2021-02-28 21:34:04 | × | bergey quits (~user@pool-74-108-99-127.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 2021-02-28 21:34:12 | → | nf__ joins (~n@monade.li) |
| 2021-02-28 21:34:46 | nf__ | is now known as nf |
| 2021-02-28 21:36:21 | <edwardk> | ok, if you're using this to hold Exceptions anyways, you'll always have a Typeable constraint, i guess my grumbles there are mostly sated |
| 2021-02-28 21:36:58 | → | nullniv15 joins (~null@unaffiliated/nullniverse) |
| 2021-02-28 21:37:20 | × | nullniverse quits (~null@unaffiliated/nullniverse) (Read error: No route to host) |
| 2021-02-28 21:37:21 | × | nullniv15 quits (~null@unaffiliated/nullniverse) (Read error: Connection reset by peer) |
| 2021-02-28 21:37:45 | → | nullniverse joins (~null@unaffiliated/nullniverse) |
| 2021-02-28 21:37:46 | × | nullniverse quits (~null@unaffiliated/nullniverse) (Max SendQ exceeded) |
| 2021-02-28 21:38:00 | × | geekosaur quits (ae68c070@cpe-174-104-192-112.neo.res.rr.com) (Quit: Connection closed) |
| 2021-02-28 21:38:42 | <NieDzejkob> | I have a set of tuples (a, b, c) and I need to retrieve the ones with matching a or b at different moments. Is there a better way to do this than multiple Maps that I have to keep in sync manually? |
| 2021-02-28 21:39:20 | → | Tario joins (~Tario@200.119.184.155) |
| 2021-02-28 21:40:33 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-83-46.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-02-28 21:40:48 | <rednaZ[m]> | edwardk: I would not have the Typeable constraint if it did not seem like the most promising approach right now. GHC is actually often floating the expensive computation out from under the coercion argument lambda recovering sharing already. But it is not often enough. |
| 2021-02-28 21:40:52 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-83-46.w86-212.abo.wanadoo.fr) |
| 2021-02-28 21:41:01 | → | redmp joins (~redmp@172.58.38.156) |
| 2021-02-28 21:43:06 | → | psutcliffe joins (~psutcliff@2a00:801:3f2:4b56:e93e:1663:ff0c:6c42) |
| 2021-02-28 21:44:02 | <hololeap> | NieDzejkob: define "better" |
| 2021-02-28 21:44:11 | <NieDzejkob> | less error-prone |
| 2021-02-28 21:44:52 | <NieDzejkob> | Making illegal states unrepresentable and all that |
| 2021-02-28 21:45:08 | <hololeap> | i'm actually having a hard time imagining what you're talking about |
All times are in UTC.