Logs: liberachat/#haskell
| 2021-06-30 17:27:42 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-06-30 17:28:15 | <buddha> | Is writing algorithms in Haskell more `fun` in Haskell compared to Python? |
| 2021-06-30 17:28:39 | <dolio> | I think almost everything is more fun in Haskell. |
| 2021-06-30 17:28:42 | <dminuoso> | Not sure what answer you expect. Im sure if you asked that question flipped around in #python you'd get the opposite response. |
| 2021-06-30 17:28:44 | <raehik> | yes |
| 2021-06-30 17:28:50 | → | peterhil joins (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) |
| 2021-06-30 17:29:32 | <dminuoso> | There's probably more value in asking "what frustrates you about the language" than "do you like doing X in your language". :-) |
| 2021-06-30 17:29:35 | → | Pickchea joins (~private@user/pickchea) |
| 2021-06-30 17:30:06 | → | alx741 joins (~alx741@186.178.108.157) |
| 2021-06-30 17:30:54 | <monochrom> | Other people bolting on dependent typing on Haskell frustrates me about the language. But this uses the word "language" to refer to culture rather than syntax and semantics. |
| 2021-06-30 17:31:24 | <buddha> | I guess I'll have to find out myself. It's like learning Vim, you'll never know what's on the other side |
| 2021-06-30 17:31:38 | <dminuoso> | I find the lack of circular imports to be the most annoying thing in the Haskell language itself. |
| 2021-06-30 17:31:50 | <koala_man> | buddha: if you enjoy list comprehensions and map/filter/lambda, then yes, definitely |
| 2021-06-30 17:31:55 | <dminuoso> | Well. In GHC Haskell I should say. :-) |
| 2021-06-30 17:33:06 | <dminuoso> | buddha: One thing to keep in mind, that in a pure, non-strict and functional settings writing algorithms is usually very different. In fact, even the idiomatic data structures are different. So especially for newcomers to haskell, much of their previous experience can't be transferred directly.. at least in the beginning. |
| 2021-06-30 17:33:14 | → | Ariakenom joins (~Ariakenom@c83-255-154-140.bredband.tele2.se) |
| 2021-06-30 17:33:38 | <buddha> | dminuoso I have xp with elixir, that might help a bit |
| 2021-06-30 17:34:15 | <monochrom> | I think in retrospect circular importing was one of those things they thought "would be cool and SML does it, what can possibly go wrong" and it backfired. See, SML can do it because, and only because, handwritten interface files are required. And it shows, GHC supports it by requiring you to handwrite interface files again. |
| 2021-06-30 17:34:44 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-30 17:35:07 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 2021-06-30 17:36:13 | <dminuoso> | buddha: Some bits are similar yeah. Just like elixir, we also make a lot of use of pattern matching and case-of, there's also a bit of similarity in some elixir acros and the way we write code in Haskell. |
| 2021-06-30 17:36:57 | <dminuoso> | Amusingly, Haskell suffers from the same string/charlist issue that erlang/elixir has. :-) |
| 2021-06-30 17:37:09 | <dminuoso> | And I reckon it's for the same reasons as well |
| 2021-06-30 17:38:39 | → | ikex1 joins (~ash@user/ikex) |
| 2021-06-30 17:38:46 | × | ikex quits (ash@user/ikex) (Ping timeout: 252 seconds) |
| 2021-06-30 17:39:19 | ikex1 | is now known as ikex |
| 2021-06-30 17:40:06 | × | motherfsck quits (~motherfsc@user/motherfsck) (Remote host closed the connection) |
| 2021-06-30 17:41:15 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-30 17:41:43 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-30 17:41:52 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) |
| 2021-06-30 17:41:56 | <buddha> | is the `+` plus operator an example of operator overloading? |
| 2021-06-30 17:42:27 | <dminuoso> | Yes, though overloading is not tied to `operators`. |
| 2021-06-30 17:42:46 | <buddha> | it's just a function right? |
| 2021-06-30 17:43:02 | <dminuoso> | Well, its what we call a "class method" |
| 2021-06-30 17:43:34 | <eggplantade> | As far as notation goes, `+` is a function name, and it has different syntax because it uses operator symbols |
| 2021-06-30 17:43:39 | <dminuoso> | You can think of a class like protocols in elixir, perhaps. |
| 2021-06-30 17:44:15 | <dminuoso> | And we call "members" of that class methods. Note I intentionally avoided the term "function", because a method could also be an immediate value, though most of the time they are actual functions. |
| 2021-06-30 17:44:38 | <dminuoso> | (Our typeclasses are much richer than protocols, but it's a good initial approximation to get acquainted with them) |
| 2021-06-30 17:46:53 | × | amcleodca quits (~andy@user/amcleodca) (Remote host closed the connection) |
| 2021-06-30 17:48:56 | <qrpnxz> | dsal, right, I thought maybe you'd want like some kind of nonempty foldable, but all foldables have a toList anyway, then you can just turn that into a nonempty and to sconcat and it's the same, so sounds good! |
| 2021-06-30 17:49:58 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-30 17:51:05 | <dsal> | It doesn’t make sense to fold1 something that isn’t non-empty. The missing piece is some kind of NonEmptyFoldable which is basically semigroupoids |
| 2021-06-30 17:51:10 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-30 17:51:10 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2021-06-30 17:51:12 | → | norias joins (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) |
| 2021-06-30 17:51:44 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-06-30 17:52:43 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-30 17:57:42 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-06-30 17:58:51 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-30 17:59:20 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-06-30 18:00:24 | × | egoist quits (~egoist@186.235.82.105) (Ping timeout: 252 seconds) |
| 2021-06-30 18:01:34 | → | egoist joins (~egoist@186.235.80.194) |
| 2021-06-30 18:03:09 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 2021-06-30 18:06:57 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-30 18:07:44 | → | warnz joins (~warnz@2600:1700:77c0:5610:409d:bff0:fc58:d5c4) |
| 2021-06-30 18:09:09 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 2021-06-30 18:09:44 | × | fvr quits (uid503686@id-503686.highgate.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-06-30 18:10:18 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 240 seconds) |
| 2021-06-30 18:13:16 | × | waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Ping timeout: 256 seconds) |
| 2021-06-30 18:14:47 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) (Remote host closed the connection) |
| 2021-06-30 18:19:36 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 268 seconds) |
| 2021-06-30 18:20:22 | → | Bob_Esponja joins (~Bob_Espon@130.red-176-83-49.dynamicip.rima-tde.net) |
| 2021-06-30 18:22:19 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 2021-06-30 18:22:32 | × | Bob_Esponja quits (~Bob_Espon@130.red-176-83-49.dynamicip.rima-tde.net) (Read error: Connection reset by peer) |
| 2021-06-30 18:23:08 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2021-06-30 18:25:50 | × | shapr quits (~user@pool-108-28-144-11.washdc.fios.verizon.net) (Remote host closed the connection) |
| 2021-06-30 18:26:49 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-06-30 18:29:10 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 272 seconds) |
| 2021-06-30 18:29:32 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-06-30 18:29:52 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 2021-06-30 18:30:41 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-30 18:36:06 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-30 18:37:25 | → | Bob_Esponja joins (~Bob_Espon@130.red-176-83-49.dynamicip.rima-tde.net) |
| 2021-06-30 18:37:54 | × | Bob_Esponja quits (~Bob_Espon@130.red-176-83-49.dynamicip.rima-tde.net) (Read error: Connection reset by peer) |
| 2021-06-30 18:38:46 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Remote host closed the connection) |
| 2021-06-30 18:39:46 | → | Bob_Esponja joins (~Bob_Espon@130.red-176-83-49.dynamicip.rima-tde.net) |
| 2021-06-30 18:40:00 | × | Bob_Esponja quits (~Bob_Espon@130.red-176-83-49.dynamicip.rima-tde.net) (Read error: Connection reset by peer) |
| 2021-06-30 18:41:06 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-06-30 18:41:14 | → | shapr joins (~user@pool-108-28-144-11.washdc.fios.verizon.net) |
| 2021-06-30 18:46:27 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-30 18:46:46 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) |
| 2021-06-30 18:47:06 | × | benin0369 quits (~benin@183.82.205.231) (Ping timeout: 240 seconds) |
| 2021-06-30 18:47:51 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-06-30 18:53:12 | × | nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 2021-06-30 18:56:30 | <maerwald> | Inb4 "total prelude" |
| 2021-06-30 18:57:21 | × | buddha quits (~buddha@27.147.234.193) (Quit: Client closed) |
| 2021-06-30 18:59:38 | maerwald | shows the Idris/Agda door |
| 2021-06-30 19:01:56 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-06-30 19:03:43 | dunj4 | is now known as dunj |
| 2021-06-30 19:03:45 | dunj | is now known as dunj3 |
| 2021-06-30 19:10:33 | → | safinaskar joins (~safinaska@109-252-90-89.nat.spd-mgts.ru) |
| 2021-06-30 19:11:42 | <safinaskar> | it seems that GADTs are equivalent to logics. (I. e. values of GADTs are proofs). If one writes function from one GADT to another, then it is proof of morphism from one logic to another |
| 2021-06-30 19:12:04 | <safinaskar> | am i first to notice this? there surely should be posts about the same, please, give me them |
| 2021-06-30 19:12:36 | <Cale> | No, and in fact, that's how type theory started out in the first place |
| 2021-06-30 19:13:03 | <safinaskar> | ok, thanks |
| 2021-06-30 19:13:06 | <safinaskar> | give me links, please |
| 2021-06-30 19:13:10 | <Cale> | Not just terms of GADTs are proofs, but terms are proofs, and types are the propositions being proved |
| 2021-06-30 19:13:30 | <safinaskar> | Cale: of course |
| 2021-06-30 19:13:45 | <safinaskar> | Cale: but GADTs allow especially elegant formalism for logics |
| 2021-06-30 19:13:52 | <safinaskar> | also, if compiler compiles "\case{}", this proves that certain formula is not deducible in a logic |
All times are in UTC.