Logs: liberachat/#haskell
| 2021-06-30 16:37:33 | × | rachel231 quits (~scratchyo@c-73-142-199-151.hsd1.nh.comcast.net) (Quit: Connection closed) |
| 2021-06-30 16:37:34 | <Boarders> | has anyone come across this issue? |
| 2021-06-30 16:38:29 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 2021-06-30 16:39:36 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2021-06-30 16:44:59 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-06-30 16:48:18 | × | mpt quits (~tom@2a02:908:1862:49e0::4) (Ping timeout: 240 seconds) |
| 2021-06-30 16:48:18 | × | jippiedoe quits (~david@2a02-a44c-e14e-1-ae15-1a10-43d7-2299.fixed6.kpn.net) (Ping timeout: 240 seconds) |
| 2021-06-30 16:48:41 | → | stevenxl_ joins (~stevenlei@c-73-45-168-220.hsd1.il.comcast.net) |
| 2021-06-30 16:50:42 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-06-30 16:51:00 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-30 16:51:28 | × | stevenxl quits (~stevenlei@174.128.182.118) (Ping timeout: 252 seconds) |
| 2021-06-30 16:52:27 | → | jao joins (jao@gateway/vpn/protonvpn/jao) |
| 2021-06-30 16:52:35 | × | nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2021-06-30 16:55:54 | × | peterhil quits (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) (Ping timeout: 240 seconds) |
| 2021-06-30 16:59:47 | → | hegstal joins (~hegstal@2a02:c7f:7604:8a00:1749:70f2:c3b4:7591) |
| 2021-06-30 17:00:01 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-30 17:01:09 | → | acidjnk_new joins (~acidjnk@p200300d0c72b954061d05013652ae098.dip0.t-ipconnect.de) |
| 2021-06-30 17:06:08 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) (Remote host closed the connection) |
| 2021-06-30 17:06:51 | fendor__ | is now known as fendor |
| 2021-06-30 17:11:32 | <janus> | Boarders: is it installed with ghcup? |
| 2021-06-30 17:11:37 | → | buddha joins (~buddha@27.147.234.193) |
| 2021-06-30 17:11:55 | <buddha> | hi |
| 2021-06-30 17:12:05 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-30 17:12:05 | <janus> | hi buddha |
| 2021-06-30 17:12:30 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-06-30 17:12:41 | <buddha> | what is the diff between `x = 10` and `let x = 10`? |
| 2021-06-30 17:12:42 | <janus> | namo buddhaya |
| 2021-06-30 17:13:27 | <janus> | buddha: you can think of your module as one giant let |
| 2021-06-30 17:13:46 | <Rembane> | buddha: in ghci or in a module? |
| 2021-06-30 17:13:53 | <buddha> | in the ghci |
| 2021-06-30 17:14:11 | <dminuoso> | I dont think there's a difference in GHCi |
| 2021-06-30 17:14:25 | <dminuoso> | Except, for MMR perhaps |
| 2021-06-30 17:14:47 | <buddha> | are they referring to the same thing? |
| 2021-06-30 17:15:05 | <Rembane> | They mean the same thing, some major versions ago you had to write `let x = 10', but now you can skip the let. |
| 2021-06-30 17:15:13 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-30 17:15:30 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-06-30 17:15:39 | <buddha> | both of them represent a function right? |
| 2021-06-30 17:15:48 | <dminuoso> | No |
| 2021-06-30 17:15:53 | <buddha> | a function that returns 10? no? |
| 2021-06-30 17:15:55 | <dminuoso> | Just the binding of a value to a name. |
| 2021-06-30 17:16:04 | <Rembane> | No, they give a name to a value |
| 2021-06-30 17:16:20 | <buddha> | how do you define functions without arguments then? |
| 2021-06-30 17:16:23 | <dminuoso> | (Or well, more precisely I should say it binds an expression to a name) |
| 2021-06-30 17:16:27 | <janus> | do functions always have arrows in their type signatures? |
| 2021-06-30 17:16:33 | <dminuoso> | buddha: That fundamentally does not make sense. |
| 2021-06-30 17:16:39 | × | zgrep quits (~zgrep@user/zgrep) (Quit: It's a quitter's world.) |
| 2021-06-30 17:16:54 | <dminuoso> | In Haskell we use the term function differently from other programming languages |
| 2021-06-30 17:17:00 | → | stevenxl joins (~stevenlei@68.235.43.165) |
| 2021-06-30 17:17:03 | <dminuoso> | Our use is more aligned with that of mathematics, where a function is just a mapping of values |
| 2021-06-30 17:17:13 | <Rembane> | janus: Assume yes, and come back here when you find out otherwise. :) |
| 2021-06-30 17:17:30 | × | alx741 quits (~alx741@186.178.109.202) (Ping timeout: 252 seconds) |
| 2021-06-30 17:17:33 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-30 17:17:37 | <buddha> | so by definition a function has to have at least one argument? |
| 2021-06-30 17:17:44 | <janus> | Rembane: is the exception that you can make (->) instances for anything? |
| 2021-06-30 17:17:45 | <dminuoso> | More to the point, exactly one argument. |
| 2021-06-30 17:17:56 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 2021-06-30 17:17:57 | <janus> | % :info (->) |
| 2021-06-30 17:17:58 | <yahb> | janus: type (->) :: * -> * -> *; type (->) = FUN 'Many :: * -> * -> *; -- Defined in `GHC.Types'; infixr -1 ->; instance forall r. Applicative ((->) r) -- Defined in `GHC.Base'; instance forall r. Functor ((->) r) -- Defined in `GHC.Base'; instance forall r. Monad ((->) r) -- Defined in `GHC.Base'; instance forall b a. Monoid b => Monoid (a -> b) -- Defined in `GHC.Base'; instance forall b a. Semigroup b => S |
| 2021-06-30 17:18:02 | → | zgrep joins (~zgrep@user/zgrep) |
| 2021-06-30 17:18:05 | <buddha> | what happens when you have multiple arguments then? |
| 2021-06-30 17:18:07 | <dminuoso> | buddha: A function that appears to take say 2 arguments, is rather a function that returns a function. |
| 2021-06-30 17:18:16 | <dminuoso> | buddha: There's two ways to deal with that |
| 2021-06-30 17:18:17 | <Rembane> | janus: Yes, and also that there are many ways to represent a function. |
| 2021-06-30 17:18:27 | <dminuoso> | Either we have the function take a product type, like a type, e.g. f :: (Int, Char) -> Bool |
| 2021-06-30 17:18:40 | <dminuoso> | Or we encode the function curried as: f' :: Int -> Char -> Bool |
| 2021-06-30 17:18:41 | × | stevenxl_ quits (~stevenlei@c-73-45-168-220.hsd1.il.comcast.net) (Read error: Connection reset by peer) |
| 2021-06-30 17:18:59 | <Rembane> | janus: F a b c could for instance be a function which you need another function to evaluate. |
| 2021-06-30 17:19:15 | <dminuoso> | Where curried just means f' is a function taking Int, and returning a function Char -> Bool. So applying this function `f 10 'c'` is actually considered `(f 10) 'c'` |
| 2021-06-30 17:19:43 | <dminuoso> | buddha: For convenience, we let you define what appears a multiple argument function, but this maps into "functions returning functions" behind the scenes. |
| 2021-06-30 17:19:58 | × | warnz quits (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) (Remote host closed the connection) |
| 2021-06-30 17:20:14 | <dminuoso> | i.e. `f x y = x + y` is equivalent to `f = \x -> \y -> x + y` |
| 2021-06-30 17:20:20 | × | slowButPresent quits (~slowButPr@user/slowbutpresent) (Ping timeout: 258 seconds) |
| 2021-06-30 17:20:32 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-30 17:20:46 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2021-06-30 17:21:21 | <janus> | when you say equivalent, what do you mean? surely the 9.0 change in subsumption would not consider eta expansion equivalent? |
| 2021-06-30 17:21:27 | → | warnz joins (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) |
| 2021-06-30 17:21:31 | <buddha> | and functions are lexically scoped? |
| 2021-06-30 17:21:50 | × | warnz quits (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) (Client Quit) |
| 2021-06-30 17:22:05 | → | slowButPresent joins (~slowButPr@user/slowbutpresent) |
| 2021-06-30 17:22:07 | → | stevenxl_ joins (~stevenlei@c-73-45-168-220.hsd1.il.comcast.net) |
| 2021-06-30 17:22:16 | <dminuoso> | buddha: Up until the module system, yes. |
| 2021-06-30 17:22:35 | <dminuoso> | janus: I mean it in the same way we teach children that the path of planets around the sun is a circle. |
| 2021-06-30 17:22:45 | ← | pragma- parts (~chaos@user/pragmatic-chaos) (Bye!) |
| 2021-06-30 17:22:50 | × | stevenxl quits (~stevenlei@68.235.43.165) (Ping timeout: 256 seconds) |
| 2021-06-30 17:22:50 | <janus> | ah ok, is this "fast and loose reasoning" ? |
| 2021-06-30 17:23:08 | <dminuoso> | No, it's a good enough approximation for pedagocal reasons that's close enough to the truth as fas as they are concerned. |
| 2021-06-30 17:23:13 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-06-30 17:24:07 | <janus> | i thought that change in subsumption only matter in the precense of undefined, which makes it a non-total language |
| 2021-06-30 17:24:25 | <janus> | the fast and loose paper talks about totality, so that is why i thought it was the relevant paper |
| 2021-06-30 17:24:26 | <dminuoso> | janus: So the subsumption stuff is related in a particular sense. |
| 2021-06-30 17:25:01 | <dminuoso> | janus: But its not because of subsumption, but for the reason simplified subsumption is introduced. But the relationship is very distance. |
| 2021-06-30 17:25:06 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-06-30 17:25:28 | × | waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Client Quit) |
| 2021-06-30 17:25:41 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-30 17:25:54 | <dminuoso> | In case of the simplified subsumption, its because `x` and \y -> x y` are not the same, but in order for GHC to elaborate certain RankNTypes situations into core, it has to transform one into the other, changing how strictness behaves. |
| 2021-06-30 17:26:25 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 265 seconds) |
| 2021-06-30 17:26:48 | × | stevenxl_ quits (~stevenlei@c-73-45-168-220.hsd1.il.comcast.net) (Ping timeout: 256 seconds) |
| 2021-06-30 17:26:51 | <dminuoso> | So the solution is to just forbid things like deep skolemnization, and suddenly GHC no longer has to do that. But in order for these programs to type check, you have to write that conversion from `x` to `\y -> x y` in the places GHC used to do it by hand now. |
| 2021-06-30 17:27:02 | → | stevenxl joins (~stevenlei@68.235.43.157) |
| 2021-06-30 17:27:08 | <dminuoso> | So this change in semantics is made explicit now, while simplifying GHC's type checker at the same time |
All times are in UTC.