Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→
Page 1 .. 520 521 522 523 524 525 526 527 528 529 530 .. 18005
— 1,800,452 events total
2021-06-18 06:26:28 → fef joins (~thedawn@user/thedawn)
2021-06-18 06:29:33 × hmmmas quits (~chenqisu1@183.217.200.246) (Quit: Leaving.)
2021-06-18 06:36:18 × MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Read error: Connection reset by peer)
2021-06-18 06:36:52 → ijlx joins (~ijlx@dsl-50-5-224-196.fuse.net)
2021-06-18 06:37:14 → boxscape joins (~boxscape@user/boxscape)
2021-06-18 06:40:56 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:c3b0:1a89:f9cb:1a29)
2021-06-18 06:42:35 → ddellacosta joins (~ddellacos@86.106.121.100)
2021-06-18 06:45:06 × BosonCollider quits (~olofs@90-227-86-119-no542.tbcn.telia.com) (Ping timeout: 240 seconds)
2021-06-18 06:45:43 → chrysanthematic joins (~chrysanth@82.2.21.4)
2021-06-18 06:45:51 × slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving)
2021-06-18 06:47:17 × ddellacosta quits (~ddellacos@86.106.121.100) (Ping timeout: 252 seconds)
2021-06-18 06:51:29 → MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com)
2021-06-18 06:54:14 → trcc_ joins (~trcc@users-1190.st.net.au.dk)
2021-06-18 06:54:20 → dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be)
2021-06-18 06:55:01 × ijlx quits (~ijlx@dsl-50-5-224-196.fuse.net) (Quit: Client closed)
2021-06-18 06:55:28 → agumonke` joins (~user@88.163.231.79)
2021-06-18 06:55:44 × trcc_ quits (~trcc@users-1190.st.net.au.dk) (Client Quit)
2021-06-18 06:56:00 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
2021-06-18 06:56:45 → ChaiTRex joins (~ChaiTRex@user/chaitrex)
2021-06-18 06:56:45 × fef quits (~thedawn@user/thedawn) (Remote host closed the connection)
2021-06-18 06:58:01 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Client Quit)
2021-06-18 06:58:16 → ChaiTRex joins (~ChaiTRex@user/chaitrex)
2021-06-18 07:00:17 → gehmehgeh joins (~user@user/gehmehgeh)
2021-06-18 07:00:35 → tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
2021-06-18 07:00:45 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2021-06-18 07:01:40 → kuribas joins (~user@ptr-25vy0i8edjvja2944v9.18120a2.ip6.access.telenet.be)
2021-06-18 07:02:43 × ft quits (~ft@shell.chaostreff-dortmund.de) (Quit: leaving)
2021-06-18 07:03:01 → ft joins (~ft@shell.chaostreff-dortmund.de)
2021-06-18 07:05:38 <dminuoso> I have a tree in which each branch (top-to-bottom) alternates between "NwD" and "UsDC". Is there a reasonable way to encode this ontop of a plain rose tree?
2021-06-18 07:06:24 ← Franciman parts (~francesco@openglass.it) (WeeChat 3.0.1)
2021-06-18 07:06:32 <dminuoso> I almost feel like this should be encodable as a fixed point type, but I cant figure out how
2021-06-18 07:06:54 <dminuoso> (i.e. the children of NwD must be UsDC, and the children of UsDC must be NwD)
2021-06-18 07:07:05 × chrysanthematic quits (~chrysanth@82.2.21.4) (Quit: chrysanthematic)
2021-06-18 07:12:27 → yoctocell joins (~yoctocell@h87-96-130-155.cust.a3fiber.se)
2021-06-18 07:12:31 → BosonCollider joins (~olofs@90-227-86-119-no542.tbcn.telia.com)
2021-06-18 07:12:48 × tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz)
2021-06-18 07:14:18 → zeenk joins (~zeenk@82.76.113.130)
2021-06-18 07:14:21 × boxscape quits (~boxscape@user/boxscape) (Quit: Connection closed)
2021-06-18 07:16:41 × hexeme quits (~hexeme@user/hexeme) (Remote host closed the connection)
2021-06-18 07:17:00 → hexeme joins (~hexeme@user/hexeme)
2021-06-18 07:20:17 <hololeap> dminuoso: I don't see a way to do that, unless you want to get into type families and a type-level tag
2021-06-18 07:21:27 × phanf quits (~phanf@226.148.192.35.bc.googleusercontent.com) (Quit: leaving)
2021-06-18 07:21:47 → jenkems joins (~jenkems@226.148.192.35.bc.googleusercontent.com)
2021-06-18 07:22:19 → ddellacosta joins (~ddellacos@86.106.121.100)
2021-06-18 07:22:51 × beka quits (~beka@104-244-27-23.static.monkeybrains.net) (Ping timeout: 272 seconds)
2021-06-18 07:23:51 → jumper149 joins (~jumper149@80.240.31.34)
2021-06-18 07:26:32 <hololeap> even then, it doesn't seem reasonable
2021-06-18 07:27:09 × ddellacosta quits (~ddellacos@86.106.121.100) (Ping timeout: 268 seconds)
2021-06-18 07:28:52 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
2021-06-18 07:29:10 → ChaiTRex joins (~ChaiTRex@user/chaitrex)
2021-06-18 07:30:20 <kuribas> it's easy if you don't want to enforce the invariant
2021-06-18 07:30:39 <dminuoso> Sure, I can just encode it as `Tree (Either NwD UsDC)` then.
2021-06-18 07:31:07 <hololeap> the mutually-recursive method seems best to me
2021-06-18 07:31:36 <dminuoso> hololeap: Yeah I began to suspect as much.
2021-06-18 07:32:51 × lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
2021-06-18 07:32:58 → hendursa1 joins (~weechat@user/hendursaga)
2021-06-18 07:33:25 <kuribas> otherwise not possible. You want to constrain the types on value level, which implies some kind of dependent types.
2021-06-18 07:35:47 <hololeap> it might be possible with a GADT holding a type level list of tags and some kind of constraint that makes sure it's in the proper order, but that's way too much complexity
2021-06-18 07:36:45 tomsmeding thinks of a red-black tree
2021-06-18 07:37:47 <dminuoso> tomsmeding: Without the balancing. ;)
2021-06-18 07:37:51 <kuribas> hololeap: how can a GADT check value level information? The "levels" information is not available on type level.
2021-06-18 07:37:52 <tomsmeding> :p
2021-06-18 07:38:01 → chele joins (~chele@user/chele)
2021-06-18 07:39:15 <dminuoso> hololeap: Mmm, what about a non-regular data type?
2021-06-18 07:39:23 <dminuoso> Naively something like:
2021-06-18 07:39:31 <kuribas> perhaps it could have worked if the tree was in recursion-scheme style.
2021-06-18 07:40:36 <dminuoso> data Tree n a = Node a [Tree (Succ n) a]
2021-06-18 07:41:13 <kuribas> data Tree a b = Node { rootLabel :: a, subForest :: [b a] }
2021-06-18 07:41:14 <dminuoso> Or rather a type family that just flips between lifted 'L and 'R `data D = L | R`
2021-06-18 07:41:41 <dminuoso> kuribas: that's what I was wondering about initially
2021-06-18 07:42:03 <dminuoso> but this is not trivial recursion anymore
2021-06-18 07:43:23 <tomsmeding> note that for `type family Flip d where Flip 'L = 'R ; Flip 'R = 'L` GHC cannot prove that `Flip (Flip d) ~ d`
2021-06-18 07:44:33 <tomsmeding> re fixed point type: yes if you take the fixed point of `data Node2 f = Node2 NwD [(UsDC, [f])]` :p
2021-06-18 07:44:44 <dminuoso> tomsmeding: Mmm, I guess Id need an SMT plugged into the type checker for that?
2021-06-18 07:44:51 <dminuoso> *SMT solver
2021-06-18 07:45:13 <tomsmeding> or `believeme :: Flip (Flip d) :~: d ; believeme = unsafeCoerce Refl` ;)
2021-06-18 07:45:19 <tomsmeding> which is what I did
2021-06-18 07:45:28 <dminuoso> tomsmeding: interesting, re Node2: I think I can actually do that!
2021-06-18 07:45:39 <dminuoso> Each tree ends with UsDC, so this seems even better.
2021-06-18 07:45:46 <tomsmeding> it's a kind of weird representation of such a tree though, in my opinion
2021-06-18 07:45:48 <tomsmeding> but it works
2021-06-18 07:46:00 → hughjfchen joins (~hughjfche@vmi556545.contaboserver.net)
2021-06-18 07:46:00 <hololeap> kuribas: it wouldn't be checking value level info. it would be pushing the NwD and UsDC tags to the type level, which would mean that you would be checking a tree of tags to ensure proper order using a type family and a constraint. it would be ugly
2021-06-18 07:46:18 × hughjfchen quits (~hughjfche@vmi556545.contaboserver.net) (Remote host closed the connection)
2021-06-18 07:46:53 × BosonCollider quits (~olofs@90-227-86-119-no542.tbcn.telia.com) (Ping timeout: 268 seconds)
2021-06-18 07:46:55 <kuribas> dminuoso: newtype Even a = Even (Tree Odd a); newtype Odd a = Odd (Tree Even a);
2021-06-18 07:48:43 <kuribas> dminuoso: not sure what you get out of this though...
2021-06-18 07:48:49 <dminuoso> Yeah that's what hololeap suggested with a mutually recursive data type
2021-06-18 07:49:13 <kuribas> but this requires a functorial encoding
2021-06-18 07:49:27 <dminuoso> Though tomsmeding's encoding that cute advantage of being uniform as well as guaranteeding that each branch ends with UsDC (a condition I didnt mention because it didnt occur to me to encode this too)
2021-06-18 07:49:44 <dminuoso> guaranteeding.
2021-06-18 07:49:44 <tomsmeding> yeah I would go either with the plain, simple, mutually recursive approach, or if I really wanted the node constructor to be the same always, perhaps use that Succ trick with a type family that defines the tag on each level (and even whether the tree can terminate there)
2021-06-18 07:49:57 <tomsmeding> yes
2021-06-18 07:50:06 <kuribas> simple is always better IMO
2021-06-18 07:50:37 <tomsmeding> you can also encode the ends-with-UsDC requirement using the simple mutually recursive approach
2021-06-18 07:50:44 × ukari quits (~ukari@user/ukari) (Remote host closed the connection)
2021-06-18 07:50:56 <hololeap> well, not exactly. I was suggesting `data Even a = Even a [Odd a]` and `data Odd a = Odd a [Even a]`
2021-06-18 07:51:08 <tomsmeding> data A = A NwD (NonEmpty B) ; data B = B UsDC [A]
2021-06-18 07:51:11 → ukari joins (~ukari@user/ukari)
2021-06-18 07:51:26 → dunkeln joins (~dunkeln@94.129.65.28)
←Prev  Next→
Page 1 .. 520 521 522 523 524 525 526 527 528 529 530 .. 18005

All times are in UTC.