Logs: freenode/#haskell
| 2020-10-10 09:45:04 | <dminuoso> | With the option of manual control, since you can just write an instance by hand if you wanted to. |
| 2020-10-10 09:45:12 | <ski> | i guess one alternative, depending, could be to define an alternative type, where the API operations are the data constructors, and then translate a value to that representation, prior to showing |
| 2020-10-10 09:45:27 | <ski> | (the showing being provided automatically by the system) |
| 2020-10-10 09:45:29 | <dminuoso> | But functions/IO/existentials/etc do bind GHCs hands |
| 2020-10-10 09:45:32 | <dminuoso> | *tie |
| 2020-10-10 09:46:02 | <dminuoso> | ski: Sure, so something like free monads rather? |
| 2020-10-10 09:46:11 | <dminuoso> | (in spirit) |
| 2020-10-10 09:46:19 | → | oldsk00l_ joins (~znc@ec2-18-130-254-135.eu-west-2.compute.amazonaws.com) |
| 2020-10-10 09:46:32 | <ski> | all the derived `Show' instances together would correspond to the standard printer, in the MLs, was rather the comparision i had in mind |
| 2020-10-10 09:47:19 | <ski> | well, this "free" representation would only be used, when you wanted to have an abstract data type |
| 2020-10-10 09:48:05 | × | oldsk00l quits (~znc@ec2-18-130-254-135.eu-west-2.compute.amazonaws.com) (Ping timeout: 240 seconds) |
| 2020-10-10 09:48:22 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 256 seconds) |
| 2020-10-10 09:48:46 | <ski> | (e.g. in Mercury, you explicitly declare when a data-type is to have any other than the structural equality (so that the data constructors no longer need to be injective, meaning that matching can, conceptually, give multiple alternative sets of bindings)) |
| 2020-10-10 09:50:28 | <dminuoso> | Mmm, how can matching give multiple alternative sets of bindings? |
| 2020-10-10 09:50:37 | <dminuoso> | Not sure I understand that |
| 2020-10-10 09:54:33 | <ski> | well, let's say `data Ratio a = a :% a'. you define `n0 :% d0 == n1 :% d1 = n0 * d1 == n1 * d0'. if you really mean this, then `(:%)' is not injective, since `1 :% 2 == 2 :% 4' is `True' |
| 2020-10-10 09:55:04 | → | kpyke joins (~kpyke@84.39.117.57) |
| 2020-10-10 09:55:17 | <ski> | so, conceptually, if you do `let f (n :% d) = ..n..d.. in f (1 :% 2)', you could bind `n = 1; d = 2', but you could just as well bind `n = 2; d = 4', or other choices |
| 2020-10-10 09:55:29 | → | kuribas joins (~user@ptr-25vy0i9duk6e6r75xae.18120a2.ip6.access.telenet.be) |
| 2020-10-10 09:56:35 | → | ClaudiusMaximus joins (~claude@198.123.199.146.dyn.plus.net) |
| 2020-10-10 09:56:58 | <dminuoso> | Ah I see |
| 2020-10-10 09:56:59 | <ski> | with this comes the proof obligation that if matching the input could produce both `n = n0; d = d0' and `n = n1; d = d1', then, you should prove that the body `..n0..d0..' is equal to the body `..n1..d1..', provided that you only know that `n0 * d1 == n1 * d0' is `True' |
| 2020-10-10 09:58:09 | → | shatriff joins (~vitaliish@88.155.112.235) |
| 2020-10-10 09:58:19 | <ski> | in Haskell, you have to think about this matters, on your own (or fail to do so), with no help from the implementation (since it doesn't know that you're defining a quotient type (having a user-defined equality), or perhaps a subtype, or a combination of the two) |
| 2020-10-10 09:58:47 | <ski> | while, in Mercury, the implementation is aware that your data constructors are not injective, and will flag your code as non-deterministic |
| 2020-10-10 09:58:48 | × | urdh quits (~urdh@unaffiliated/urdh) (Read error: Connection reset by peer) |
| 2020-10-10 09:59:08 | → | urdh joins (~urdh@unaffiliated/urdh) |
| 2020-10-10 09:59:17 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds) |
| 2020-10-10 09:59:48 | <ski> | you can't really prove to it that, at some point, the non-determinism doesn't matter, is "cancelled out". but you can promise to it, at that point, that that is the case (and that discharges the non-determinism that otherwise would taint every operation that calls the present one) |
| 2020-10-10 10:01:08 | <ski> | the reason why Mercury has to do this (if it wants to support quotient types (as represented via abstract data types), sanely), is because in Mercury, equality checking is more closely integrated with semantic equality. conceptually it's the same predicate there, unlike in Haskell, which distinguishes `==' from `=' |
| 2020-10-10 10:03:18 | <ski> | (from the POV of Haskell, `(==)' is just another type class method. the implementation doesn't really assume that it respects some laws that one'd expect equality to satisfy. while in Mercury, the implementation does rely on such laws) |
| 2020-10-10 10:04:22 | → | knupfer joins (~Thunderbi@200116b824272b00c07c84fffe7936f7.dip.versatel-1u1.de) |
| 2020-10-10 10:04:36 | → | knupfer1 joins (~Thunderbi@i59F7FF4B.versanet.de) |
| 2020-10-10 10:08:41 | × | qz quits (~quetzal@li272-85.members.linode.com) (Read error: Connection reset by peer) |
| 2020-10-10 10:08:57 | × | knupfer quits (~Thunderbi@200116b824272b00c07c84fffe7936f7.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 2020-10-10 10:08:58 | knupfer1 | is now known as knupfer |
| 2020-10-10 10:09:31 | → | mdunnio joins (~mdunnio@208.59.170.5) |
| 2020-10-10 10:12:28 | hackage | servant-docs-simple 0.3.0.0 - Generate endpoints overview for Servant API https://hackage.haskell.org/package/servant-docs-simple-0.3.0.0 (HolmuskTechTeam) |
| 2020-10-10 10:13:29 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) |
| 2020-10-10 10:13:45 | × | mdunnio quits (~mdunnio@208.59.170.5) (Ping timeout: 240 seconds) |
| 2020-10-10 10:13:51 | × | GyroW quits (~GyroW@unaffiliated/gyrow) (Quit: Someone ate my pie) |
| 2020-10-10 10:14:01 | → | GyroW joins (~GyroW@d54C03E98.access.telenet.be) |
| 2020-10-10 10:14:01 | × | GyroW quits (~GyroW@d54C03E98.access.telenet.be) (Changing host) |
| 2020-10-10 10:14:01 | → | GyroW joins (~GyroW@unaffiliated/gyrow) |
| 2020-10-10 10:14:56 | → | HaskellYogi joins (~vivekrama@49.207.201.29) |
| 2020-10-10 10:15:58 | <dminuoso> | ski: I guess its two fold since Haskell implementations to assume reflexivity and transitivity of (=) at least. |
| 2020-10-10 10:16:17 | → | qz joins (~quetzal@li272-85.members.linode.com) |
| 2020-10-10 10:18:49 | × | dcabrejas quits (bcd609cc@188.214.9.204) (Ping timeout: 245 seconds) |
| 2020-10-10 10:19:07 | × | shatriff quits (~vitaliish@88.155.112.235) (Ping timeout: 240 seconds) |
| 2020-10-10 10:21:33 | → | shatriff joins (~vitaliish@88.155.189.140) |
| 2020-10-10 10:22:30 | → | xerox_ joins (~xerox@unaffiliated/xerox) |
| 2020-10-10 10:23:37 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-10 10:25:21 | <kuribas> | ski: I was wondering, in dependently typed languages you could require class instances to come with proofs, and then have rewrite rules based on those proofs. |
| 2020-10-10 10:25:44 | <kuribas> | ski: it would allow for more optimizations. |
| 2020-10-10 10:28:02 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 2020-10-10 10:28:44 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 2020-10-10 10:29:01 | <ski> | dminuoso : library operations, yea. but not the language implementations themselves, afaik |
| 2020-10-10 10:29:02 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 2020-10-10 10:29:15 | <ski> | kuribas : yea .. possibly |
| 2020-10-10 10:29:50 | → | alp_ joins (~alp@2a01:e0a:58b:4920:8d6d:4e03:3914:cd97) |
| 2020-10-10 10:30:23 | × | ClaudiusMaximus quits (~claude@198.123.199.146.dyn.plus.net) (Changing host) |
| 2020-10-10 10:30:23 | → | ClaudiusMaximus joins (~claude@unaffiliated/claudiusmaximus) |
| 2020-10-10 10:30:35 | <ski> | (then, in HoTT, one could express quotient types with extra "equality constructors" of a data-type. and then, when defining a function, matching on inputs of that type, one'd also need to (forced by the type system, and exhaustiveness checker) prove the well-definedness condition exemplified above) |
| 2020-10-10 10:31:23 | → | snakemas1 joins (~snakemast@213.100.206.23) |
| 2020-10-10 10:31:41 | → | thir joins (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de) |
| 2020-10-10 10:36:05 | × | coot quits (~coot@37.30.49.218.nat.umts.dynamic.t-mobile.pl) (Ping timeout: 260 seconds) |
| 2020-10-10 10:36:22 | × | thir quits (~thir@p200300f27f02580060eb7dde324e54c8.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2020-10-10 10:36:23 | → | oisdk joins (~oisdk@2001:bb6:3329:d100:d4b4:3667:7218:633) |
| 2020-10-10 10:37:05 | × | HaskellYogi quits (~vivekrama@49.207.201.29) (Ping timeout: 240 seconds) |
| 2020-10-10 10:38:52 | × | rprije quits (~rprije@203.214.95.251) (Ping timeout: 256 seconds) |
| 2020-10-10 10:39:22 | → | HaskellYogi joins (~vivekrama@49.207.201.29) |
| 2020-10-10 10:40:45 | × | snakemas1 quits (~snakemast@213.100.206.23) (Ping timeout: 260 seconds) |
| 2020-10-10 10:43:18 | → | malook joins (~Thunderbi@5.82.111.189) |
| 2020-10-10 10:43:58 | × | HaskellYogi quits (~vivekrama@49.207.201.29) (Ping timeout: 260 seconds) |
| 2020-10-10 10:44:47 | → | HaskellYogi joins (~vivekrama@49.207.201.29) |
| 2020-10-10 10:46:13 | → | snakemas1 joins (~snakemast@213.100.206.23) |
| 2020-10-10 10:47:16 | × | HaskellYogi quits (~vivekrama@49.207.201.29) (Remote host closed the connection) |
| 2020-10-10 10:47:30 | → | HaskellYogi joins (~vivekrama@49.207.201.29) |
| 2020-10-10 10:50:58 | × | snakemas1 quits (~snakemast@213.100.206.23) (Ping timeout: 260 seconds) |
| 2020-10-10 10:51:06 | → | AlterEgo- joins (~ladew@124-198-158-163.dynamic.caiway.nl) |
| 2020-10-10 10:54:16 | → | burritoprogramme joins (5549a868@athedsl-286922.home.otenet.gr) |
| 2020-10-10 10:54:48 | <burritoprogramme> | exercises to do while learning haskell in uni? |
| 2020-10-10 10:54:56 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:a16f:75:586:b3b0) (Quit: cosimone) |
| 2020-10-10 10:55:22 | <no-n> | lift |
| 2020-10-10 10:55:38 | <no-n> | lift as much as possible |
| 2020-10-10 10:55:56 | <burritoprogramme> | :( |
| 2020-10-10 10:55:59 | <Rembane> | There are some good ones but I've forgotten the link. ski, do you know the command to the Stanford course? |
| 2020-10-10 10:56:07 | <burritoprogramme> | or eat borritos? |
| 2020-10-10 10:56:15 | <no-n> | yes |
| 2020-10-10 10:56:18 | <davve> | project euler |
| 2020-10-10 10:56:42 | <no-n> | lift burritos if you can |
| 2020-10-10 10:57:21 | <Rembane> | burritoprogramme: Lets start with this one: https://wiki.haskell.org/H-99:_Ninety-Nine_Haskell_Problems |
| 2020-10-10 10:57:39 | <davve> | ^ all the best students from my CS class did P.E excercies :P |
| 2020-10-10 10:58:09 | <davve> | good challenges |
| 2020-10-10 10:59:08 | <davve> | not haskell-specific in any way, but haskell is a good place to solve them and there are haskell solutions to everything |
| 2020-10-10 10:59:18 | <Squarism> | ghoulguy, hey. You dont happen to be around? I have a question about the addressing solution you proposed. |
| 2020-10-10 11:07:03 | × | alp_ quits (~alp@2a01:e0a:58b:4920:8d6d:4e03:3914:cd97) (Ping timeout: 272 seconds) |
| 2020-10-10 11:10:54 | → | xsperry joins (~as@unaffiliated/xsperry) |
| 2020-10-10 11:15:45 | → | jchia__ joins (~jchia@45.32.62.73) |
| 2020-10-10 11:16:46 | × | jchia__ quits (~jchia@45.32.62.73) (Remote host closed the connection) |
All times are in UTC.