Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 63 64 65 66 67 68 69 70 71 72 73 .. 5022
— 502,152 events total
2020-09-19 07:36:11 → danvet_ joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa)
2020-09-19 07:36:16 <edwardk> its whatever names you have before you start binding things up
2020-09-19 07:37:03 × irc_user quits (uid423822@gateway/web/irccloud.com/x-stvaebjkkjdergtx) (Quit: Connection closed for inactivity)
2020-09-19 07:37:16 <edwardk> heck, when working with meta variables the 'a' in my expressions is often something like an newtype Meta = Meta (IORef (Maybe (Term Meta)))
2020-09-19 07:38:03 <edwardk> so i start out with Expr String, because its easy to work with in the parser, finish closing my terms, because i traverse over them with traverse (const Nothing) -- which tells me Nothing if the term is not closed, or Just (Expr a) for any a i want if it is closed
2020-09-19 07:38:32 <edwardk> then I can start using it as Expr Void for a while, maybe switching to Expr Meta when doing unification
2020-09-19 07:38:48 <edwardk> s/Term/Expr/ in the definition of meta to use that though
2020-09-19 07:39:41 <edwardk> abstract1 looks for all occurrences of that name in Term a and converts them to the () in Scope () Term a
2020-09-19 07:40:07 <edwardk> abstract is more general and can be used to grab several names at once, say for a pattern or a recursive let binding
2020-09-19 07:40:37 <siraben> That makes sense
2020-09-19 07:40:39 <edwardk> instantiate1 is how you substitute a term for the bound () in Scope () Term a
2020-09-19 07:41:01 <siraben> hasType (lam 0 $ Var 0) (pi 0 (Var 0) (Var 0)) seems to fail, but hasType (lam 0 $ Var 0) (pi 0 (Var 1) (Var 1)) succeeds
2020-09-19 07:41:16 <siraben> It seemed to try to equate Var 0 and Var 1, hm.
2020-09-19 07:42:12 <siraben> I'm trying to do a simple, (\x → x) : Π (x : Star). x → x
2020-09-19 07:42:15 <edwardk> (\x. x) :: Pi(x :: y). y -- is what the second one says
2020-09-19 07:42:18 → supercoven joins (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi)
2020-09-19 07:42:19 × supercoven quits (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Max SendQ exceeded)
2020-09-19 07:42:27 × jedws quits (~jedws@121.209.139.222) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-19 07:42:33 → supercoven joins (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi)
2020-09-19 07:43:09 <edwardk> the former says (\x.x) :: Pi(x:some_unbound_variable_named_0).x. no?
2020-09-19 07:43:26 <siraben> Ah, hm.
2020-09-19 07:43:36 <edwardk> er i don't know your pi constructor there
2020-09-19 07:43:39 <edwardk> let me read the code
2020-09-19 07:43:41 → rekahsoft joins (~rekahsoft@CPE0008a20f982f-CM64777d666260.cpe.net.cable.rogers.com)
2020-09-19 07:44:02 <edwardk> but it should be something along those lines. pi should only be binding the variable name in the result type not the arg type
2020-09-19 07:44:07 <siraben> http://ix.io/2y5J
2020-09-19 07:44:21 <siraben> it's the same as the one in the lambda-pi repo, but with error messages
2020-09-19 07:44:34 → oxide joins (~lambda@unaffiliated/mclaren)
2020-09-19 07:45:04 × toorevitimirp quits (~tooreviti@117.182.182.33) (Remote host closed the connection)
2020-09-19 07:45:17 → jedws joins (~jedws@121.209.139.222)
2020-09-19 07:46:25 <edwardk> i'd expect your hasType thing to be like
2020-09-19 07:46:38 → toorevitimirp joins (~tooreviti@117.182.182.33)
2020-09-19 07:46:46 × platypine quits (~platypine@c-73-249-162-185.hsd1.ct.comcast.net) (Read error: Connection reset by peer)
2020-09-19 07:47:07 → platypine joins (~platypine@c-73-249-162-185.hsd1.ct.comcast.net)
2020-09-19 07:47:19 <siraben> Ah before it would return a Bool, heh.
2020-09-19 07:47:31 <edwardk> hasType (lam "x" $ Var "x") (pi "y" Star (Var "y"))
2020-09-19 07:48:26 <siraben> Translating that I have, hasType (lam 0 $ Var 0) (pi 1 Star (Var 1)) which gets Left "Failed to unify Var 1 with Star"
2020-09-19 07:48:27 × supercoven quits (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Max SendQ exceeded)
2020-09-19 07:48:41 → supercoven joins (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi)
2020-09-19 07:48:44 → gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net)
2020-09-19 07:48:47 × rekahsoft quits (~rekahsoft@CPE0008a20f982f-CM64777d666260.cpe.net.cable.rogers.com) (Remote host closed the connection)
2020-09-19 07:48:54 <edwardk> where you may have to traverse (const Nothing) -- over both of those to close them and match whatever types hasType expects or generalize hasType to Expr a and Val a with Eq
2020-09-19 07:49:32 × toorevitimirp quits (~tooreviti@117.182.182.33) (Client Quit)
2020-09-19 07:50:07 → kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz)
2020-09-19 07:50:40 <siraben> Why would traverse (const Nothing) close them?
2020-09-19 07:50:53 → rekahsoft joins (~rekahsoft@CPE0008a20f982f-CM64777d666260.cpe.net.cable.rogers.com)
2020-09-19 07:51:07 <phadej> :t foldMap (const Nothing) []
2020-09-19 07:51:08 <lambdabot> Semigroup a => Maybe a
2020-09-19 07:51:16 <phadej> :t traverse (const Nothing) []
2020-09-19 07:51:18 <lambdabot> Maybe [b]
2020-09-19 07:51:23 <phadej> :t traverse (const Nothing) "foobar"
2020-09-19 07:51:25 <lambdabot> Maybe [b]
2020-09-19 07:51:27 <phadej> traverse (const Nothing) "foobar"
2020-09-19 07:51:31 <phadej> > traverse (const Nothing) "foobar"
2020-09-19 07:51:34 <lambdabot> Nothing
2020-09-19 07:51:35 <phadej> > traverse (const Nothing) []
2020-09-19 07:51:38 <lambdabot> Just []
2020-09-19 07:51:50 <phadej> "there is no 'a'"
2020-09-19 07:52:02 × jedws quits (~jedws@121.209.139.222) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-19 07:52:27 <phadej> recall, that in `bound` 'a' is a type of free variables
2020-09-19 07:52:40 <phadej> if there is no 'a', there is no free variables -> expression is closed
2020-09-19 07:52:53 → toorevitimirp joins (~tooreviti@117.182.182.33)
2020-09-19 07:53:09 <phadej> ('a' in 'Expr a')
2020-09-19 07:53:39 × gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 260 seconds)
2020-09-19 07:54:02 → jedws joins (~jedws@121.209.139.222)
2020-09-19 07:54:06 → bahamas joins (~lucian@unaffiliated/bahamas)
2020-09-19 07:54:30 <siraben> traverse (const Nothing) (lam 0 $ Var 0) :: Maybe (Expr b)
2020-09-19 07:54:30 <siraben> for me
2020-09-19 07:54:36 <siraben> Result is Just (Lam (Scope (Var (B ()))))
2020-09-19 07:54:48 × kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 260 seconds)
2020-09-19 07:54:52 <edwardk> yes
2020-09-19 07:54:54 <edwardk> that is a closed term
2020-09-19 07:54:54 <phadej> yes, \x.x is closed
2020-09-19 07:55:03 <edwardk> try it with lam 0 $ Var 1
2020-09-19 07:55:06 <edwardk> and it'll bail with Nothing
2020-09-19 07:55:30 <siraben> Ah I see
2020-09-19 07:55:33 <edwardk> but if it succeeds, because the term is closed, you can use it as Expr a for any a you like
2020-09-19 07:55:45 × jneira_ quits (~jneira@80.30.101.206) (Ping timeout: 240 seconds)
2020-09-19 07:55:46 <edwardk> that way you can work 'conveniently' with strings while parsing
2020-09-19 07:55:50 <edwardk> and then switch to integers
2020-09-19 07:56:00 <edwardk> or just passing around types during typechecking
2020-09-19 07:57:00 → dansho joins (~dansho@ip68-108-167-185.lv.lv.cox.net)
2020-09-19 07:57:20 <siraben> Hm, maybe this implementation of lambda pi is bugged? It was written in 2014
2020-09-19 07:57:25 <edwardk> i think so
2020-09-19 07:57:33 <siraben> I can't seem to get \x → x to have the polymorphic type
2020-09-19 07:57:36 <edwardk> i don't have Control.Monad.Gen in scope, what is that from?
2020-09-19 07:57:45 <siraben> monad-gen
2020-09-19 07:58:09 <edwardk> well, to make a polymorphic if you'd have to pass the argument first
2020-09-19 07:58:09 × jedws quits (~jedws@121.209.139.222) (Client Quit)
2020-09-19 07:58:40 <edwardk> id :: Pi(A:*). A -> A
2020-09-19 07:58:40 × bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 258 seconds)
2020-09-19 07:59:18 <edwardk> so you need two Pis and two lambdas, this language lacks implicit vs. explicit lambdas/pis.
2020-09-19 08:00:07 <siraben> Well, time to read elaboration-zoo then. hm.
2020-09-19 08:00:08 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-19 08:00:10 <edwardk> id = \_ a. a -- needs to ignore its first arg
2020-09-19 08:00:27 <siraben> What if I want fully explicit lambdas and pis?
2020-09-19 08:00:35 <siraben> What would that look like?
2020-09-19 08:00:49 <edwardk> id :: pi (a : star). pi (_ : a). a
2020-09-19 08:00:59 <edwardk> id = \_. \a. a
2020-09-19 08:01:04 <siraben> ((A :: *) (x :: A). x) :: Pi (A :: *). a
←Prev  Next→
Page 1 .. 63 64 65 66 67 68 69 70 71 72 73 .. 5022

All times are in UTC.