Logs: liberachat/#haskell
| 2021-08-17 09:21:11 | × | adam1 quits (~adam@2001-b011-4007-0471-9e76-5e8f-4259-c5af.dynamic-ip6.hinet.net) (Quit: WeeChat 3.2) |
| 2021-08-17 09:21:33 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-08-17 09:21:46 | → | obs\ joins (~obscur1ty@156.192.222.172) |
| 2021-08-17 09:21:46 | × | obs\ quits (~obscur1ty@156.192.222.172) (Changing host) |
| 2021-08-17 09:21:46 | → | obs\ joins (~obscur1ty@user/obs/x-5924898) |
| 2021-08-17 09:23:47 | × | obscur1ty quits (~obscur1ty@user/obs/x-5924898) (Ping timeout: 245 seconds) |
| 2021-08-17 09:24:13 | → | gambpang joins (~ian@207.181.230.156) |
| 2021-08-17 09:25:17 | × | hendursa1 quits (~weechat@user/hendursaga) (Quit: hendursa1) |
| 2021-08-17 09:25:21 | × | obs\ quits (~obscur1ty@user/obs/x-5924898) (Read error: Connection reset by peer) |
| 2021-08-17 09:25:28 | → | obs\ joins (~obscur1ty@156.192.180.119) |
| 2021-08-17 09:25:28 | × | obs\ quits (~obscur1ty@156.192.180.119) (Changing host) |
| 2021-08-17 09:25:28 | → | obs\ joins (~obscur1ty@user/obs/x-5924898) |
| 2021-08-17 09:25:46 | → | hendursaga joins (~weechat@user/hendursaga) |
| 2021-08-17 09:31:52 | → | trevor joins (uid389732@id-389732.tooting.irccloud.com) |
| 2021-08-17 09:33:52 | ← | idf parts (~idf@198.23.223.146) (Using Circe, the loveliest of all IRC clients) |
| 2021-08-17 09:37:39 | × | benin036932 quits (~benin@106.198.88.152) (Quit: Ping timeout (120 seconds)) |
| 2021-08-17 09:38:47 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 245 seconds) |
| 2021-08-17 09:40:50 | → | oxide joins (~lambda@user/oxide) |
| 2021-08-17 09:42:31 | → | idf joins (~idf@198.23.223.146) |
| 2021-08-17 09:43:12 | → | jtomas joins (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) |
| 2021-08-17 09:43:16 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 09:45:58 | <kuribas> | which logic language would you recommend? I'd like one which has a good IDE (or emacs), and (optional) automated proofs. Export to haskell or other FP languages would be nice. |
| 2021-08-17 09:46:39 | <kuribas> | I looked at idris, but proving in idris feels like a secondary feature. |
| 2021-08-17 09:47:11 | <opqdonut> | logic language usually refers to logic programming a la prolog. are you looking for a proof system instead? |
| 2021-08-17 09:47:28 | <opqdonut> | aka proof assistant |
| 2021-08-17 09:47:39 | <opqdonut> | coq is fairly popular and has a nice emacs mode |
| 2021-08-17 09:48:05 | <opqdonut> | isabelle is another notable one, but I don't have experience with it |
| 2021-08-17 09:49:53 | → | aarvar joins (~aaron@2601:602:a080:fa0:417e:358b:8f59:9c9) |
| 2021-08-17 09:50:19 | <oak-> | Haskell also has the Liquid Haskell |
| 2021-08-17 09:50:21 | → | chomwitt joins (~chomwitt@2a02:587:dc0c:e200:12c3:7bff:fe6d:d374) |
| 2021-08-17 09:52:57 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-08-17 09:53:24 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2021-08-17 09:58:21 | × | gambpang quits (~ian@207.181.230.156) (Ping timeout: 268 seconds) |
| 2021-08-17 09:59:09 | → | benin036932 joins (~benin@106.198.88.152) |
| 2021-08-17 10:08:18 | <kuribas> | opqdonut: right, proof language :) |
| 2021-08-17 10:08:39 | <kuribas> | oak-: what I don't like about liquid haskell is that it doesn't encode bounds. |
| 2021-08-17 10:08:49 | <kuribas> | For example, it treats Int as an integer, which it isn't! |
| 2021-08-17 10:08:59 | → | dschrempf joins (~dominik@2a01-036d-0118-a2d1-6956-051d-7043-4e79.pool6.digikabel.hu) |
| 2021-08-17 10:09:10 | <kuribas> | opqdonut: and agda or lean? |
| 2021-08-17 10:11:00 | → | mousey joins (~skymouse@gateway/tor-sasl/mousey) |
| 2021-08-17 10:11:51 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 10:12:01 | <opqdonut> | kuribas: agda is definitely more programming-oriented with not that much proof automation |
| 2021-08-17 10:12:08 | <opqdonut> | lean I've heard of but haven't tried |
| 2021-08-17 10:13:25 | <kuribas> | opqdonut: I saw they made a proof of some complicated theorem (which took months). That's quite impressive. |
| 2021-08-17 10:13:40 | <kuribas> | Maybe it's more for proving math, rather than proving programs correct. |
| 2021-08-17 10:13:42 | <kuribas> | ? |
| 2021-08-17 10:14:22 | <opqdonut> | yeah I think isabelle and lean are more in the math camp, coq is kinda in the middle |
| 2021-08-17 10:14:41 | <opqdonut> | you can write some code in coq, prove it correct, and then have coq output haskell code |
| 2021-08-17 10:14:57 | <opqdonut> | haven't done that myself, just worked through some type theory stuff in coq |
| 2021-08-17 10:15:12 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-08-17 10:15:28 | <opqdonut> | you'll probably find more advice from somebody more experienced than me, but that's my two cents :) |
| 2021-08-17 10:17:16 | <kuribas> | oh, and there's f star, which exports to ocaml and f#, but not haskell. |
| 2021-08-17 10:17:54 | × | nrl^ quits (~nrl@209.65.131.194) (Remote host closed the connection) |
| 2021-08-17 10:23:37 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-08-17 10:25:01 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-17 10:25:05 | → | pbrisbin joins (~patrick@pool-108-16-214-93.phlapa.fios.verizon.net) |
| 2021-08-17 10:26:43 | <kuribas> | opqdonut: agda has this: https://agda.readthedocs.io/en/v2.5.3/tools/auto.html |
| 2021-08-17 10:26:52 | <kuribas> | opqdonut: maybe it's not ver sofisticated? |
| 2021-08-17 10:27:42 | <opqdonut> | yeah that's mostly for single holes in a proof |
| 2021-08-17 10:28:42 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-08-17 10:29:15 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 10:30:10 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-08-17 10:30:13 | × | dschrempf quits (~dominik@2a01-036d-0118-a2d1-6956-051d-7043-4e79.pool6.digikabel.hu) (Ping timeout: 258 seconds) |
| 2021-08-17 10:30:52 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-17 10:31:29 | <kuribas> | "Another mechanism for proof automation is proof search action in emacs mode. It enumerates possible proof terms (limited to 5 seconds), and if one of the terms fits the specification, it will be put in the meta variable where the action is invoked. " |
| 2021-08-17 10:31:46 | <kuribas> | https://en.wikipedia.org/wiki/Agda_(programming_language)#Proof_automation |
| 2021-08-17 10:35:27 | × | chomwitt quits (~chomwitt@2a02:587:dc0c:e200:12c3:7bff:fe6d:d374) (Ping timeout: 245 seconds) |
| 2021-08-17 10:35:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 2021-08-17 10:36:16 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-17 10:37:24 | × | tcard_ quits (~tcard@p2307053-ipngn17101hodogaya.kanagawa.ocn.ne.jp) (Quit: Leaving) |
| 2021-08-17 10:40:07 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 10:43:36 | → | tcard joins (~tcard@p2307053-ipngn17101hodogaya.kanagawa.ocn.ne.jp) |
| 2021-08-17 10:48:47 | × | azeem quits (~azeem@dynamic-adsl-94-34-33-6.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-08-17 10:50:09 | → | azeem joins (~azeem@dynamic-adsl-94-34-33-6.clienti.tiscali.it) |
| 2021-08-17 10:57:07 | → | dsrt^ joins (~dsrt@209.65.131.194) |
| 2021-08-17 10:59:13 | × | mousey quits (~skymouse@gateway/tor-sasl/mousey) (Ping timeout: 244 seconds) |
| 2021-08-17 11:00:12 | × | burnside_ quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-08-17 11:00:57 | → | alx741 joins (~alx741@181.196.68.125) |
| 2021-08-17 11:02:24 | → | fhutty14 joins (~fhutty14@c83-252-75-55.bredband.tele2.se) |
| 2021-08-17 11:03:21 | → | skykanin joins (~skykanin@115.81-166-221.customer.lyse.net) |
| 2021-08-17 11:08:10 | × | pbrisbin quits (~patrick@pool-108-16-214-93.phlapa.fios.verizon.net) (Ping timeout: 240 seconds) |
| 2021-08-17 11:09:25 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.2) |
| 2021-08-17 11:12:31 | trevor | is now known as rovert |
| 2021-08-17 11:15:45 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 11:22:10 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 240 seconds) |
| 2021-08-17 11:22:14 | → | cfricke joins (~cfricke@user/cfricke) |
| 2021-08-17 11:22:39 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-17 11:26:32 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 268 seconds) |
| 2021-08-17 11:27:32 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 245 seconds) |
| 2021-08-17 11:28:14 | → | dschrempf joins (~dominik@2a01-036d-0118-a2d1-e318-72ef-8701-cb8b.pool6.digikabel.hu) |
| 2021-08-17 11:29:43 | → | chisui joins (~chisui@200116b864e3ed0025ab38eae95cca2d.dip.versatel-1u1.de) |
| 2021-08-17 11:30:53 | <chisui> | Hey, what is a good current sound library for haskell. There are some listed on the wiki, but the articles where last updated in 2010. |
| 2021-08-17 11:31:41 | <jophish> | previously I've used the sdl audio bindings |
| 2021-08-17 11:32:56 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 11:35:10 | × | aarvar quits (~aaron@2601:602:a080:fa0:417e:358b:8f59:9c9) (Ping timeout: 240 seconds) |
| 2021-08-17 11:36:10 | <chisui> | jophish: Thanks, do you remember which package exactly you used? There are several on hackage |
| 2021-08-17 11:36:21 | <hpc> | i once used synthesizer-alsa to build up sounds from nothing - it was fun to use but i didn't get very far into it |
| 2021-08-17 11:36:36 | <jophish> | probably https://hackage.haskell.org/package/sdl2-mixer |
| 2021-08-17 11:37:26 | <jophish> | oh, sorry https://hackage.haskell.org/package/sdl2 |
| 2021-08-17 11:37:30 | <jophish> | that has SDL.Audio |
All times are in UTC.