Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 .. 5022
— 502,152 events total
2020-11-15 22:24:00 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-11-15 22:24:19 <boom> the prof rewrote this expression as λx.(λy.((x z) y))
2020-11-15 22:24:31 <boom> he said something about priority
2020-11-15 22:25:11 <koz_> boom: Most explanations of the lambda calculus define what binds more tightly than what.
2020-11-15 22:25:12 <moet> i guess he's trying to teach you the associativity of application
2020-11-15 22:25:16 <koz_> This is called 'precedence'.
2020-11-15 22:25:33 <koz_> I would recommend looking at whatever source for its syntax you got given closely - this is usually somewhat buried.
2020-11-15 22:25:53 <moet> yeah, it's very important to fully parenthesize an expression to avoid this ambiguity..
2020-11-15 22:25:55 <koz_> The main reason is to avoid having to explicitly parenthesise everything.
2020-11-15 22:27:19 × robert___ quits (uid452915@gateway/web/irccloud.com/x-lmflebnllvyjwmec) (Quit: Connection closed for inactivity)
2020-11-15 22:27:50 → conal joins (~conal@64.71.133.70)
2020-11-15 22:28:00 <boom> I was told that s t1 ... tn ... = (... (s,t1)...)tn and the application has priority over the abstraction
2020-11-15 22:28:28 <koz_> OK, so let's follow that through.
2020-11-15 22:29:00 → Kave joins (54126924@84.18.105.36)
2020-11-15 22:29:18 <boom> I'm saying to myself, in my formula what is s, t1 ?
2020-11-15 22:29:18 × jneira_ quits (~jneira@198.red-176-83-81.dynamicip.rima-tde.net) (Read error: Connection reset by peer)
2020-11-15 22:29:21 <koz_> Since application has priority, \x\y x z y is really \x\y (x z y)
2020-11-15 22:29:37 → jneira_ joins (~jneira@192.red-2-137-106.dynamicip.rima-tde.net)
2020-11-15 22:29:42 <koz_> Then, by the first rule, we have \x\y (x z y) is really \x\y ((x z) y).
2020-11-15 22:29:52 × dcoutts_ quits (~duncan@33.14.75.194.dyn.plus.net) (Remote host closed the connection)
2020-11-15 22:30:11 <koz_> Then, by the first rule again, we have that \x\y ((x z) y) is really \x (\y ((x z) y))
2020-11-15 22:30:19 → dcoutts_ joins (~duncan@33.14.75.194.dyn.plus.net)
2020-11-15 22:30:32 × Kave quits (54126924@84.18.105.36) (Remote host closed the connection)
2020-11-15 22:30:40 <boom> Ok why is x y z part oif the application, I would expect only z and y to be part of it
2020-11-15 22:30:42 <boom> ?
2020-11-15 22:30:57 <koz_> Because there's nothing else it could possibly be.
2020-11-15 22:31:20 <koz_> In order to have anything other than application, you either have to have another \ there.
2020-11-15 22:31:25 <koz_> (or lambda symbol, same diff)
2020-11-15 22:31:28 → Lycurgus joins (~niemand@cpe-45-46-134-163.buffalo.res.rr.com)
2020-11-15 22:31:50 <koz_> If you have a b c d e f g h i j k ...., all applications.
2020-11-15 22:33:02 × shutdown_-h_now quits (~arjan@2001:1c06:2d0b:2312:d540:265f:6057:f956) (Ping timeout: 264 seconds)
2020-11-15 22:33:27 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-11-15 22:33:36 <koz_> Actually, I was slightly wrong - that last step isn't actually the first rule.
2020-11-15 22:34:01 <koz_> The first rule there is application-related only based on your description.
2020-11-15 22:35:52 <boom> in s t1 ... tn ... = (... (s,t1)...)tn is there a difference between s and the ts ?
2020-11-15 22:36:02 <boom> t1, t2 ...
2020-11-15 22:36:02 <boom> ?
2020-11-15 22:36:03 → o1lo01ol1o joins (~o1lo01ol1@bl11-140-216.dsl.telepac.pt)
2020-11-15 22:36:11 <koz_> boom: In what sense do you mean 'is there a difference'?
2020-11-15 22:36:20 <koz_> I'm not sure I understand your question.
2020-11-15 22:36:24 <boom> are these all terms ?
2020-11-15 22:36:36 <koz_> Yes.
2020-11-15 22:36:46 <koz_> Because in the lambda calculus there isn't anything else.
2020-11-15 22:39:15 × LKoen_ quits (~LKoen@9.253.88.92.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”)
2020-11-15 22:39:28 → shutdown_-h_now joins (~arjan@2001:1c06:2d0b:2312:190f:5fcb:2d71:58b)
2020-11-15 22:40:03 <boom> Ok, so \x.s is the abstraction. If I understand correctly this is like saying that s is and epression that depends on x, am I corrcect?
2020-11-15 22:40:26 <boom> an expression*
2020-11-15 22:40:36 × o1lo01ol1o quits (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) (Ping timeout: 256 seconds)
2020-11-15 22:40:44 <koz_> I'm not sure what you mean by that. \x . s is a lambda, correct. If by 'expression' you mean 'term', then the answer is 'it depends on what s is'.
2020-11-15 22:41:04 <koz_> You can have \x . y, which is totally fine, and then nothing depends on x at all.
2020-11-15 22:41:30 <boom> ok so what does \x . y mean ?
2020-11-15 22:41:33 → mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de)
2020-11-15 22:41:40 <boom> I'm not sure i've understood
2020-11-15 22:41:44 <koz_> boom: We're not in the world of 'meaning' yet at all.
2020-11-15 22:42:07 <koz_> \x . y is a lambda abstraction, whose body is y.
2020-11-15 22:42:15 <koz_> In my case, 'y' is a free variable.
2020-11-15 22:42:35 <koz_> In this case, nothing depends on anything.
2020-11-15 22:42:43 <boom> ok
2020-11-15 22:43:07 → conal joins (~conal@64.71.133.70)
2020-11-15 22:43:11 <koz_> If you had '\x . y x', then you can kind of argue that when you apply '\x . y x' to something, the _result_ of the application depends on the argument.
2020-11-15 22:43:46 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-11-15 22:43:56 <koz_> For example: '(\x . y x) z' is an application, which reduces to 'y z'.
2020-11-15 22:44:20 <koz_> However, '(\x . y) z' reduces to 'y', (\x . y) foobar' reduces to 'y', etc.
2020-11-15 22:45:14 <boom> so here when you write \x .y x here what is the body of the lambda expression ?
2020-11-15 22:45:19 <boom> is it y x
2020-11-15 22:45:19 <boom> ?
2020-11-15 22:45:31 <boom> or is it y and then you apply x
2020-11-15 22:45:32 <boom> ?
2020-11-15 22:45:32 <koz_> '\x . y x' has the body 'y x'.
2020-11-15 22:45:49 <koz_> This has nothing to do with applying anything - it's a question of form.
2020-11-15 22:46:08 <boom> ok so anything after the dot is part of the body ?
2020-11-15 22:46:15 → conal joins (~conal@64.71.133.70)
2020-11-15 22:46:41 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-11-15 22:47:02 <koz_> boom: An abstraction has the form \VAR . BODY. I wrote them in caps to show that they stand for (respectively) an arbitrary variable and an arbitrary term.
2020-11-15 22:47:22 <MarcelineVQ> var sometimes called head
2020-11-15 22:47:33 <koz_> Yep!
2020-11-15 22:47:56 → conal joins (~conal@64.71.133.70)
2020-11-15 22:48:38 <boom> VAR and BODY can be any term or varibale ?
2020-11-15 22:48:51 <koz_> VAR can be any variable. BODY can be any term.
2020-11-15 22:50:01 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-11-15 22:50:37 <boom> so if I go back to λx.λy.x z y Is λy.x z y the body of the abstraction λx ?
2020-11-15 22:50:43 → conal joins (~conal@64.71.133.70)
2020-11-15 22:50:44 <koz_> Correct!
2020-11-15 22:51:15 × MarcelineVQ quits (~anja@198.254.202.72) (Remote host closed the connection)
2020-11-15 22:51:19 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-11-15 22:52:05 × Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer)
2020-11-15 22:52:10 → conal joins (~conal@64.71.133.70)
2020-11-15 22:52:25 → MarcelineVQ joins (~anja@198.254.202.72)
2020-11-15 22:53:17 × conal quits (~conal@64.71.133.70) (Client Quit)
2020-11-15 22:53:33 <moet> oof, trying to use ((*) :: Nat -> Nat -> Nat) from GHC.TypeLits ...
2020-11-15 22:53:47 <moet> since it collides with * (the kind of concrete types) ...
2020-11-15 22:53:54 × jneira_ quits (~jneira@192.red-2-137-106.dynamicip.rima-tde.net) (Remote host closed the connection)
2020-11-15 22:54:07 <koz_> moet: You probably want to import Data.Kind (Type) and use 'Type' instead of '*'.
2020-11-15 22:54:25 <moet> koz_: i'm trying to refer to the Nat level multiply
2020-11-15 22:54:33 <moet> and ghc keeps thinking i'm talking aout Type
2020-11-15 22:54:52 <koz_> Did you enable TypeOperators?
2020-11-15 22:54:54 <MarcelineVQ> Do you have/need TypeOperators on?
2020-11-15 22:54:57 <moet> yes
2020-11-15 22:55:08 <koz_> moet: Could you pastebin the exact error message?
2020-11-15 22:55:16 <moet> let's see.. how do we do this with the bot again
←Prev  Next→
Page 1 .. 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 .. 5022

All times are in UTC.