Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 894 895 896 897 898 899 900 901 902 903 904 .. 5022
— 502,152 events total
2020-10-27 16:04:36 <Raito_Bezarius> read *
2020-10-27 16:05:15 × Abletai quits (~Lautris@p5df28535.dip0.t-ipconnect.de) (Client Quit)
2020-10-27 16:05:42 × Chi1thangoo quits (~Chi1thang@87.112.60.168) (Ping timeout: 272 seconds)
2020-10-27 16:06:18 → p-core joins (~Thunderbi@2001:718:1e03:5128:2ab7:7f35:48a1:8515)
2020-10-27 16:07:21 × kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection)
2020-10-27 16:07:28 hackage http-client-openssl 0.3.2.0 - http-client backend using the OpenSSL library. https://hackage.haskell.org/package/http-client-openssl-0.3.2.0 (MichaelSnoyman)
2020-10-27 16:08:00 → Rudd0 joins (~Rudd0@185.189.115.108)
2020-10-27 16:08:59 → kuribas joins (~user@ptr-25vy0i99c8o0gmravvh.18120a2.ip6.access.telenet.be)
2020-10-27 16:09:09 → kritzefitz joins (~kritzefit@212.86.56.80)
2020-10-27 16:09:16 → invaser joins (~Thunderbi@31.148.23.125)
2020-10-27 16:10:45 <T0pH4t> so should this not be legal, I get that x is a rigid type if I try to invoke it with an instance of Show, but it should be legal... `data ShowW = forall x. Show x => ShowW (x -> String)`
2020-10-27 16:10:52 <T0pH4t> i feel like i'm screwing up the type sig
2020-10-27 16:11:38 <tomsmeding> T0pH4t: what is your intention with that data type?
2020-10-27 16:12:07 <T0pH4t> its a simple example, but essentially `case w of ShowW f -> f (8 :: Int)`
2020-10-27 16:12:11 <T0pH4t> for example ^
2020-10-27 16:12:27 <tomsmeding> as it's written, that 'x' in 'forall x' is an existential variable
2020-10-27 16:12:29 → StoneToad_ joins (~StoneToad@199-167-119-149.ppp.storm.ca)
2020-10-27 16:12:40 → Sgeo joins (~Sgeo@ool-18b982ad.dyn.optonline.net)
2020-10-27 16:12:46 <tomsmeding> meaning that if you have a value ShowW f, then there _exists_ an x such that f is of type x -> String
2020-10-27 16:13:17 <tomsmeding> since you can't know whether that x is Int, that application f (8 :: Int) won't typecheck
2020-10-27 16:13:24 → geowiesnot joins (~user@87-89-181-157.abo.bbox.fr)
2020-10-27 16:13:30 <T0pH4t> well x is an instance of Show..
2020-10-27 16:13:33 × nitrix quits (~nitrix@haskell/developer/nitrix) (Quit: ZNC 1.8.2 - https://znc.in)
2020-10-27 16:13:34 → geekosaur joins (82659a09@host154-009.vpn.uakron.edu)
2020-10-27 16:13:38 <tomsmeding> sure, but you don't know which one
2020-10-27 16:13:42 <T0pH4t> the function should not care about x
2020-10-27 16:13:43 <tomsmeding> might be Float
2020-10-27 16:13:49 <T0pH4t> could be, should not care
2020-10-27 16:13:55 <T0pH4t> all it cares is that x has show
2020-10-27 16:13:57 <tomsmeding> but you're applying it to an Int!
2020-10-27 16:14:13 <T0pH4t> right, but x is a Show instance
2020-10-27 16:14:22 <tomsmeding> perhaps you wanted your declaration to mean: for _any_ x that is Show, f is a function that takes it
2020-10-27 16:14:29 <tomsmeding> is that accurate?
2020-10-27 16:14:30 <T0pH4t> yes
2020-10-27 16:14:33 <tomsmeding> right
2020-10-27 16:14:47 <T0pH4t> which is why i think my type sig is wrong :/
2020-10-27 16:15:16 <tomsmeding> data ShowW = ShowW (forall x. Show x => x -> String)
2020-10-27 16:15:21 → werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net)
2020-10-27 16:15:22 <tomsmeding> now x is universally quantified
2020-10-27 16:15:31 → damianfral3 joins (~damianfra@174.red-37-13-187.dynamicip.rima-tde.net)
2020-10-27 16:15:38 <tomsmeding> so the _user_ of the ShowW can choose x
2020-10-27 16:15:39 × StoneToad quits (~StoneToad@199-167-119-186.ppp.storm.ca) (Ping timeout: 260 seconds)
2020-10-27 16:15:47 <T0pH4t> that was it! thx tomsmeding.
2020-10-27 16:15:58 → nitrix joins (~nitrix@haskell/developer/nitrix)
2020-10-27 16:15:59 × dmwitch quits (~dmwit@pool-108-18-228-100.washdc.fios.verizon.net) (Read error: Connection reset by peer)
2020-10-27 16:16:04 <tomsmeding> as you wrote it, x was existentially quantified, so the _producer_ of the ShowW chooses x, and the caller has no idea which one was chosen
2020-10-27 16:16:16 <T0pH4t> ok, make sense
2020-10-27 16:16:37 <T0pH4t> odd that existentially would compile tho
2020-10-27 16:16:43 <T0pH4t> i don't see how that could ever resolve
2020-10-27 16:17:01 → dmwit joins (~dmwit@pool-108-18-228-100.washdc.fios.verizon.net)
2020-10-27 16:17:06 <tomsmeding> well, consider the following type
2020-10-27 16:17:31 <tomsmeding> data ToShow = forall x. Show x => ToShow (Int -> x)
2020-10-27 16:17:54 <tomsmeding> then as the producer of a ToShow, you can insert any function from Int to something that implements Show
2020-10-27 16:18:13 → bartemius joins (~bartemius@109-252-20-20.nat.spd-mgts.ru)
2020-10-27 16:18:13 <tomsmeding> as the user of a ToShow, you get a function Int -> x, where you have no idea what x is except that it implements Show
2020-10-27 16:18:27 <tomsmeding> see: same situation as in your datatype, but suddenly you can actually use this
2020-10-27 16:18:49 <tomsmeding> because if you have a ToShow f, then you can do 'show (f 42)', and you'll get a String :)
2020-10-27 16:18:51 <T0pH4t> oh so it inverses
2020-10-27 16:18:53 <T0pH4t> interesting
2020-10-27 16:19:20 <T0pH4t> very cool, good to know. Thx!
2020-10-27 16:19:34 <tomsmeding> https://wiki.haskell.org/Existential_type
2020-10-27 16:19:38 <tomsmeding> this may or may not be a good explanation
2020-10-27 16:20:09 <T0pH4t> haha as with many haskell wiki pages lol
2020-10-27 16:20:40 <tomsmeding> do you know the use of GADTs for expression AST's?
2020-10-27 16:20:48 <tomsmeding> (the typical motivating examples for GADTs)
2020-10-27 16:21:21 × gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Remote host closed the connection)
2020-10-27 16:21:24 × gxt quits (~gxt@gateway/tor-sasl/gxt) (Remote host closed the connection)
2020-10-27 16:21:34 <tomsmeding> like this one https://en.wikibooks.org/wiki/Haskell/GADT#GADTs
2020-10-27 16:22:04 → gxt joins (~gxt@gateway/tor-sasl/gxt)
2020-10-27 16:22:08 <tomsmeding> sometimes it's useful to define the following: data SomeExpr = forall a. SomeExpr (Expr a)
2020-10-27 16:22:34 <T0pH4t> yeah gdats i use fairly often
2020-10-27 16:22:44 <T0pH4t> gadts*
2020-10-27 16:22:55 × wraithm quits (~wraithm@unaffiliated/wraithm) (Excess Flood)
2020-10-27 16:22:59 <tomsmeding> e.g. a parser function might have type signature: String -> Either ErrorMsg SomeExpr
2020-10-27 16:23:10 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-27 16:23:20 <T0pH4t> right, infact i'm buidling a parser right now ;)
2020-10-27 16:23:37 <tomsmeding> existentials are quite useful in some circumstances :)
2020-10-27 16:24:12 <tomsmeding> the syntax where the exact placement of the 'forall' determines whether it's universal or existential can be very counter-intuitive however
2020-10-27 16:24:15 <T0pH4t> for example `data Parser a = PNum (forall x. (GTLType x, Num x) => I.Expression x -> I.GTL a)`
2020-10-27 16:24:18 → tromp joins (~tromp@dhcp-077-249-230-040.chello.nl)
2020-10-27 16:24:33 <tomsmeding> yeah there 'x' is universal
2020-10-27 16:24:43 <tomsmeding> unsure what GTL is though :)
2020-10-27 16:24:57 <T0pH4t> yeah, my own monad for the language
2020-10-27 16:25:01 → wraithm joins (~wraithm@unaffiliated/wraithm)
2020-10-27 16:25:25 <T0pH4t> but then you can have `parseToken :: Token -> Parser a -> I.GTL a`
2020-10-27 16:25:34 <T0pH4t> such that you can do some really cool stuff
2020-10-27 16:26:57 × chele quits (~chele@ip5b416ea2.dynamic.kabel-deutschland.de) (Quit: Leaving)
2020-10-27 16:26:57 → conal joins (~conal@64.71.133.70)
2020-10-27 16:27:34 → dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com)
2020-10-27 16:27:47 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds)
2020-10-27 16:29:46 × raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds)
2020-10-27 16:30:11 ← teardown parts (~user@unaffiliated/mrush) ()
2020-10-27 16:30:12 → raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2020-10-27 16:30:21 → wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net)
2020-10-27 16:30:52 × wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Client Quit)
2020-10-27 16:30:58 × taurux quits (~taurux@net-93-151-203-8.cust.vodafonedsl.it) (Quit: ZNC 1.7.5 - https://znc.in)
2020-10-27 16:31:10 → wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net)
2020-10-27 16:31:35 → teardown joins (~user@unaffiliated/mrush)
2020-10-27 16:34:16 × conal quits (~conal@64.71.133.70) (Read error: Connection reset by peer)
2020-10-27 16:34:58 → Stanley00 joins (~stanley00@unaffiliated/stanley00)
←Prev  Next→
Page 1 .. 894 895 896 897 898 899 900 901 902 903 904 .. 5022

All times are in UTC.