Logs: liberachat/#haskell
| 2021-06-23 13:58:10 | → | nerdypepper joins (~nerdypepp@user/nerdypepper) |
| 2021-06-23 13:58:44 | × | remexre quits (~nathan@user/remexre) (Read error: Connection reset by peer) |
| 2021-06-23 13:59:52 | × | smarton quits (~smarton@2a01:4f9:c010:4e92::1) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 2021-06-23 14:00:39 | → | DNH joins (~DNH@2a09:bac0:48::82b:7a06) |
| 2021-06-23 14:01:33 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:e846:fcb5:a54b:afb8) |
| 2021-06-23 14:02:29 | → | remexre joins (~nathan@user/remexre) |
| 2021-06-23 14:02:41 | → | smarton joins (~smarton@121407.xyz) |
| 2021-06-23 14:03:00 | × | jakzale quits (uid499518@id-499518.charlton.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-06-23 14:04:23 | → | sayola joins (~vekto@dslb-088-078-152-192.088.078.pools.vodafone-ip.de) |
| 2021-06-23 14:05:32 | → | trcc_ joins (~trcc@eduroam09.au.dk) |
| 2021-06-23 14:06:18 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:e846:fcb5:a54b:afb8) (Ping timeout: 264 seconds) |
| 2021-06-23 14:07:02 | → | safinaskar joins (~safinaska@109-252-90-89.nat.spd-mgts.ru) |
| 2021-06-23 14:07:06 | × | ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Ping timeout: 250 seconds) |
| 2021-06-23 14:07:17 | <safinaskar> | is it true that "forall a." always means "forall a :: Type."? |
| 2021-06-23 14:07:21 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 2021-06-23 14:08:50 | × | trcc quits (~trcc@users-1190.st.net.au.dk) (Ping timeout: 268 seconds) |
| 2021-06-23 14:10:03 | <lortabac> | safinaskar: no, sometimes a different kind can be infered |
| 2021-06-23 14:10:15 | <dminuoso> | % :set -XPolyKinds |
| 2021-06-23 14:10:15 | <yahb> | dminuoso: |
| 2021-06-23 14:10:16 | × | trcc_ quits (~trcc@eduroam09.au.dk) (Ping timeout: 265 seconds) |
| 2021-06-23 14:10:30 | <safinaskar> | lortabac: thanks |
| 2021-06-23 14:11:42 | → | fendor_ joins (~fendor@178.165.189.179.wireless.dyn.drei.com) |
| 2021-06-23 14:12:14 | <dminuoso> | % f :: forall a b. a -> Const a b; f = Const |
| 2021-06-23 14:12:14 | <yahb> | dminuoso: |
| 2021-06-23 14:12:16 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 2021-06-23 14:12:18 | <dminuoso> | % :t f -- safinaskar |
| 2021-06-23 14:12:18 | <yahb> | dminuoso: forall {k} {a} {b :: k}. a -> Const a b |
| 2021-06-23 14:13:49 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2021-06-23 14:14:17 | × | fendor quits (~fendor@178.115.129.107.wireless.dyn.drei.com) (Ping timeout: 258 seconds) |
| 2021-06-23 14:14:50 | fendor_ | is now known as fendor |
| 2021-06-23 14:15:03 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Ping timeout: 258 seconds) |
| 2021-06-23 14:15:05 | → | betelgeuse joins (~john2gb@94-225-47-8.access.telenet.be) |
| 2021-06-23 14:15:21 | ← | safinaskar parts (~safinaska@109-252-90-89.nat.spd-mgts.ru) () |
| 2021-06-23 14:19:05 | → | safinaskar joins (~safinaska@109-252-90-89.nat.spd-mgts.ru) |
| 2021-06-23 14:20:38 | <safinaskar> | is it true that "singletons" library is limited compared to hypothetical future dependent haskell (dh), because with singletons (as opposed to true dh) you cannot have types depending on runtime values? |
| 2021-06-23 14:21:57 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 258 seconds) |
| 2021-06-23 14:22:18 | → | jao joins (jao@gateway/vpn/protonvpn/jao) |
| 2021-06-23 14:22:18 | × | betelgeuse quits (~john2gb@94-225-47-8.access.telenet.be) (Read error: Connection reset by peer) |
| 2021-06-23 14:22:18 | → | jneira_ joins (~jneira_@131.red-79-155-1.dynamicip.rima-tde.net) |
| 2021-06-23 14:22:32 | → | hounded joins (~hounded@2603-7000-da43-eccc-0000-0000-0000-0cec.res6.spectrum.com) |
| 2021-06-23 14:22:39 | → | hounded_woodstoc joins (~hounded@2603-7000-da43-eccc-0000-0000-0000-0cec.res6.spectrum.com) |
| 2021-06-23 14:22:39 | × | hounded_woodstoc quits (~hounded@2603-7000-da43-eccc-0000-0000-0000-0cec.res6.spectrum.com) (Client Quit) |
| 2021-06-23 14:23:42 | <merijn> | "probably"? |
| 2021-06-23 14:23:52 | → | betelgeuse joins (~john2gb@94-225-47-8.access.telenet.be) |
| 2021-06-23 14:24:12 | <merijn> | It's also probably true that Dependent Haskell will always suck, even in the future |
| 2021-06-23 14:24:15 | × | Morrow quits (~Morrow@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 258 seconds) |
| 2021-06-23 14:24:18 | × | shapr quits (~user@2601:7c0:8180:89d0:e21a:92b8:d08a:508f) (Ping timeout: 264 seconds) |
| 2021-06-23 14:24:28 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 2021-06-23 14:26:24 | <safinaskar> | merijn: i didn't say "probably" |
| 2021-06-23 14:29:03 | <dminuoso> | To be fair, singletons gives you a good approximating for lightweight dependently typed programming. |
| 2021-06-23 14:29:12 | × | betelgeuse quits (~john2gb@94-225-47-8.access.telenet.be) (Ping timeout: 250 seconds) |
| 2021-06-23 14:29:22 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 2021-06-23 14:30:16 | <merijn> | safinaskar: Probably was my answer |
| 2021-06-23 14:30:28 | <merijn> | "is this true?" probably, yes |
| 2021-06-23 14:31:26 | <safinaskar> | well, my question is about current state |
| 2021-06-23 14:31:44 | × | BosonCollider quits (~olofs@90-227-86-119-no542.tbcn.telia.com) (Ping timeout: 252 seconds) |
| 2021-06-23 14:31:46 | <safinaskar> | is it true that currently you cannot pass runtime values as arguments to types? |
| 2021-06-23 14:32:14 | <chisui> | What's the status of the Unsaturated Type Families proposal anyways? |
| 2021-06-23 14:32:32 | <merijn> | That depends on what you're opinion on "faking something that looks like passing runtime values to types" is |
| 2021-06-23 14:32:41 | <merijn> | Can you do it? No. |
| 2021-06-23 14:32:52 | <merijn> | Does singletons let you fake the ability to do it? Yes. |
| 2021-06-23 14:34:12 | <safinaskar> | ok, thanks |
| 2021-06-23 14:34:14 | ← | safinaskar parts (~safinaska@109-252-90-89.nat.spd-mgts.ru) () |
| 2021-06-23 14:34:30 | <dminuoso> | What an odd fella. |
| 2021-06-23 14:35:05 | → | peterhil joins (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) |
| 2021-06-23 14:35:59 | <davean> | There was so much left unsaid in their question I struggled to come up with a question that would narrow down what they were asking enough to make it worth asking to try to get to an answer |
| 2021-06-23 14:37:23 | <maerwald[m]> | Maybe this is an assignment and they just needed *any* answer |
| 2021-06-23 14:37:32 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-06-23 14:37:38 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-23 14:38:09 | × | egoist quits (~egoist@186.235.85.100) (Quit: WeeChat 3.1) |
| 2021-06-23 14:38:40 | <chisui> | ... or win an argument :D |
| 2021-06-23 14:39:02 | <maerwald> | Yeah, that's even more important and requires our support |
| 2021-06-23 14:39:23 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-06-23 14:39:57 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 2021-06-23 14:40:08 | → | BosonCollider joins (~olofs@90-227-86-119-no542.tbcn.telia.com) |
| 2021-06-23 14:43:39 | <davean> | I mean, I guess core to the problem is types don't exist along side runtime values in any sense |
| 2021-06-23 14:43:52 | <davean> | so the question is, on the face of it, nonsensicle |
| 2021-06-23 14:44:09 | <davean> | but many type-looking things do exist |
| 2021-06-23 14:45:10 | × | CookE[] quits (~thedawn@user/thedawn) (Ping timeout: 244 seconds) |
| 2021-06-23 14:45:58 | <dminuoso> | Snarky opinion: Python is dependently typed: x if (type(o) is str) else y |
| 2021-06-23 14:46:40 | <dminuoso> | Type checking your program amounts to running it and see if its well behaved. |
| 2021-06-23 14:47:25 | × | ystael quits (~ystael@user/ystael) (Read error: Connection reset by peer) |
| 2021-06-23 14:48:12 | → | ystael joins (~ystael@user/ystael) |
| 2021-06-23 14:49:04 | → | hammock joins (~Hammock@2600:1700:19a1:3330::625) |
| 2021-06-23 14:49:29 | <maerwald> | It's well behaved by definition no? |
| 2021-06-23 14:49:30 | × | chomwitt quits (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4) (Ping timeout: 264 seconds) |
| 2021-06-23 14:49:49 | <davean> | yah the thing maerwald said |
| 2021-06-23 14:51:19 | → | betelgeuse joins (~john2gb@94-225-47-8.access.telenet.be) |
| 2021-06-23 14:54:09 | <nshepperd> | it passes type checking if it does what you want |
| 2021-06-23 14:54:18 | <nshepperd> | The most powerful type system on earth! |
| 2021-06-23 14:55:44 | <maerwald> | We just need a confogurable type system |
| 2021-06-23 14:56:05 | <maerwald> | confoguration... |
| 2021-06-23 14:56:24 | maerwald | signs off lol |
| 2021-06-23 14:58:38 | × | betelgeuse quits (~john2gb@94-225-47-8.access.telenet.be) (Read error: Connection reset by peer) |
| 2021-06-23 14:59:40 | <gentauro_> | maerwald: sign off? Is that a certificate? :P |
| 2021-06-23 14:59:46 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-23 15:00:05 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-23 15:00:12 | → | betelgeuse joins (~john2gb@94-225-47-8.access.telenet.be) |
| 2021-06-23 15:01:10 | → | teaSlurper joins (~chris@81.96.113.213) |
| 2021-06-23 15:01:48 | gentauro_ | is now known as gentauro |
All times are in UTC.