Logs: freenode/#haskell

←Prev Next→

Page 1 .. 4365 4366 4367 4368 4369 4370 4371 4372 4373 4374 4375 .. 5022

— 502,152 events total

2021-04-12 03:58:59	<ski>	to
2021-04-12 03:59:15	<ski>	MkQOps :: forall q. ((q,a -> q -> q,q -> Maybe (q,a)) -> QueueOps a)
2021-04-12 03:59:21	<ski>	or simply
2021-04-12 03:59:24	<ski>	MkQOps :: forall q. (q,a -> q -> q,q -> Maybe (q,a)) -> QueueOps a
2021-04-12 03:59:30	→	abhixec joins (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net)
2021-04-12 03:59:45	<ski>	(also `a' is really quantified with a `forall' over this whole signature)
2021-04-12 04:00:14	<Newbievarine>	I understand all that but what you're saying that if in haskell you write f :: a -> (forall b. Foo b => b) that the range type is actually a universal quantification in haskell. (not sure you can even write this actually)
2021-04-12 04:00:20	→	vicfred joins (vicfred@gateway/vpn/mullvad/vicfred)
2021-04-12 04:00:48	<ski>	so, a data constructor (or generally, any function), which takes an argument of existentially quantified type, is basically the same as a polymorphic ditto, that accepts an argument for any `q' (in this case), and whose result type doesn't mention `q'
2021-04-12 04:01:10	<ski>	Newbievarine : yes, and yes (you can write that, with extensions)
2021-04-12 04:01:38	<Newbievarine>	okay. I got the wrong impression by the way forall always got brought up int he syntax of declaring existential types. thanks for the clarification
2021-04-12 04:01:44	<ski>	so, using the `ExistentialQuantification' extension (which, imho, is a misnomer), we can now express `QueueOps' as
2021-04-12 04:01:57	<Newbievarine>	but yes what I meant then was (exists a. Tc a .. so on and so forth
2021-04-12 04:01:59	<ski>	data QueueOps a = forall q. MkQOps (q,a -> q -> q,q -> Maybe (q,a))
2021-04-12 04:02:06	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
2021-04-12 04:02:38	<ski>	and this `forall q.' means universal quantification, means polymorphism, means that the data constructor `MkQOps' is polymorphic
2021-04-12 04:02:40	→	ulfryk joins (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6)
2021-04-12 04:02:48	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-04-12 04:02:58	<ski>	it's not the case that, somehow, `forall' really means `exists', in this case
2021-04-12 04:03:46	<ski>	similarly, `(Cxt *> T) -> U' is logially equivalent to `Cxt => (T -> U)'
2021-04-12 04:03:50	<Newbievarine>	because of the implicit universal quantification in Haskell I thought that the forall keyword got hijacked but I see now you can actually use it explicit in a subexpression as you say, with an extension, and it's actually universal quantification
2021-04-12 04:04:46	<Newbievarine>	no such support for existential quantification I'm guessing ?
2021-04-12 04:05:08	<ski>	a value of type `Cxt => ...' expects the caller/user/consumer to provide evidence for the constraint `Cxt'. while a value of type `Cxt *> ...', that is, the callee/implementor/producer of it, will itself provide such evidence of `Cxt' to the caller/&c.
2021-04-12 04:06:16	<ski>	the other, (b) way of representing/encoding `exists q. (q,a -> q -> q,q -> Maybe (q,a))' uses the general equivalence between `T' and `forall o. (T -> o) -> o'
2021-04-12 04:07:27	×	ulfryk quits (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) (Ping timeout: 260 seconds)
2021-04-12 04:07:52	<ski>	in this case, we get `forall o. ((exists q. (q,a -> q -> q,q -> Maybe (q,a))) -> o) -> o' which then is equivalent to `forall o. (forall q. (q,a -> q -> q,q -> Maybe (q,a)) -> o) -> o', or, currying the callback/continuation, `forall o. (forall q. q -> (a -> q -> q) -> (q -> Maybe (q,a)) -> o) -> o'. this is a rank-two type, since it has a `forall' in an argument type
2021-04-12 04:07:54	×	pavonia quits (~user@unaffiliated/siracusa) (Quit: Bye!)
2021-04-12 04:08:08	→	ulfryk joins (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6)
2021-04-12 04:08:39	<ski>	(i stress that there's two encodings to emphasize that `ExistentialQuantification' is not "the way to do existentials". it's one possible way)
2021-04-12 04:08:57	ski	nods to Newbievarine
2021-04-12 04:09:21	<ski>	fwiw, did you ever check out "Polymorphic Type Inference" by Michael I. Schwartzbach in 1995-03 at <https://cs.au.dk/~amoeller/mis/typeinf.p(s\|df)>,<https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.1493> ?
2021-04-12 04:10:06	<ski>	it also mentions existentials. might be interesting to take a glance at
2021-04-12 04:10:14	<ski>	@where on-understanding
2021-04-12 04:10:14	<lambdabot>	"On Understanding Types, Data Abstraction, and Polymorphism" by Luca Cardelli,Peter Wegner in 1985-12 at <http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf>
2021-04-12 04:10:19	<ski>	is also nice
2021-04-12 04:12:00	<Newbievarine>	thanks for the references
2021-04-12 04:12:06	<ski>	@where on-understanding-revisited
2021-04-12 04:12:06	<lambdabot>	"On Understanding Data Abstraction, Revisited" by William R. Cook in 2009-10 at <http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf>
2021-04-12 04:12:37	×	ulfryk quits (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) (Ping timeout: 250 seconds)
2021-04-12 04:12:38	→	PragCypher_ joins (~cypher@li1507-98.members.linode.com)
2021-04-12 04:12:38	<ski>	talks a bit more on OO vs. ADT (abstract data types). both are related to existentials, albeit different ways of using them
2021-04-12 04:12:43	→	dminuoso_ joins (~dminuoso@static.88-198-218-68.clients.your-server.de)
2021-04-12 04:12:53	→	electrostat_ joins (~dag@unaffiliated/electrostat)
2021-04-12 04:13:28	→	pieguy128_ joins (~pieguy128@bas1-quebec14-67-70-101-46.dsl.bell.ca)
2021-04-12 04:13:47	→	texasmynsted_ joins (~texasmyns@99.96.221.112)
2021-04-12 04:14:11	<ski>	relevant here is that `exists s. (s,s -> ..s..)' is equivalent to `nu s. ..s..' (greatest fixedpoint). similarly to how `forall r. (..r.. -> r) -> r' is equivalent to `mu r. ..r..' (least fixedpoint)
2021-04-12 04:14:49	→	dilinger joins (~dilinger@spindle.queued.net)
2021-04-12 04:14:59	→	oleks_ joins (~oleks@188.166.34.97)
2021-04-12 04:15:11	→	akhesaca1o joins (~caro@212.83.144.58)
2021-04-12 04:15:28	→	tristanC_ joins (~tristanC@unaffiliated/tristanc)
2021-04-12 04:15:36	→	AWizzArd_ joins (~code@gehrels.uberspace.de)
2021-04-12 04:15:52	→	cafce25_ joins (~cafce25@ipbcc3009d.dynamic.kabel-deutschland.de)
2021-04-12 04:15:53	<ski>	e.g., taking `exists q. (q,a -> q -> q,q -> Maybe (q,a))', we can rephrase this as `exists q. (q,q -> (a -> q,Maybe (q,a)))', which then becomes `nu q. (a -> q,Maybe (q,a))'. which translates to the recursive (thought of as coinductive) `data QueueOps a = MkQOps (a -> QueueOps a) (Maybe (a,QueueOps a))'
2021-04-12 04:15:55	<Newbievarine>	anyway says right here at the beginning https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/existential_quantification.html#existentially-quantified-data-constructors that the syntax is such that "data Blah = forall a. Boop a" means a construct Boop of type forall a. a -> Blah
2021-04-12 04:16:02	×	texasmynsted quits (~texasmyns@99.96.221.112) (Killed (tolkien.freenode.net (Nickname regained by services)))
2021-04-12 04:16:02	texasmynsted_	is now known as texasmynsted
2021-04-12 04:16:05	<Newbievarine>	suppose I should've read that part :D
2021-04-12 04:16:15	<ski>	yup
2021-04-12 04:16:50	<ski>	so .. often, instead of using existentials, one can use recursive types
2021-04-12 04:17:10	<ski>	(and this is a typically OO thing to do)
2021-04-12 04:17:58	<ski>	(however, this fails if one e.g. have "binary methods", like if we had had `q -> q -> q', for merging two queues into a single queue, or something like that)
2021-04-12 04:19:12	→	wraithm_ joins (~wraithm@unaffiliated/wraithm)
2021-04-12 04:19:16	×	jiribenes quits (~jiribenes@rosa.jiribenes.com) (Remote host closed the connection)
2021-04-12 04:20:02	→	jiribenes joins (~jiribenes@rosa.jiribenes.com)
2021-04-12 04:20:18	→	aib42 joins (~aib@unaffiliated/aib42)
2021-04-12 04:20:25	×	pnotequalnp[m] quits (pnotequaln@gateway/shell/matrix.org/x-vbfhpdihocudbihr) (.net .split)
2021-04-12 04:20:25	×	amerocu[m] quits (amerocumat@gateway/shell/matrix.org/x-qxnfpxkjfoepsjkc) (.net .split)
2021-04-12 04:20:25	×	Poyo[m] quits (stikynotha@gateway/shell/matrix.org/x-hdaxlpnazrfvbqll) (.net .split)
2021-04-12 04:20:26	×	heck-to-the-gnom quits (heck-to-th@gateway/shell/matrix.org/x-odwuoyyyfqjuhqfr) (.net .split)
2021-04-12 04:20:26	×	VarikValefor[m] quits (varikvalef@gateway/shell/matrix.org/x-rxkwfuaqsqeyxnjv) (.net .split)
2021-04-12 04:20:26	×	anon1891[m] quits (anon1891ma@gateway/shell/matrix.org/x-onnujzintxhdncvb) (.net .split)
2021-04-12 04:20:26	×	cafce25 quits (~cafce25@ipbcc3009d.dynamic.kabel-deutschland.de) (.net .split)
2021-04-12 04:20:26	×	beardhatcode quits (robbertbea@gateway/shell/matrix.org/x-xwmepnlvznlpjdga) (.net .split)
2021-04-12 04:20:26	×	kadoban quits (kadobanemp@gateway/shell/matrix.org/x-gxlvabnrocccxmxd) (.net .split)
2021-04-12 04:20:26	×	mly quits (mlydisenco@gateway/shell/matrix.org/x-hdizmtyvxksdkslu) (.net .split)
2021-04-12 04:20:26	×	DevTurks[m] quits (turkdevops@gateway/shell/matrix.org/x-ojlnprlhammzunlz) (.net .split)
2021-04-12 04:20:26	×	pieguy128 quits (~pieguy128@bras-base-mtrlpq5031w-grc-47-67-70-101-46.dsl.bell.ca) (.net .split)
2021-04-12 04:20:26	×	jtojnar quits (jtojnarmat@gateway/shell/matrix.org/x-lztialmegsqbabni) (.net .split)
2021-04-12 04:20:27	×	wraithm quits (~wraithm@unaffiliated/wraithm) (.net .split)
2021-04-12 04:20:27	×	norsxa quits (uid494793@gateway/web/irccloud.com/x-wurwmiwscjouwjvh) (.net .split)
2021-04-12 04:20:27	×	angerman quits (sid209936@gateway/web/irccloud.com/x-telvwebhmibfciob) (.net .split)
2021-04-12 04:20:27	×	amatecha____ quits (sid10006@gateway/web/irccloud.com/x-zvybgedfthmrvwqy) (.net .split)
2021-04-12 04:20:27	×	cawfee quits (chiya@2406:3003:2077:2341::babe) (.net .split)
2021-04-12 04:20:27	×	SolarAquarion quits (SolarAquar@gateway/shell/panicbnc/x-jhqcerqxwmhuufxz) (.net .split)
2021-04-12 04:20:27	×	Papa quits (~papa@unaffiliated/papa) (.net .split)
2021-04-12 04:20:27	×	AWizzArd quits (~code@unaffiliated/awizzard) (.net .split)
2021-04-12 04:20:27	×	tristanC quits (~tristanC@unaffiliated/tristanc) (.net .split)
2021-04-12 04:20:27	×	gambpang quits (~gambpang@unaffiliated/gambpang) (.net .split)
2021-04-12 04:20:27	×	Klumben quits (Nsaiswatch@gateway/shell/panicbnc/x-tsikniggqbsrqudz) (.net .split)
2021-04-12 04:20:27	×	urdh quits (~urdh@unaffiliated/urdh) (.net .split)
2021-04-12 04:20:27	×	dminuoso quits (~dminuoso@static.88-198-218-68.clients.your-server.de) (.net .split)
2021-04-12 04:20:27	×	PragCypher quits (~cypher@li1507-98.members.linode.com) (.net .split)
2021-04-12 04:20:27	×	aib quits (~aib@unaffiliated/aib42) (.net .split)
2021-04-12 04:20:27	×	electrostat quits (~dag@unaffiliated/electrostat) (.net .split)
2021-04-12 04:20:27	×	PatrickRobotham_ quits (sid18270@gateway/web/irccloud.com/x-oiupfqgvgmcusgoi) (.net .split)
2021-04-12 04:20:27	×	sclv quits (sid39734@haskell/developer/sclv) (.net .split)
2021-04-12 04:20:27	×	scav quits (sid309693@gateway/web/irccloud.com/x-uslhiglasceegqqw) (.net .split)
2021-04-12 04:20:27	×	anderson quits (~ande@159.65.95.130) (.net .split)
2021-04-12 04:20:27	×	akhesacaro quits (~caro@212.83.144.58) (.net .split)
2021-04-12 04:20:27	×	earthy_ quits (~arthurvl@deban2.xs4all.space) (.net .split)

←Prev Next→

Page 1 .. 4365 4366 4367 4368 4369 4370 4371 4372 4373 4374 4375 .. 5022

All times are in UTC.