Logs: freenode/#haskell
| 2021-05-11 13:27:04 | <sphi> | ype level |
| 2021-05-11 13:27:04 | <sphi> | > data Verb method (statusCode :: Nat) (contentType :: [*]) a |
| 2021-05-11 13:27:04 | <sphi> | type Get = Verb 'GET 200 |
| 2021-05-11 13:27:06 | <lambdabot> | <hint>:1:1: error: <hint>:1:1: error: parse error on input ‘data’ |
| 2021-05-11 13:27:10 | <sphi> | like so. |
| 2021-05-11 13:27:38 | <sphi> | what's up with 'GET ? |
| 2021-05-11 13:27:49 | <Taneb> | sphi: that means it's a value at the type level, rather than a type called GET |
| 2021-05-11 13:28:08 | <Taneb> | It's sometimes necessary so you don't get confused when you're doing lots of type-level stuff |
| 2021-05-11 13:28:11 | <merijn> | Disagree, tbh |
| 2021-05-11 13:28:21 | <sphi> | Taneb: like 1 2 3 instead of say, Int ? |
| 2021-05-11 13:28:25 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-05-11 13:28:31 | <merijn> | It *is* a type called GET, it's just not a type of kind * |
| 2021-05-11 13:28:47 | → | gentauro joins (~gentauro@unaffiliated/gentauro) |
| 2021-05-11 13:28:57 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-05-11 13:29:05 | <sphi> | ```type Delete = Verb 'DELETE 200 |
| 2021-05-11 13:29:05 | <sphi> | type Patch = Verb 'PATCH 200 |
| 2021-05-11 13:29:05 | <sphi> | type Post = Verb 'POST 200 |
| 2021-05-11 13:29:05 | <sphi> | type Put = Verb 'PUT 200 |
| 2021-05-11 13:29:07 | <sphi> | ``` |
| 2021-05-11 13:29:09 | <merijn> | sphi: There is an extension called DataKinds, which lets you turn "values" into "types |
| 2021-05-11 13:29:11 | <Taneb> | sphi: like the GET in data StdMethod = GET | ... rather than some data GET |
| 2021-05-11 13:29:22 | <merijn> | sphi: THis, however, presents a problem |
| 2021-05-11 13:29:49 | <sphi> | yea, it's kind of confusing |
| 2021-05-11 13:30:14 | <merijn> | sphi: Consider "data Foo = Foo", now how can I refer to the 2nd Foo (i.e. the data constructor) at the type level when using DataKinds, since "Foo" would just refer to to the *type*, not the new "value turned into a type" |
| 2021-05-11 13:30:46 | <merijn> | sphi: The ' syntax disambiguates this 'Foo says "I mean the value-turned-into-type Foo, not the type" |
| 2021-05-11 13:31:41 | <sphi> | merijn: ah, i see. |
| 2021-05-11 13:32:19 | <sphi> | follow up noob question. why would i want to refer to "value turned into a type" at type level ? |
| 2021-05-11 13:32:30 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-05-11 13:33:15 | <sphi> | OT, good luch with the talk, shapr: : D |
| 2021-05-11 13:33:21 | <sphi> | luck* |
| 2021-05-11 13:33:28 | <shapr> | yeah, I just gotta finish up with some links ... hmm |
| 2021-05-11 13:33:39 | <Taneb> | sphi: servant uses that technique a lot for describing the API in the type level. |
| 2021-05-11 13:33:40 | <shapr> | I need to do another test run beforehand |
| 2021-05-11 13:34:20 | → | nineonine joins (~nineonine@2604:3d08:777e:900:e4fe:87c8:c43b:fc90) |
| 2021-05-11 13:34:33 | <Taneb> | The idea is we want to parametrize the verb with what HTTP method it uses, and because we're doing this in types, it needs to be a type. However, it doesn't make sense to put anything like Int or Maybe in there, so we want a smaller kind |
| 2021-05-11 13:34:37 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-wydsfqjrhoioptxh) |
| 2021-05-11 13:35:00 | <Taneb> | We make a type for the possible HTTP methods, then lift that type to the kind level and hence its values to the type level |
| 2021-05-11 13:35:50 | <sphi> | Taneb: the docs are making more sense now. |
| 2021-05-11 13:36:00 | <sphi> | Thanks! |
| 2021-05-11 13:36:18 | <sphi> | ^ merijn: shapr Taneb : |
| 2021-05-11 13:42:32 | → | jamm__ joins (~jamm@unaffiliated/jamm) |
| 2021-05-11 13:42:45 | × | RusAlex quits (~Chel@unaffiliated/rusalex) (Quit: WeeChat 3.0) |
| 2021-05-11 13:44:41 | × | idhugo quits (~idhugo@80-62-116-231-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 2021-05-11 13:44:50 | → | gemmaro_ja joins (~Thunderbi@240f:74:d1f0:1:1bf:3730:3a54:b192) |
| 2021-05-11 13:45:03 | → | jame_227 joins (519fdca5@host81-159-220-165.range81-159.btcentralplus.com) |
| 2021-05-11 13:46:03 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 258 seconds) |
| 2021-05-11 13:46:46 | → | johncylee joins (~johncylee@185.163.110.100) |
| 2021-05-11 13:47:57 | <jame_227> | Hi, I had a quick question about how lazy evaluation works. say the generator [ doSomething x | x <- xs]. when this generator is called with say the argument !! 0, to return the first value from this function would it only evaluate the first x from xs? |
| 2021-05-11 13:48:24 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2021-05-11 13:48:26 | <opqdonut> | short answer: yes |
| 2021-05-11 13:48:50 | <tomsmeding> | assuming that's the only thing you do with that generator |
| 2021-05-11 13:48:56 | <opqdonut> | long answer: you can find out by hand-evaluating the expression `head (map doSomething xs)` |
| 2021-05-11 13:49:44 | <opqdonut> | I've just written a chapter for my course about this https://haskell.mooc.fi/part2#how-does-haskell-work |
| 2021-05-11 13:49:51 | <opqdonut> | 10.4.1 has some evaluation examples |
| 2021-05-11 13:50:28 | <jame_227> | Thank you for that, I will take a read :) |
| 2021-05-11 13:52:27 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 2021-05-11 13:53:29 | × | drbean_ quits (~drbean@TC210-63-209-98.static.apol.com.tw) (Ping timeout: 265 seconds) |
| 2021-05-11 13:54:34 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 2021-05-11 13:55:10 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 2021-05-11 13:56:41 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 240 seconds) |
| 2021-05-11 13:59:33 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds) |
| 2021-05-11 13:59:55 | → | Deide joins (~Deide@217.155.19.23) |
| 2021-05-11 14:00:20 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-05-11 14:01:50 | × | kritzefitz quits (~kritzefit@2003:5b:203b:200::10:49) (Remote host closed the connection) |
| 2021-05-11 14:02:57 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 2021-05-11 14:03:56 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-05-11 14:08:11 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-05-11 14:09:48 | × | Tops21 quits (~Tobias@dyndsl-095-033-090-210.ewe-ip-backbone.de) (Quit: Leaving.) |
| 2021-05-11 14:10:37 | → | Tops2 joins (~Tobias@dyndsl-095-033-090-210.ewe-ip-backbone.de) |
| 2021-05-11 14:12:40 | → | idhugo joins (~idhugo@80-62-116-231-mobile.dk.customer.tdc.net) |
| 2021-05-11 14:12:41 | × | trepanger_ quits (~z@173-16-201-214.client.mchsi.com) (Ping timeout: 240 seconds) |
| 2021-05-11 14:14:02 | × | hypercube quits (~hypercube@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Quit: WeeChat 3.1) |
| 2021-05-11 14:16:33 | → | alx741 joins (~alx741@186.178.109.110) |
| 2021-05-11 14:17:11 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 2021-05-11 14:17:20 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-sfhlcsgoerbublmd) |
| 2021-05-11 14:20:53 | × | idhugo quits (~idhugo@80-62-116-231-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 2021-05-11 14:24:28 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 2021-05-11 14:24:52 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 2021-05-11 14:27:12 | ← | maralorn parts (maralornma@gateway/shell/matrix.org/x-mkcwpfwlappvvein) ("User left") |
| 2021-05-11 14:29:05 | → | maralorn joins (maralornma@gateway/shell/matrix.org/x-mkcwpfwlappvvein) |
| 2021-05-11 14:29:22 | → | Sgeo joins (~Sgeo@ool-18b9875e.dyn.optonline.net) |
| 2021-05-11 14:30:38 | × | jamm__ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 2021-05-11 14:31:04 | → | wonko7 joins (~wonko7@62.115.229.50) |
| 2021-05-11 14:32:29 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-05-11 14:34:59 | × | nineonine quits (~nineonine@2604:3d08:777e:900:e4fe:87c8:c43b:fc90) (Ping timeout: 245 seconds) |
| 2021-05-11 14:35:06 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 3.1) |
| 2021-05-11 14:36:20 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 2021-05-11 14:36:30 | × | carlomagno quits (~cararell@148.87.23.5) (Ping timeout: 265 seconds) |
| 2021-05-11 14:36:53 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-05-11 14:36:57 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 250 seconds) |
| 2021-05-11 14:41:07 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-05-11 14:41:48 | m1dnight1 | is now known as m1dnight_ |
| 2021-05-11 14:42:21 | → | LKoen joins (~LKoen@156.168.9.109.rev.sfr.net) |
| 2021-05-11 14:43:16 | → | geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) |
| 2021-05-11 14:44:51 | → | Shuppiluliuma joins (~shuppilul@153.33.68.161) |
| 2021-05-11 14:45:05 | × | kidbuu quits (~Thunderbi@116.40.185.87) (Quit: kidbuu) |
| 2021-05-11 14:45:11 | × | thunderrd quits (~thunderrd@183.182.115.120) (Remote host closed the connection) |
| 2021-05-11 14:46:52 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-05-11 14:47:57 | hackage | bisc 0.3.0.0 - A small tool that clears cookies (and more). https://hackage.haskell.org/package/bisc-0.3.0.0 (rnhmjoj) |
| 2021-05-11 14:48:30 | → | mrchampion joins (~mrchampio@38.18.109.23) |
All times are in UTC.