Logs: freenode/#haskell

←Prev Next→

Page 1 .. 13 14 15 16 17 18 19 20 21 22 23 .. 5022

— 502,152 events total

2020-09-17 06:46:33	<edwardk>	https://hub.darcs.net/dolio/upts/browse/Language/UPTS/SyntaxTree.hs#39 is an example of a small pure type system with universe polymorphism by dolio that uses bound
2020-09-17 06:46:38	<siraben>	I haven't used the bound library before, will it handle the scoping and substitution for me?
2020-09-17 06:46:43	<edwardk>	yeah
2020-09-17 06:47:05	<edwardk>	your Term type becomes a monad, using (>>=) for substitution.
2020-09-17 06:47:15	<edwardk>	and Scope () Term becomes 'and i need an extra bound variable'
2020-09-17 06:47:20	<MarcelineVQ>	is the purpose of that 'approximately well typed' to check if something could be correct, with less work, before you check fully?
2020-09-17 06:47:23	<edwardk>	and you use >>>= to walk over that
2020-09-17 06:47:28	<edwardk>	MarcelineVQ: yeah
2020-09-17 06:47:37	<edwardk>	catch most of the stupid programmer bugs
2020-09-17 06:47:40	<edwardk>	basically a form of lint
2020-09-17 06:48:27	<edwardk>	maybe if you cps transformed everything you could get into a state where you could do reflection to create the types off terms locally that you'd need... or you could wait for richard to finish dependent hakell
2020-09-17 06:48:29	<edwardk>	er haskell
2020-09-17 06:48:49	→	borne joins (~fritjof@200116b8641fc4005e981dab12496c3b.dip.versatel-1u1.de)
2020-09-17 06:49:00	×	xff0x_ quits (~fox@2001:1a81:5306:e200:7599:d48:f5dc:5fef) (Ping timeout: 244 seconds)
2020-09-17 06:49:14	×	knupfer quits (~Thunderbi@mue-88-130-61-060.dsl.tropolys.de) (Ping timeout: 272 seconds)
2020-09-17 06:49:14	<edwardk>	https://hub.darcs.net/dolio/upts/browse/Language/UPTS/SyntaxTree.hs#73 see how the >>>= is used for the body of the lambda?
2020-09-17 06:49:49	<siraben>	Ah
2020-09-17 06:49:50	<edwardk>	https://www.schoolofhaskell.com/user/edwardk/bound is an article i wrote on bound
2020-09-17 06:50:07	→	xff0x_ joins (~fox@2001:1a81:5306:e200:5d84:8198:9ead:fb9f)
2020-09-17 06:50:15	<siraben>	great, saved.
2020-09-17 06:50:20	×	justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) ()
2020-09-17 06:50:30	<edwardk>	the key is that when you need a Term and have a Scope () Term you need to give me the value for the extra variable. it won't typecheck if you f up the name manipulation
2020-09-17 06:51:08	<edwardk>	abstract1 and instantiate1 give you tools for converting from Scope () m <-> m by capturing/instantiating
2020-09-17 06:51:21	<edwardk>	bound works best when you're working with a language with one type of name
2020-09-17 06:51:39	<edwardk>	we made it work for ermine by lots of hand-holding
2020-09-17 06:52:05	<edwardk>	but its quite pleasant to just walk terms, be able to >>= for substituting in your environment, use foldMap to extract free variables.
2020-09-17 06:52:23	<edwardk>	Scope is basically a 'faster' EitherT
2020-09-17 06:53:02	<edwardk>	abstract and instantiate handle the case where you want to bind multiple variables at once, (i don't have to just put on a (), maybe i'm binding 8 variables at once in a recursive let binding/where clause, etc.
2020-09-17 06:54:12	×	tomboy64 quits (~tomboy64@gateway/tor-sasl/tomboy64) (Remote host closed the connection)
2020-09-17 06:55:52	×	mirrorbird quits (~psutcliff@2a00:801:44b:8959:8d6c:276b:332b:1c71) (Remote host closed the connection)
2020-09-17 06:56:04	→	chele joins (~chele@ip5b416ea2.dynamic.kabel-deutschland.de)
2020-09-17 06:56:32	→	mirrorbird joins (~psutcliff@2a00:801:44b:8959:8d6c:276b:332b:1c71)
2020-09-17 06:58:24	<gnumonik>	I thought I remembered some function in the lens library that returns a list of (maybe strings that represent?) the lenses/etc that exist for a datatype. Anyone know what that is or am I mistaken?
2020-09-17 07:02:27	<edwardk>	:t universe
2020-09-17 07:02:28	<lambdabot>	Plated a => a -> [a]
2020-09-17 07:02:33	<edwardk>	er that's not it
2020-09-17 07:02:46	→	rapskalian joins (~user@2601:804:8400:5750:6d07:cb01:64a9:36bb)
2020-09-17 07:03:21	→	bitmagie joins (~Thunderbi@200116b80670970060cb385f030853d4.dip.versatel-1u1.de)
2020-09-17 07:03:28	→	mmohammadi9812 joins (~mmohammad@5.116.223.123)
2020-09-17 07:03:31	<edwardk>	:t contexts
2020-09-17 07:03:33	<lambdabot>	Plated a => a -> [Context a a a]
2020-09-17 07:03:47	<edwardk>	:t contextsOf
2020-09-17 07:03:49	<lambdabot>	ATraversal' a a -> a -> [Context a a a]
2020-09-17 07:03:55	×	falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Ping timeout: 240 seconds)
2020-09-17 07:04:02	<edwardk>	that gives you each of the 'one hole contexts' of a term
2020-09-17 07:04:53	<edwardk>	you give a traversal that knows how to find all the parts, and it give you back a context which has what was in that position and a function that can sew the type back up around a new value.
2020-09-17 07:05:09	<edwardk>	contexts works off the Plated data type
2020-09-17 07:05:39	<edwardk>	a context is a "lens that has been applied to an 's'"
2020-09-17 07:05:51	×	da39a3ee5e6b4b0d quits (~textual@2403:6200:8876:37d7:55fb:4d37:ffc2:715b) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-17 07:05:55	<gnumonik>	That should work, thanks!
2020-09-17 07:06:13	×	gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 272 seconds)
2020-09-17 07:06:14	<edwardk>	if you think of a lens as s -> (a, b -> t) Context a b t = (a, b -> t)
2020-09-17 07:06:37	<edwardk>	with some newtype and typical lens over-generality applied
2020-09-17 07:06:46	<edwardk>	:info Context
2020-09-17 07:06:52	→	whiteline joins (~whiteline@unaffiliated/whiteline)
2020-09-17 07:06:58	<edwardk>	@info Context
2020-09-17 07:06:59	<lambdabot>	Context
2020-09-17 07:07:05	<edwardk>	that was helpful.
2020-09-17 07:07:07	<edwardk>	@type Context
2020-09-17 07:07:09	<lambdabot>	(b -> t) -> a -> Context a b t
2020-09-17 07:07:41	×	rapskalian quits (~user@2601:804:8400:5750:6d07:cb01:64a9:36bb) (Ping timeout: 244 seconds)
2020-09-17 07:08:19	×	sumo_r9 quits (0ec9fb69@14-201-251-105.tpgi.com.au) (Remote host closed the connection)
2020-09-17 07:09:48	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-17 07:10:01	×	mmohammadi9812 quits (~mmohammad@5.116.223.123) (Ping timeout: 272 seconds)
2020-09-17 07:10:49	→	mmohammadi9812 joins (~mmohammad@5.238.164.128)
2020-09-17 07:10:52	×	tzh quits (~tzh@2601:448:c500:5300::ad1c) (Quit: zzz)
2020-09-17 07:10:56	→	tomboy64 joins (~tomboy64@gateway/tor-sasl/tomboy64)
2020-09-17 07:11:06	×	asan quits (~yan4138@124.78.5.33) (Ping timeout: 256 seconds)
2020-09-17 07:13:19	→	kritzefitz joins (~kritzefit@fw-front.credativ.com)
2020-09-17 07:15:52	×	finkata quits (~dpetrov@83.222.188.39) (Remote host closed the connection)
2020-09-17 07:15:55	×	oxide quits (~lambda@unaffiliated/mclaren) (Read error: Connection reset by peer)
2020-09-17 07:16:21	→	asan joins (~yan4138@61.170.146.94)
2020-09-17 07:17:40	→	da39a3ee5e6b4b0d joins (~textual@2403:6200:8876:37d7:55fb:4d37:ffc2:715b)
2020-09-17 07:18:53	×	pera quits (~pera@unaffiliated/pera) (Ping timeout: 272 seconds)
2020-09-17 07:19:56	×	heatsink quits (~heatsink@2600:1700:bef1:5e10:b0dc:6c54:247b:ece) (Remote host closed the connection)
2020-09-17 07:20:58	→	alp_ joins (~alp@2a01:e0a:58b:4920:90ae:a5d:9349:f8d8)
2020-09-17 07:21:58	→	ph88 joins (~ph88@2a02:8109:9e40:2704:6cf2:c517:5b95:5f99)
2020-09-17 07:22:15	→	gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net)
2020-09-17 07:22:21	→	maier joins (~maier@b2b-37-24-119-190.unitymedia.biz)
2020-09-17 07:22:29	maier	is now known as kenran
2020-09-17 07:22:38	→	yoneda joins (~mike@193.206.102.122)
2020-09-17 07:23:06	×	yoneda quits (~mike@193.206.102.122) (Client Quit)
2020-09-17 07:23:17	<kenran>	Is there a specific reason why Data.Vector.Storable.Vector doesn't have "the usual" instances? I'm specifically wondering about Foldable.
2020-09-17 07:25:51	→	yoneda joins (~mike@193.206.102.122)
2020-09-17 07:25:58	×	stiell quits (~stian@fsf/member/stiell) (Ping timeout: 272 seconds)
2020-09-17 07:26:22	→	pera joins (~pera@unaffiliated/pera)
2020-09-17 07:26:48	×	gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds)
2020-09-17 07:27:13	<Axman6>	because you can't put a constraint on the types of the values stored in it to guarantee they are sStorablwe
2020-09-17 07:27:19	<Axman6>	Storable*
2020-09-17 07:27:30	<dminuoso>	% :t foldr
2020-09-17 07:27:31	<yahb>	dminuoso: Foldable t => (a -> b -> b) -> b -> t a -> b
2020-09-17 07:27:40	<dminuoso>	kenran: ^- See how b is unconstrained?
2020-09-17 07:28:07	<nshepperd>	it's the lack of constraint on 'a' that is the problem here
2020-09-17 07:28:19	<dminuoso>	Oh
2020-09-17 07:28:49	<dminuoso>	nshepperd: Why does that matter?
2020-09-17 07:30:27	→	AstroDroid joins (~AstroDroi@84.39.117.57)
2020-09-17 07:30:34	<dminuoso>	Ah nevermind, heh.
2020-09-17 07:30:44	<nshepperd>	because where t ~ Storable.Vector you can't get the 'a's out of that 't a' without having the Storable a instance at hand
2020-09-17 07:30:56	<dminuoso>	nshepperd: I kept thinking of Functor for some bizarre reason.
2020-09-17 07:31:15	<dminuoso>	In which case it'd be both a and b that'd need the Storable constraint

←Prev Next→

Page 1 .. 13 14 15 16 17 18 19 20 21 22 23 .. 5022

All times are in UTC.