Logs: freenode/#haskell
| 2021-03-12 23:11:55 | <hololeap> | :t take |
| 2021-03-12 23:11:57 | <lambdabot> | Int -> [a] -> [a] |
| 2021-03-12 23:12:25 | <hololeap> | @hoogle Foldable t => Int -> t a -> t a |
| 2021-03-12 23:12:27 | <lambdabot> | Data.Vector.Generic take :: Vector v a => Int -> v a -> v a |
| 2021-03-12 23:12:27 | <lambdabot> | Data.Vector.Generic drop :: Vector v a => Int -> v a -> v a |
| 2021-03-12 23:12:27 | <lambdabot> | Data.Vector.Generic unsafeTake :: Vector v a => Int -> v a -> v a |
| 2021-03-12 23:12:55 | <infinisil> | hololeap: Where I'm going I don't need take :P |
| 2021-03-12 23:13:23 | <infinisil> | Limiting recursion depth while printing using Generic's |
| 2021-03-12 23:14:11 | <Gurkenglas> | (where "number of nodes" is the length of each chain from bottom, of course :) ) |
| 2021-03-12 23:14:25 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:9d6d:f5b3:4e2:6d89) |
| 2021-03-12 23:14:36 | <hololeap> | ok, but if the data structure supports some cutoff to lazy evaluation, then you could just use Show, or am i missing something? |
| 2021-03-12 23:14:54 | <monochrom> | OK, infinitely many nodes may be infinite height or infinite breadth or both. |
| 2021-03-12 23:15:25 | <monochrom> | For finite height, do induction on height. For infinite height, oo = oo done. |
| 2021-03-12 23:15:32 | hololeap | feels the impending poke of a thorn |
| 2021-03-12 23:15:45 | <infinisil> | hololeap: How would that work? How would Show know it should not print further? |
| 2021-03-12 23:16:12 | <Gurkenglas> | i doubt that the shape of the values ought to be relevant. i agree that the proof should proceed by some sort of induction |
| 2021-03-12 23:16:35 | <hololeap> | it wouldn't because that responsibility would be pushed onto something that passes to show |
| 2021-03-12 23:16:42 | <monochrom> | And the tree just has to be y in tree form, which can still has a few bottoms and that's why it can still be finite height. We are just evolving x towards y, not towards normal form. |
| 2021-03-12 23:16:58 | × | joebobjoe quits (~joebobjoe@unaffiliated/joebobjoe) (Ping timeout: 276 seconds) |
| 2021-03-12 23:17:20 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:9d6d:f5b3:4e2:6d89) (Client Quit) |
| 2021-03-12 23:17:23 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:c79:3d13:d977:c947) |
| 2021-03-12 23:17:23 | <Gurkenglas> | i'd be interested whether the proof depends on some other statements that are true for haskell types but not every pointed algebraic domain with arbitrary meets |
| 2021-03-12 23:17:26 | × | mouseghost quits (~draco@wikipedia/desperek) (Quit: mew wew) |
| 2021-03-12 23:18:02 | → | usr25_tm joins (~usr25@unaffiliated/usr25) |
| 2021-03-12 23:18:28 | <infinisil> | hololeap: Ah yeah but I don't want to do that in my case |
| 2021-03-12 23:18:45 | <monochrom> | I think you need computability-related assumptions, such as "no continuum between two values, ever". |
| 2021-03-12 23:18:53 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 2021-03-12 23:18:59 | <monochrom> | In fact, no Zeno paradox either. |
| 2021-03-12 23:19:08 | <infinisil> | hololeap: I have like 100 data types that I want to log, and some of them can get arbitrarily large in size. Using show would print arbitrarily long log lines |
| 2021-03-12 23:19:29 | <infinisil> | I'm creating a class like Show, but which allows limiting the recursion depth generically |
| 2021-03-12 23:19:30 | → | elliott__ joins (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) |
| 2021-03-12 23:20:17 | × | borne quits (~fritjof@200116b86456970065fd8eaafdc5f06e.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 2021-03-12 23:21:04 | × | elliott__ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Client Quit) |
| 2021-03-12 23:21:08 | <hololeap> | i wonder if there is a typeclass for any recursive data structure that can count its depth |
| 2021-03-12 23:21:37 | <hololeap> | that sounds more useful than a specialized Show, IMO |
| 2021-03-12 23:21:43 | × | usr25 quits (~usr25@unaffiliated/usr25) (Ping timeout: 245 seconds) |
| 2021-03-12 23:21:54 | <infinisil> | Hmm yeah it does |
| 2021-03-12 23:22:03 | <Gurkenglas> | (huh i didnt even notice till now but there exist infinite descending chains, such as iterate (bottom:) (repeat ())) |
| 2021-03-12 23:22:06 | <monochrom> | I think this is a requirement you need and it's a well-established extra condition in domain theory to acknowledge that we're talking about computing. |
| 2021-03-12 23:22:11 | <infinisil> | hololeap: Though that wouldn't work, because `countDepth [1..] = \infty` |
| 2021-03-12 23:22:39 | × | dhouthoo quits (~dhouthoo@ptr-eitgbj2w0uu6delkbrh.18120a2.ip6.access.telenet.be) (Quit: WeeChat 3.0) |
| 2021-03-12 23:22:54 | martin02_ | is now known as martin02 |
| 2021-03-12 23:23:02 | × | blueonyx quits (b9d4ab4b@unaffiliated/blueonyx) (Ping timeout: 240 seconds) |
| 2021-03-12 23:23:03 | <monochrom> | There is a definition of "finite element". It's very technical, but the idea is that, e.g., 4 : 4 : bottom is finite, 4 : 4 : 4 : ... (to no end) is not finite. |
| 2021-03-12 23:23:06 | × | DataComputist quits (~lumeng@50.43.26.251) (Ping timeout: 246 seconds) |
| 2021-03-12 23:23:38 | <monochrom> | And the extra requirement is this: Every x equals the lub of all finite elements below x. |
| 2021-03-12 23:23:57 | × | __minoru__shirae quits (~shiraeesh@109.166.56.60) (Ping timeout: 264 seconds) |
| 2021-03-12 23:24:09 | → | DataComputist joins (~lumeng@50.43.26.251) |
| 2021-03-12 23:24:27 | <hololeap> | i'm thinking something along the lines of `takeR :: Recursive t => Int -> r a -> r a` and `showUntil :: (Show1 t, Recursive t) => Int -> r a -> String` |
| 2021-03-12 23:24:48 | <hololeap> | oops s/t/r/ |
| 2021-03-12 23:25:46 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-03-12 23:26:21 | <hololeap> | infinisil: i'm not saying it's better than your idea, just a bit more general perhaps |
| 2021-03-12 23:26:40 | <Gurkenglas> | finite x are exactly compact x, yes? aka every chain with lub x includes x |
| 2021-03-12 23:27:09 | <Gurkenglas> | then "every x equals the lub of all finite elements below x" is exactly "algebraic" |
| 2021-03-12 23:27:10 | → | borne joins (~fritjof@200116b86456970065fd8eaafdc5f06e.dip.versatel-1u1.de) |
| 2021-03-12 23:27:18 | <infinisil> | hololeap: Hmm yeah that does sound interesting |
| 2021-03-12 23:27:52 | × | rj quits (~x@gateway/tor-sasl/rj) (Ping timeout: 268 seconds) |
| 2021-03-12 23:28:09 | <infinisil> | hololeap: Though what would it replace the values that it cuts off with? |
| 2021-03-12 23:28:10 | <Gurkenglas> | (assuming meets, i think) |
| 2021-03-12 23:28:39 | × | xsperry quits (~as@unaffiliated/xsperry) (Remote host closed the connection) |
| 2021-03-12 23:29:04 | <Gurkenglas> | (nevermind should work without meets) |
| 2021-03-12 23:29:25 | <hololeap> | i know that someone here has refered to recursion-schemes as "a joke." not sure why; probably something to do with performance |
| 2021-03-12 23:29:53 | <hololeap> | i've always thought that abstracting out the recursive part of recursive data types was a neat idea |
| 2021-03-12 23:30:06 | infinisil | agrees |
| 2021-03-12 23:30:35 | <infinisil> | Would it maybe be something like `takeR :: Recursive r => Int -> r a -> r (Maybe a)`? |
| 2021-03-12 23:31:17 | → | usr256 joins (~usr25@unaffiliated/usr25) |
| 2021-03-12 23:31:18 | → | rj joins (~x@gateway/tor-sasl/rj) |
| 2021-03-12 23:31:34 | × | pera quits (~pera@unaffiliated/pera) (Read error: Connection reset by peer) |
| 2021-03-12 23:32:35 | <infinisil> | hololeap: monochrom: Oh the Data class kind of looks very relevant: https://hackage.haskell.org/package/base-4.11.0.0/docs/Data-Data.html#t:Data |
| 2021-03-12 23:32:43 | <hololeap> | that depends on if the functor you're recursing over has some sort of "nullary constructor" |
| 2021-03-12 23:32:46 | <infinisil> | I have a feeling such a recursion-limiting print could be implemented with this |
| 2021-03-12 23:32:47 | <Gurkenglas> | https://hackage.haskell.org/package/free-5.1.6/docs/Control-Monad-Free.html#v:cutoff :) |
| 2021-03-12 23:33:13 | <infinisil> | Gurkenglas: Oh nice! |
| 2021-03-12 23:33:33 | × | notzmv quits (~zmv@unaffiliated/zmv) (Ping timeout: 264 seconds) |
| 2021-03-12 23:33:40 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2021-03-12 23:33:48 | <Gurkenglas> | ekmett got there a decade ago |
| 2021-03-12 23:33:49 | <monochrom> | compact and finite coincide for complete lattices. But I'm afraid compactness doesn't make sense for most domains. Most domains refuse to be complete lattices. |
| 2021-03-12 23:34:16 | <hololeap> | some subset of Recursive woudld be data types that recurse over a functor that can short circuit the recursion |
| 2021-03-12 23:35:07 | → | myShoggoth joins (~myShoggot@75.164.81.55) |
| 2021-03-12 23:35:21 | × | usr25_tm quits (~usr25@unaffiliated/usr25) (Ping timeout: 264 seconds) |
| 2021-03-12 23:35:44 | <Gurkenglas> | monochrom, lemme guess finite will end up being "the length of each finest chain from bottom to x is finite" |
| 2021-03-12 23:36:54 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 256 seconds) |
| 2021-03-12 23:37:11 | <Gurkenglas> | (aka the most defined [()] -> () wouldn't be finite) |
| 2021-03-12 23:37:51 | <hololeap> | so, Fix (a,) is isomorphic to an infinite stream and the recursion will go on as long as we are willing to consume it, but Fix (Compose Maybe (a,)) is isomorphic to a list (did i get that right?) and it could end at any moment |
| 2021-03-12 23:38:02 | <monochrom> | I hope it's true. But the definition I know doesn't say it directly (pun intended, just you wait), and I don't have any idea what it means except when applied to ADTs for example it does come out as "finite tree height". |
| 2021-03-12 23:39:13 | <monochrom> | Here is the definition: k is finite iff for every directed set D, if k is below the join of D, then k is below someone in D. |
| 2021-03-12 23:40:08 | <Gurkenglas> | yep thats compact. is my version different? |
| 2021-03-12 23:41:21 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 264 seconds) |
| 2021-03-12 23:41:42 | <monochrom> | compactness removes "directed". and it s/someone in D/some finite subset of D/ |
| 2021-03-12 23:41:43 | <hololeap> | infinisil: actually, no, you don't need to return `r (Maybe a)`, even if your recursive type may be finite, just like `take` doesn't return [Maybe a] |
| 2021-03-12 23:41:51 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-03-12 23:41:58 | <monochrom> | err, s/someone in D/join of some finite subset of D/ |
| 2021-03-12 23:42:11 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-12 23:42:21 | <hololeap> | it either returns the structure up to the depth you specified, or up to the end of the structure. whichever is shortest. |
| 2021-03-12 23:43:23 | <monochrom> | I would play safe and not use compactness per se because it presumes arbitrary joins exist, which is false for the actually useful domains. |
| 2021-03-12 23:43:33 | <hololeap> | infinisil: but how would you handle rose trees, for instance, where the possible inifinty is in two dimensions? |
| 2021-03-12 23:43:33 | <Gurkenglas> | oh man i really hope im just confused and everyone doesnt actually override the same terminology |
| 2021-03-12 23:43:37 | → | bergey` joins (~user@pool-74-108-99-127.nycmny.fios.verizon.net) |
| 2021-03-12 23:43:43 | <monochrom> | In terms of intuition it's OK to analogize them of course. |
| 2021-03-12 23:43:45 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
All times are in UTC.