Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 .. 5022
— 502,152 events total
2020-11-19 12:47:59 <boxscape> actually is ordered). If you want to delete an element in that list, you'll need a proof that less-than is transitive, as e.g. if you have [a,b,c] and want to delete b, you'll need to somehow construct a proof that a<c to get a new ordered list
2020-11-19 12:48:56 <dminuoso> Makes sense
2020-11-19 12:49:18 <dminuoso> So providing this proof is just to be able to re-construct this provably ordered list after the operation
2020-11-19 12:49:23 × gxt quits (~gxt@gateway/tor-sasl/gxt) (Ping timeout: 240 seconds)
2020-11-19 12:49:24 <boxscape> right
2020-11-19 12:49:39 <dminuoso> And the value is, you have some provable assurance the ordering is preserved by all operations
2020-11-19 12:49:46 <boxscape> yes
2020-11-19 12:50:24 <dminuoso> (in the absence of shortcircuiting the proof with bottom, of course)
2020-11-19 12:50:34 × p0a quits (~user@unaffiliated/p0a) (Quit: bye)
2020-11-19 12:50:45 <boxscape> right, though at least you can be sure that if your program *does* produce a result, it's a correct result
2020-11-19 12:51:07 <dminuoso> well that depends though, if the proof of transitivity is just bottom.. ?
2020-11-19 12:51:13 <dminuoso> It has to be runnable code
2020-11-19 12:51:21 <Boomerang> We use Refl very often at work when writing circuits in Clash. Clash uses type level Nat everywhere, it's often useful to choose which sub-circuit to use depending on the type
2020-11-19 12:51:59 <boxscape> right, it's still run to construct the actual proof object. Richard Eisenberg actually suggested in his thesis to replace equality proofs with unsafeCoerce Refl via a rewrite rule if you're sure they're total, for performance's sake
2020-11-19 12:52:10 → gxt joins (~gxt@gateway/tor-sasl/gxt)
2020-11-19 12:53:24 <dminuoso> Ah right, because Refl still has a runtime representation
2020-11-19 12:53:31 <boxscape> yeah
2020-11-19 12:59:23 <boxscape> (Though you can't do this unsafeCoerce stuff with all proofs, because for less-than for example, proofs will typically have different run-time reprenentations depending on how large the difference between the two values is, at least for comparing data Nat = S Nat | Z)
2020-11-19 13:00:15 × shangxiao quits (~davids@101.181.159.140) (Quit: WeeChat 2.9)
2020-11-19 13:01:59 <boxscape> (that is, data (<) :: Nat -> Nat -> Type where ZltS :: Z < (S n); SltS :: n < m -> (S n) < (S m), so for example SltS (SltS (ZltS) :: 2 < 5)
2020-11-19 13:02:19 <boxscape> (I guess what matters there is actually the size of the first value, not the difference between them)
2020-11-19 13:02:30 × troydm quits (~troydm@unaffiliated/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset)
2020-11-19 13:02:36 × elliott__ quits (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 240 seconds)
2020-11-19 13:03:08 → elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net)
2020-11-19 13:03:11 → nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45)
2020-11-19 13:05:15 → acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net)
2020-11-19 13:07:41 → xacktm joins (xacktm@gateway/shell/panicbnc/x-fxbrslxxjjorsbbu)
2020-11-19 13:07:47 × kritzefitz quits (~kritzefit@fw-front.credativ.com) (Read error: Connection timed out)
2020-11-19 13:08:15 → n0042 joins (d055ed89@208.85.237.137)
2020-11-19 13:10:14 → urodna joins (~urodna@unaffiliated/urodna)
2020-11-19 13:12:47 → texasmynsted joins (~texasmyns@212.102.45.112)
2020-11-19 13:13:16 × valdyn quits (~valdyn@host-88-217-143-53.customer.m-online.net) (Ping timeout: 260 seconds)
2020-11-19 13:14:29 → geekosaur joins (82659a09@host154-009.vpn.uakron.edu)
2020-11-19 13:15:55 → christo joins (~chris@81.96.113.213)
2020-11-19 13:16:00 × jwynn6 quits (~jwynn6@050-088-122-078.res.spectrum.com) (Read error: Connection reset by peer)
2020-11-19 13:16:19 → jwynn6 joins (~jwynn6@050-088-122-078.res.spectrum.com)
2020-11-19 13:18:14 → tromp_ joins (~tromp@dhcp-077-249-230-040.chello.nl)
2020-11-19 13:18:15 × tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Read error: Connection reset by peer)
2020-11-19 13:21:47 × bitmapper quits (uid464869@gateway/web/irccloud.com/x-xpsufctbszodgohs) (Quit: Connection closed for inactivity)
2020-11-19 13:22:26 → troydm joins (~troydm@unaffiliated/troydm)
2020-11-19 13:22:36 × acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 265 seconds)
2020-11-19 13:24:45 × chalkmonster quits (~chalkmons@unaffiliated/chalkmonster) (Ping timeout: 240 seconds)
2020-11-19 13:24:57 → kritzefitz joins (~kritzefit@fw-front.credativ.com)
2020-11-19 13:31:30 → aarvar joins (~foewfoiew@50.35.43.33)
2020-11-19 13:31:36 × christo quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-11-19 13:32:47 → christo joins (~chris@81.96.113.213)
2020-11-19 13:32:57 → cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd)
2020-11-19 13:33:46 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-19 13:35:42 × n0042 quits (d055ed89@208.85.237.137) (Remote host closed the connection)
2020-11-19 13:38:46 × gnumonic_ quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Read error: Connection reset by peer)
2020-11-19 13:39:37 → n0042 joins (d055ed89@208.85.237.137)
2020-11-19 13:39:49 → LKoen joins (~LKoen@169.244.88.92.rev.sfr.net)
2020-11-19 13:40:00 hackage subG 0.4.1.0 - Some extension to the Foldable and Monoid classes. https://hackage.haskell.org/package/subG-0.4.1.0 (OleksandrZhabenko)
2020-11-19 13:40:22 <n0042> Are there any rules or guidelines for messing with the Lambdabot? That looks like fun but I don't want to break it or anything
2020-11-19 13:40:59 <Uniaika> don't try to form an emotional connection with it, you'll be disappointed
2020-11-19 13:41:21 <n0042> :O
2020-11-19 13:41:31 <boxscape> n0042 you may know this but if you want to mess with it without spamming #haskell, you can do so in DMs. If you do find a way to break it, seems like a great opportunity for a bug report
2020-11-19 13:41:34 <boxscape> @botsnack
2020-11-19 13:41:34 <lambdabot> :)
2020-11-19 13:41:36 <geekosaur> .oO { if you can break it, we did it wrong }
2020-11-19 13:41:36 <tdammers> I thought lambdabot was a "she"?
2020-11-19 13:42:08 <Uniaika> I don't have a habit of anthropomorphising bots
2020-11-19 13:42:10 <n0042> Thank you boxscape. That is a good tip
2020-11-19 13:42:25 <tdammers> ships are "she" too
2020-11-19 13:43:13 <Uniaika> tdammers: that's a maritime culture convention :P
2020-11-19 13:43:33 <boxscape> countries do, too
2020-11-19 13:43:42 <boxscape> s/do/are
2020-11-19 13:43:53 <Uniaika> is that so?
2020-11-19 13:44:18 <boxscape> yes, I mostly hear it in geopolitical commentary
2020-11-19 13:44:26 <boxscape> or cgpgrey's videos
2020-11-19 13:44:39 → nbloomf joins (~nbloomf@2600:1700:ad14:3020:2da3:37d0:5114:5834)
2020-11-19 13:46:07 <boxscape> ..or, actually, I think in geopolitical commentary I usually see the capital being used
2020-11-19 13:46:24 × cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Ping timeout: 260 seconds)
2020-11-19 13:46:40 <n0042> That's definitely a thing.
2020-11-19 13:46:41 <tdammers> Uniaika: if sailors can have weird traditions, why can't we
2020-11-19 13:47:24 <boxscape> because if you anthropomorphize lambdabot, you'll form emotional connections with it, and as we learned that means you'll be disappointed
2020-11-19 13:47:32 × wei2912 quits (~wei2912@unaffiliated/wei2912) (Remote host closed the connection)
2020-11-19 13:47:57 <ski> lambdabot was anthropomorphized as a she, rather long ago, yes
2020-11-19 13:48:06 <dminuoso> authoritatively?
2020-11-19 13:48:19 dminuoso didn't get the memo
2020-11-19 13:48:27 <n0042> What is the command to make Lambdabot evaluate an expression or list comprehension?
2020-11-19 13:48:47 <boxscape> > [ x | x <- [1..5] ]
2020-11-19 13:48:49 <lambdabot> [1,2,3,4,5]
2020-11-19 13:48:56 <ski> the South Park style avatar for lambdabot, chosen by voting in #haskell-blah, was definitely female
2020-11-19 13:48:59 <dminuoso> > fix error
2020-11-19 13:49:02 <lambdabot> "*Exception: *Exception: *Exception: *Exception: *Exception: *Exception: *Ex...
2020-11-19 13:49:03 → machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca)
2020-11-19 13:49:09 <boxscape> (a list comprehension is an expression fwiw)
2020-11-19 13:49:12 <Uniaika> ski: is that channel still alive?
2020-11-19 13:49:17 <boxscape> ish
2020-11-19 13:49:23 → __monty_1 joins (~toonn@unaffiliated/toonn)
2020-11-19 13:49:24 <boxscape> #haskell-offtopic is more popular
2020-11-19 13:49:34 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:2da3:37d0:5114:5834) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-19 13:49:36 <dminuoso> ski: Maybe we could have the Haskell Foundation make an announcement then, as their first official act.
2020-11-19 13:49:43 <dminuoso> It seems relevant.
2020-11-19 13:49:58 <Uniaika> hahaha
2020-11-19 13:50:05 × __monty__ quits (~toonn@unaffiliated/toonn) (Ping timeout: 240 seconds)
2020-11-19 13:50:05 <n0042> Excellent, thank you. I tried to do it without a space after the prompt, which is why it wasn't working.
2020-11-19 13:50:11 <ski> i'm not sure if the page where there were some South Park style avatars for some people on #haskell / #haskell-blah, is still available somewhere. the original link doesn't work anymore, at least
2020-11-19 13:51:08 ski idly recalls the `@vixen' command
←Prev  Next→
Page 1 .. 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 .. 5022

All times are in UTC.