Newest at the top
| 2024-09-23 08:35:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 08:35:19 +0200 | CiaoSen | (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) |
| 2024-09-23 08:35:13 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-09-23 08:34:34 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 2024-09-23 08:25:24 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 2024-09-23 08:24:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-23 08:24:40 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-23 08:24:00 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-09-23 08:18:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 08:07:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-23 08:02:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 07:57:02 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-23 07:56:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-23 07:55:19 +0200 | euleritian | (~euleritia@dynamic-176-007-153-048.176.7.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 2024-09-23 07:53:22 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb6581c435b27e22238d.dip0.t-ipconnect.de) |
| 2024-09-23 07:51:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 07:49:58 +0200 | youthlic | (~Thunderbi@user/youthlic) |
| 2024-09-23 07:48:03 +0200 | lambdaRule | (~lambdaRul@node-1w7jr9phpv013mevadflg9a0e.ipv6.telus.net) (Quit: Client closed) |
| 2024-09-23 07:47:51 +0200 | ChanServ | +v haskellbridge |
| 2024-09-23 07:47:51 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 2024-09-23 07:47:26 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2024-09-23 07:42:11 +0200 | ChanServ | +v haskellbridge |
| 2024-09-23 07:42:11 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 2024-09-23 07:41:47 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2024-09-23 07:41:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-23 07:41:19 +0200 | kuribas | (~user@ptr-17d51enh08wgcmf553y.18120a2.ip6.access.telenet.be) |
| 2024-09-23 07:39:35 +0200 | neuroevolutus | (~neuroevol@37.19.200.139) |
| 2024-09-23 07:35:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-23 07:34:54 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
| 2024-09-23 07:33:51 +0200 | billchenchina- | (~billchenc@113.57.152.160) (Ping timeout: 246 seconds) |
| 2024-09-23 07:31:48 +0200 | <Axman6> | that would have been better as a paste... |
| 2024-09-23 07:31:24 +0200 | <Axman6> | like data Expr a where Num :: Int -> Expr Int; Bool' :: Bool -> Expr Bool; Plus :: Expr a -> Expr a -> Expr a; Eq :: Eq a => Expr a -> Expr a -> Expr Bool. When you pattern match on eval :: Expr a -> a; eval e = case e of Eq a b -> eval a == eval b; ...; we've brought into scope that the two expressions represent something of the same type, and that those types have an Eq constraint so we can use == |
| 2024-09-23 07:30:22 +0200 | euleritian | (~euleritia@dynamic-176-007-153-048.176.7.pool.telefonica.de) |
| 2024-09-23 07:30:21 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:caad:a8df:b144:6c96) (Ping timeout: 246 seconds) |
| 2024-09-23 07:30:13 +0200 | <c_wraith> | all the work is being done in the type system with the GADTs |
| 2024-09-23 07:30:08 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-09-23 07:30:03 +0200 | <c_wraith> | It's really funny looking at everything in Data.Type.Equality with a definition like foo Refl = Refl or bar Refl Refl = Refl |
| 2024-09-23 07:28:55 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 265 seconds) |
| 2024-09-23 07:28:16 +0200 | <Axman6> | :~: is probably one of the more confusing common uses of GADTs, seeing the usual example of a simple expression tree is useful for understanding how each constructor carries some typoe information which gets exposed by pattern matching |
| 2024-09-23 07:26:50 +0200 | <lambdaRule> | Thanks a lot! c_wraith, Axman6, geekosaur. |
| 2024-09-23 07:24:07 +0200 | <c_wraith> | yes. Matching specifically that constructor brings that into scope. |
| 2024-09-23 07:23:47 +0200 | <lambdaRule> | so the key is a ~ b is the information bring into the scope by pattern matching the input |
| 2024-09-23 07:23:26 +0200 | <c_wraith> | yes, exactly |
| 2024-09-23 07:23:05 +0200 | <lambdaRule> | so the refl call with type a then compiler see that the expected type is a := b but since a ~ b so refl works |
| 2024-09-23 07:22:52 +0200 | <Axman6> | if* |
| 2024-09-23 07:22:36 +0200 | <Axman6> | Notice the definition of :~:: data a :~: b where Refl :: a :~: a -- you can only produce values of type a :~: b is a is equal to b |
| 2024-09-23 07:22:15 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-09-23 07:21:38 +0200 | <lambdaRule> | I see, it's getting clearer... |
| 2024-09-23 07:21:35 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) |
| 2024-09-23 07:21:08 +0200 | <c_wraith> | That's one of the main feature of GADTs, and not really in scope for that post. I think it expect you to know what they do already. |