Logs: freenode/#haskell

←Prev Next→

Page 1 .. 242 243 244 245 246 247 248 249 250 251 252 .. 5022

— 502,152 events total

2020-09-27 04:22:05	<fraktor>	I would say that using types and associated functions to build state machines is perfectly correct, but those functions are not part of the type.
2020-09-27 04:22:25	<justsomeguy>	That sounds reasonable.
2020-09-27 04:22:26	×	furnost quits (~guy-laure@62-210-71-182.rev.poneytelecom.eu) (Read error: Connection reset by peer)
2020-09-27 04:22:31	→	falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a)
2020-09-27 04:22:32	<dsal>	A type is more like a set of possible values. A sum type adds to of those sets together. A product type multiplies them together. Probably something about burritos as well.
2020-09-27 04:22:36	<dolio>	How is `data Peano = Zero \| Suc Peano` a finite state machine?
2020-09-27 04:23:17	<dsal>	s/to of// -- not sure what happened there.
2020-09-27 04:23:23	×	ddellacosta quits (~dd@86.106.121.168) (Ping timeout: 240 seconds)
2020-09-27 04:25:45	<justsomeguy>	I suppose that would be an infinite type!
2020-09-27 04:25:57	<dolio>	It has infinite things in it, yeah.
2020-09-27 04:26:20	<justsomeguy>	I haven't yet figured out how to calculate the carnality of types, yet.
2020-09-27 04:26:46	<justsomeguy>	:g/ yet /d
2020-09-27 04:26:55	<dolio>	Infinitely many, even. Even in languages where the values themselves aren't infinite.
2020-09-27 04:27:55	<solonarv>	it is actually fairly simple
2020-09-27 04:28:25	<solonarv>	'\|' becomes '+', constructors with multiple fields become products
2020-09-27 04:28:25	×	mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer)
2020-09-27 04:28:57	→	mu_ joins (~mu@unaffiliated/mu)
2020-09-27 04:29:05	<solonarv>	e.g. 'data Foo = X Int Bool \| Y Word8' becomes 'Foo = Int * Bool + Word8'
2020-09-27 04:29:26	×	Orbstheorem quits (~roosember@hellendaal.orbstheorem.ch) (Ping timeout: 246 seconds)
2020-09-27 04:29:40	<solonarv>	substituting in the numbers for those: 'Foo = 2^64 * 2 + 2^8', and the rest is arithmetic
2020-09-27 04:29:51	→	ystael joins (~ystael@209.6.50.55)
2020-09-27 04:30:00	<dsal>	justsomeguy: Well, you can calculate cardinality of types at some point, but a product type of two lists is ∞*∞ whereas a sum type of two lists is just ∞+∞
2020-09-27 04:30:15	<justsomeguy>	If you have a type like “Peano = Zero \| Suc Peano”, is the carnality (1 * infinity) + 1?
2020-09-27 04:30:36	<dolio>	Infinite cardinalities get kind of ill behaved in constructive settings, though.
2020-09-27 04:31:37	<dsal>	Yeah. A more practical way to think of it is, e.g. what `Maybe t` does to `t`. It increases the cardinality by 1. Whereas you had all of the values of `t` before, now you have the same values + `Nothing`
2020-09-27 04:33:28	<dsal>	`Either a b` can contain any value of type `b` or any value of type `a`, so the total number of values it can contain is the sum of the cardinality of those two.
2020-09-27 04:34:04	×	xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 246 seconds)
2020-09-27 04:34:06	<dsal>	A product type `t` like `t a b` can contain a value of `b` for every value of `a`
2020-09-27 04:34:58	×	ystael quits (~ystael@209.6.50.55) (Ping timeout: 260 seconds)
2020-09-27 04:37:13	<justsomeguy>	Oh man, this beer is so good. Blueberry maple stout -- it's like I'm drinking a blueberry pancake.
2020-09-27 04:37:39	<justsomeguy>	Agh, that sounds awful, lol.
2020-09-27 04:37:40	×	sand_dull quits (~theuser@185.217.69.182) (Quit: Lost terminal)
2020-09-27 04:38:17	×	mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer)
2020-09-27 04:38:49	→	mu_ joins (~mu@unaffiliated/mu)
2020-09-27 04:45:45	→	isovector1 joins (~isovector@172.103.216.166.cable.tpia.cipherkey.com)
2020-09-27 04:47:35	×	elliott__ quits (~elliott@pool-100-36-54-163.washdc.fios.verizon.net) (Ping timeout: 265 seconds)
2020-09-27 04:48:04	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds)
2020-09-27 04:48:29	×	mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer)
2020-09-27 04:48:49	→	mu_ joins (~mu@unaffiliated/mu)
2020-09-27 04:54:52	→	snakemasterflex joins (~snakemast@213.100.206.23)
2020-09-27 04:58:27	×	mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer)
2020-09-27 04:58:48	→	mu_ joins (~mu@unaffiliated/mu)
2020-09-27 04:59:46	×	snakemasterflex quits (~snakemast@213.100.206.23) (Ping timeout: 272 seconds)
2020-09-27 05:02:07	×	ryansmccoy quits (~ryansmcco@193.37.254.27) (Ping timeout: 240 seconds)
2020-09-27 05:02:50	→	ryansmccoy joins (~ryansmcco@193.37.254.27)
2020-09-27 05:07:24	×	ryansmccoy quits (~ryansmcco@193.37.254.27) (Ping timeout: 265 seconds)
2020-09-27 05:07:45	→	ryansmccoy joins (~ryansmcco@193.37.254.27)
2020-09-27 05:08:44	×	mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer)
2020-09-27 05:08:50	→	mu__ joins (~mu@unaffiliated/mu)
2020-09-27 05:11:43	×	fraktor quits (~walt@129.93.191.18) (Ping timeout: 260 seconds)
2020-09-27 05:11:45	<koz_>	Something something I wrote a whole library for calculating the cardinality of finitary types.
2020-09-27 05:13:41	→	fraktor joins (~walt@193.32.127.214)
2020-09-27 05:13:41	<solonarv>	justsomeguy: for a recursive type, you end up with an equation like Peano = 1 + Peano; solve it and the solution is indeed Peano = ∞
2020-09-27 05:14:08	×	_vaibhavingale_ quits (~Adium@203.188.228.27) (Read error: Connection reset by peer)
2020-09-27 05:14:24	<justsomeguy>	Interesting!
2020-09-27 05:14:29	<koz_>	solonarv: Yay for the weird and wonderful world of infinity, where ordinars and cardinals no longer line up.
2020-09-27 05:14:50	×	fraktor quits (~walt@193.32.127.214) (Client Quit)
2020-09-27 05:16:18	<justsomeguy>	(One question I've had is: If you have a set of 0..-Inf and a set of 1..+inf, is the superset of both of them larger than either of the member sets?)
2020-09-27 05:16:29	<koz_>	justsomeguy: What do you mean by 'larger'?
2020-09-27 05:16:40	→	_vaibhavingale_ joins (~Adium@203.188.228.27)
2020-09-27 05:16:48	<justsomeguy>	...huh, I don't know. I guess the cardinality of the set.
2020-09-27 05:17:01	<solonarv>	in that case they are the same size, because there is a bijection between them
2020-09-27 05:17:12	<koz_>	Yep, that's exactly right.
2020-09-27 05:17:30	<koz_>	The only notion of 'size' sets admit is bijection.
2020-09-27 05:17:55	<justsomeguy>	Is a bijection a one-to-one correspondence?
2020-09-27 05:17:56	<koz_>	So therefore, a set which can be bijected with N (i.e. the natural numbers) has the same cardinality as any other such set.
2020-09-27 05:17:59	<koz_>	justsomeguy: Yep.
2020-09-27 05:17:59	<solonarv>	yes
2020-09-27 05:18:08	<koz_>	More precisely, a function that is both one-to-one and onto.
2020-09-27 05:18:18	<koz_>	(or 'injective and surjective' if you prefer)
2020-09-27 05:18:18	×	mu__ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer)
2020-09-27 05:18:20	<solonarv>	if the sets have additional structure (such as an ordering) then you can talk about more fine-grained size distinctions
2020-09-27 05:18:30	<solonarv>	this is the difference between cardinals and ordinals, sort of
2020-09-27 05:18:36	<koz_>	solonarv: Technically _all_ sets have an ordering.
2020-09-27 05:18:42	<koz_>	(thanks, well-ordering theorem!)
2020-09-27 05:18:49	→	mu_ joins (~mu@unaffiliated/mu)
2020-09-27 05:19:03	<solonarv>	right but you have to pick one and that affects which other ordered sets they're the same size as
2020-09-27 05:19:21	<koz_>	Yeah, then sure. That's where ordinals come in.
2020-09-27 05:19:40	<koz_>	Because while omega + 1 and omega + 2 have the same cardinality, they're different ordinals.
2020-09-27 05:19:44	<koz_>	Because infinity is weird.
2020-09-27 05:20:44	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-27 05:21:27	→	xerox_ joins (~xerox@unaffiliated/xerox)
2020-09-27 05:21:31	<koz_>	(I also love that technically, due to AC, all sets are well-ordered, but the ordering is not specified)
2020-09-27 05:21:40	<koz_>	(since we can only assert that it exists, not what it is)
2020-09-27 05:21:47	<koz_>	(thanks, non-constructive axioms...)
2020-09-27 05:23:05	×	justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds)
2020-09-27 05:24:11	→	howdoi joins (uid224@gateway/web/irccloud.com/x-lsrmpslujgdujhwj)
2020-09-27 05:26:11	<dolio>	Ordering isn't size, though.
2020-09-27 05:26:18	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-09-27 05:27:06	×	danso quits (~dan@107-190-41-58.cpe.teksavvy.com) (Quit: WeeChat 2.9)
2020-09-27 05:27:37	<dolio>	Like, when you consider the additional structure, it isn't affecting the size.
2020-09-27 05:28:41	×	mu_ quits (~mu@unaffiliated/mu) (Read error: Connection reset by peer)
2020-09-27 05:28:50	→	mu__ joins (~mu@unaffiliated/mu)
2020-09-27 05:30:19	<petersen>	dminuoso: right but somehow it is giving me a CPP error
2020-09-27 05:34:20	×	urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna)
2020-09-27 05:34:26	→	justanotheruser joins (~justanoth@unaffiliated/justanotheruser)
2020-09-27 05:36:14	<nshepperd>	solonarv: what's an example of a notion of size that depends on ordering?
2020-09-27 05:36:45	×	Sheilong quits (uid293653@gateway/web/irccloud.com/x-ilwvjocsxxlvfkle) ()
2020-09-27 05:36:59	<solonarv>	"which ordinal is this this order-isomorphic to?"
2020-09-27 05:36:59	×	eager_lambda quits (~gdrvnl@cpe-76-94-36-134.socal.res.rr.com) (Ping timeout: 246 seconds)

←Prev Next→

Page 1 .. 242 243 244 245 246 247 248 249 250 251 252 .. 5022

All times are in UTC.