Newest at the top
| 2024-09-23 07:20:34 +0200 | <c_wraith> | So GHC treats the two type variables as interchangeable |
| 2024-09-23 07:20:20 +0200 | <c_wraith> | Yeah. When you match on Eq.Refl, it adds (a ~ b) to the context |
| 2024-09-23 07:19:24 +0200 | <Axman6> | it's not, it's all happening at the type system. But we know that if we received _anything_ of type a :~: b, then it could only have been a value of Refl, which requires that a ~ b, so we've been given evidence that those types are the same. Then we call refl at the type a to produce a := a. The argument is unused, but its type is used |
| 2024-09-23 07:17:27 +0200 | <Axman6> | (someone please jump in if I'm completely wrong here) |
| 2024-09-23 07:17:21 +0200 | <lambdaRule> | I still don't see how the input (a :~: b) is used anywhere to get to the result |
| 2024-09-23 07:17:08 +0200 | <Axman6> | but we're being specific about which a, it's the same a that the argument to toLeibniz had (and :~: is evidence that a ~ b, so we can produce a := b, a.k.a a := a) |
| 2024-09-23 07:16:17 +0200 | <Axman6> | that's what refl does, it produces something of type a := a |
| 2024-09-23 07:15:56 +0200 | <Axman6> | (uh, I guess x :: Int :~: Int; x = Refl, but yo uknow what I mean) |
| 2024-09-23 07:15:43 +0200 | <lambdaRule> | ok, how do we get to a := b from this call? |
| 2024-09-23 07:14:09 +0200 | <Axman6> | toLeibniz even |
| 2024-09-23 07:13:53 +0200 | <Axman6> | if we had x = Int :~: Int, then toLiebnitz x would become refl @Int |
| 2024-09-23 07:12:57 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 276 seconds) |
| 2024-09-23 07:12:38 +0200 | <Axman6> | so in toLeibniz :: forall a b. (a :~: b) -> (a := b) when we use refl @a, we're specifically saying we want to call refl with a being _the same `a`_ as our call to toLeibniz |
| 2024-09-23 07:12:00 +0200 | <lambdaRule> | right |
| 2024-09-23 07:11:32 +0200 | <Axman6> | refl :: forall a. a := a, right? |
| 2024-09-23 07:11:05 +0200 | <c_wraith> | the @a is on a use of refl, not Refl |
| 2024-09-23 07:11:03 +0200 | <Axman6> | what's the full type of refl, including forall? |
| 2024-09-23 07:10:43 +0200 | <lambdaRule> | I don't see why type a would work |
| 2024-09-23 07:10:29 +0200 | <lambdaRule> | the hole after Refl should be: forall c. c a -> c b |
| 2024-09-23 07:10:28 +0200 | <lambdaRule> | Refl _ |
| 2024-09-23 07:10:28 +0200 | <lambdaRule> | from what I understand, the expected return type is a:=b, so a := b |
| 2024-09-23 07:09:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-23 07:04:45 +0200 | <c_wraith> | ah, why did he reuse the constructor name? I don't expect Refl to have an argument! |
| 2024-09-23 07:04:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 07:03:53 +0200 | <geekosaur> | `a` is the expected type. The `@` indicates a type application https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_applications.html |
| 2024-09-23 07:02:50 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-09-23 07:02:42 +0200 | <lambdaRule> | I see that "refl = Refl id" so refl expects Refl constructor with a functor like argument. how does "a" fit the expected type? |
| 2024-09-23 06:59:54 +0200 | billchenchina- | (~billchenc@113.57.152.160) |
| 2024-09-23 06:59:44 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Ping timeout: 244 seconds) |
| 2024-09-23 06:58:38 +0200 | <lambdaRule> | Hi, I am confused in this piece of code: "toLeibniz Eq.Refl = refl @a" in the section "Equivalence of Leibniz and propositional equality" (https://ryanglscott.github.io/2021/08/22/leibniz-equality-in-haskell-part-1/), how does it work on the right hand side? |
| 2024-09-23 06:55:19 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-09-23 06:54:53 +0200 | lambdaRule | (~lambdaRul@node-1w7jr9phpv013mevadflg9a0e.ipv6.telus.net) |
| 2024-09-23 06:53:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-23 06:48:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 06:38:02 +0200 | doyougnu | (~doyougnu@syn-045-046-170-068.res.spectrum.com) |
| 2024-09-23 06:37:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-23 06:37:46 +0200 | doyougnu | (~doyougnu@syn-045-046-170-068.res.spectrum.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-09-23 06:32:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 06:25:16 +0200 | michalz | (~michalz@185.246.207.205) |
| 2024-09-23 06:22:55 +0200 | son0p | (~ff@186.121.41.9) (Ping timeout: 264 seconds) |
| 2024-09-23 06:21:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-23 06:17:09 +0200 | foul_owl | (~kerry@185.219.141.162) |
| 2024-09-23 06:17:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 06:06:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-23 06:04:03 +0200 | foul_owl | (~kerry@174-21-143-250.tukw.qwest.net) (Ping timeout: 276 seconds) |
| 2024-09-23 06:01:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 05:59:09 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
| 2024-09-23 05:54:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-23 05:50:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 05:46:20 +0200 | yellowbean | (~yellowbea@awork087050.netvigator.com) (Remote host closed the connection) |