Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 986 987 988 989 990 991 992 993 994 995 996 .. 5022
— 502,152 events total
2020-11-01 11:42:25 <merijn> PerseusPlease: Oh!
2020-11-01 11:42:40 <merijn> PerseusPlease: That's because the pragma only enables it in the file, *not* in ghci itself :p
2020-11-01 11:42:50 <merijn> PerseusPlease: Use ":seti -XFlexibleContexts"
2020-11-01 11:42:57 <PerseusPlease> ahhhhhhhh...!
2020-11-01 11:43:02 <PerseusPlease> that's the magic
2020-11-01 11:43:19 <PerseusPlease> I tried {-# LANGUAGE FlexibleContexts #-}
2020-11-01 11:43:31 <merijn> Yeah, that doesn't work in ghci
2020-11-01 11:44:02 × pjb quits (~t@2a01cb04063ec5000c3dc2e28b3d9ccb.ipv6.abo.wanadoo.fr) (Ping timeout: 260 seconds)
2020-11-01 11:44:05 → drbean joins (~drbean@TC210-63-209-219.static.apol.com.tw)
2020-11-01 11:45:02 × sam___ quits (~sam@49.152.205.77.rev.sfr.net) (Ping timeout: 264 seconds)
2020-11-01 11:45:22 → florian_ joins (~florian@2a01:e35:2fe9:ecb0:bc5c:10ad:bdba:b477)
2020-11-01 11:46:38 → sam___ joins (~sam@4.196.204.77.rev.sfr.net)
2020-11-01 11:47:27 → ubert joins (~Thunderbi@p200300ecdf1e539fe6b318fffe838f33.dip0.t-ipconnect.de)
2020-11-01 11:52:04 → thir joins (~thir@p200300f27f0b7e00f4e9381c2bf90854.dip0.t-ipconnect.de)
2020-11-01 11:52:42 → jesee joins (~jesee@116.30.192.63)
2020-11-01 11:52:49 <florian_> Hi there ! Do you have any opinion about Agda ?!
2020-11-01 11:54:17 <__monty__> florian_: It's cool stuff.
2020-11-01 11:56:04 <florian_> monty : So do you use it ? and in which context do you use it ?
2020-11-01 11:56:15 → pjb joins (~t@2a01cb04063ec5002c0fc7d86fb8e728.ipv6.abo.wanadoo.fr)
2020-11-01 11:56:25 → jedws joins (~jedws@101.184.150.81)
2020-11-01 11:57:15 × jesee quits (~jesee@116.30.192.63) (Quit: Leaving)
2020-11-01 11:57:32 <__monty__> Not anymore, basically just took a look at it. It's viable as a way to do computer checked proofs.
2020-11-01 11:58:03 <__monty__> It's interesting for dependent types and for its syntax.
2020-11-01 11:58:04 × acidjnk_new quits (~acidjnk@p200300d0c7226044298aa97eef668aef.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-11-01 11:58:40 × Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection)
2020-11-01 11:58:54 → nschoe joins (~quassel@2a01:e0a:3c4:c7b0:c059:9ac8:a690:3133)
2020-11-01 11:59:24 × thir quits (~thir@p200300f27f0b7e00f4e9381c2bf90854.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-11-01 12:00:01 × creffett|irssi quits (~creffett|@195.206.169.184) ()
2020-11-01 12:00:06 → Chi1thangoo joins (~Chi1thang@87.112.60.168)
2020-11-01 12:03:05 → Varis joins (~Tadas@unaffiliated/varis)
2020-11-01 12:03:11 → britva joins (~britva@2a02:aa13:7240:2980:fc63:822e:7d74:772d)
2020-11-01 12:05:18 × brisbin quits (~patrick@pool-173-49-158-4.phlapa.fios.verizon.net) (Ping timeout: 260 seconds)
2020-11-01 12:05:24 × ubert quits (~Thunderbi@p200300ecdf1e539fe6b318fffe838f33.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2020-11-01 12:05:42 × jedws quits (~jedws@101.184.150.81) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-01 12:06:13 → dhil joins (~dhil@195.213.192.85)
2020-11-01 12:07:50 × petersen quits (~petersen@redhat/juhp) (Ping timeout: 264 seconds)
2020-11-01 12:07:57 → brisbin joins (~patrick@pool-173-49-158-4.phlapa.fios.verizon.net)
2020-11-01 12:09:49 × chaosmasttter quits (~chaosmast@p200300c4a72dee01c4c235ce0df4f033.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2020-11-01 12:10:01 <florian_> Do you see any value to use Agda to dev a game or application ?
2020-11-01 12:12:10 × Guest_47 quits (54b72aa9@p54b72aa9.dip0.t-ipconnect.de) (Remote host closed the connection)
2020-11-01 12:13:26 <akegalj> florian_: I think Idris is orianted more to suite that niche
2020-11-01 12:13:55 × cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 2.9)
2020-11-01 12:15:41 <__monty__> florian_: It would be a really cool project. But Agda's implementation is really not ready to produce performant code, at least last time I looked at it. Idris is kind of an Agda with a practical implementation but slightly less interesting and currently in flux because Idris 2 will be so different.
2020-11-01 12:17:06 × Nachtgespenst quits (~user@unaffiliated/siracusa) (Quit: Bye!)
2020-11-01 12:18:02 × nschoe quits (~quassel@2a01:e0a:3c4:c7b0:c059:9ac8:a690:3133) (Ping timeout: 264 seconds)
2020-11-01 12:19:07 <maerwald> Agda and game development?
2020-11-01 12:19:40 → Tops2 joins (~Tobias@dyndsl-095-033-023-063.ewe-ip-backbone.de)
2020-11-01 12:19:41 <maerwald> are you gonna write an entire ecosystem of game dev libraries from scratch? :D
2020-11-01 12:19:58 <akegalj> Also, my impression is that Agda's comunity is more focused on proof checking. As a result, Agda contains a lot of libraries to serve that goal. I don't think many people experimented with agda and game dev
2020-11-01 12:20:00 → solonarv joins (~solonarv@astrasbourg-653-1-117-122.w90-33.abo.wanadoo.fr)
2020-11-01 12:20:35 → dansho_ joins (~dansho@ip68-108-167-185.lv.lv.cox.net)
2020-11-01 12:20:48 → nhandler1 joins (~nhandler@185.204.1.185)
2020-11-01 12:20:50 <__monty__> I did a tiny experiment to see if using dependent types to make it impossible to design impossible levels could work.
2020-11-01 12:20:53 <int-e> Hmm, a "game" can be so many things.
2020-11-01 12:21:18 <__monty__> Wouldn't call it game dev by any stretch of the imagination though.
2020-11-01 12:21:20 <int-e> . o O ( Minesweeper )
2020-11-01 12:21:31 <akegalj> or chess
2020-11-01 12:22:13 <florian_> monty : Ok so Agda give a huge Type system that can be really interesting for an game or app, but the efficiency of the implementation is not good enough for that ? ( is want you try to said ? )
2020-11-01 12:22:57 <florian_> maerwald : yes
2020-11-01 12:23:05 <__monty__> florian_: Yes, unless you have the resources to develop a compiler and library ecosystem, Agda isn't a practical choice as the implementation language.
2020-11-01 12:23:11 <akegalj> florian_: If it some turn based game, then it might work out
2020-11-01 12:23:50 <__monty__> If it's just for a hobby project though, I'd say it'd be way more interesting than writing it in python or something.
2020-11-01 12:24:14 <int-e> It might be an interesting experiment... but what practical benefit do you expect?
2020-11-01 12:24:42 <__monty__> Enlightenment, obviously : )
2020-11-01 12:25:10 <int-e> __monty__: I get that, but what practical benefit do you expect. :-P
2020-11-01 12:25:44 → alp joins (~alp@2a01:e0a:58b:4920:89f1:ba96:ddf:92c2)
2020-11-01 12:26:10 <int-e> (I honestly think that the "experiment" part covers the potential enlightenment.)
2020-11-01 12:26:30 <maerwald> florian_: let me know when you've completed your first game in Agda
2020-11-01 12:27:45 <florian_> int-e : build stuff in a really elegant way and have a proof that your logic system do what you expect, no ?
2020-11-01 12:27:49 <int-e> Hmm, is "the incredible proof machine" a game? :)
2020-11-01 12:27:51 ski . o O ( "The Next Mainstream Programming Languages: A Game Developers's Perspective" (slides) by Tim Sweeney in 2005 at <http://www.st.cs.uni-saarland.de/edu/seminare/2005/advanced-fp/docs/sweeny.pdf> )
2020-11-01 12:28:51 <florian_> maerwald : haha why ?
2020-11-01 12:29:20 → Franciman joins (~francesco@host-79-36-167-172.retail.telecomitalia.it)
2020-11-01 12:30:10 → ahmr88 joins (~ahmr88@cpc85006-haye22-2-0-cust131.17-4.cable.virginm.net)
2020-11-01 12:30:31 <ski> (section from page 27 mentions dependent types, a bit)
2020-11-01 12:31:05 × brisbin quits (~patrick@pool-173-49-158-4.phlapa.fios.verizon.net) (Ping timeout: 240 seconds)
2020-11-01 12:31:16 <int-e> haha, 30fps@720p
2020-11-01 12:31:17 <florian_> ski : thanks a lot ! It's seems really interesting !
2020-11-01 12:32:07 <ski> Carmack has also talked a bit about functional programming, from a game programming perspective
2020-11-01 12:32:23 <__monty__> Yeah, that's a good talk.
2020-11-01 12:32:58 <__monty__> florian_: It'd be a lot more practical to do an implementation and a model of your logic in either a proof assistant or a model checker.
2020-11-01 12:34:01 <int-e> ski: is that 27 hex... (ouch)
2020-11-01 12:35:36 <int-e> But he uses "dependently-typed" as a proxy for a ranged integer type, which is a rather narrow extension of the type system. And I suspect he wants the compiler to infer the ranges, rather than the programmer to write them, most of the time? Hard to say.
2020-11-01 12:35:48 <florian_> monty : Because Agda is not a proof assistant ?
2020-11-01 12:36:23 <__monty__> florian_: It kinda is, the assistance is just fairly minimal, at least as compared to coq for example.
2020-11-01 12:36:27 → machinedgod joins (~machinedg@24.105.81.50)
2020-11-01 12:37:29 <maerwald> ski: you mean that one twitter post years ago?
2020-11-01 12:37:35 <ski> florian_ : <https://gamasutra.com/view/news/169296/Indepth_Functional_programming_in_C.php>,<https://www.youtube.com/watch?v=1PhArSujR_A>
2020-11-01 12:37:44 <ski> maerwald : no idea
2020-11-01 12:37:59 <__monty__> florian_: I'd recommend setting out to learn Agda and write something really simple, like tic-tac-toe or something. That'll probably give you enough insight into why no one here is going "Woohoo, yeah!!! Agda for games!"
2020-11-01 12:38:13 <florian_> monty : Ok, do you use coq ? Do know a language/software/system to do model checking ?
2020-11-01 12:38:28 <ski> int-e : "Reliability" section
2020-11-01 12:39:09 <__monty__> I don't, not enough time, I'd like to though. Model checker I'm most interested in is TLA+.
2020-11-01 12:39:44 <int-e> ski: Oh you mean the whole section, not the single slide.
2020-11-01 12:39:54 <ski> int-e : yes. it's not too fancy. but it does include Pi
2020-11-01 12:39:58 <ski> yep
2020-11-01 12:40:16 <int-e> I should figure out whether there are any dependently typed programming success stories out there.
2020-11-01 12:40:31 <florian_> ski : thanks I will check that !
2020-11-01 12:40:57 <__monty__> Well, compcert was certified using dependent types (coq), at least in part, no?
2020-11-01 12:41:07 <ski> (mind that Carmack isn't talking about dependent types, that i recall. but it could still be interesting)
←Prev  Next→
Page 1 .. 986 987 988 989 990 991 992 993 994 995 996 .. 5022

All times are in UTC.