Logs: freenode/#haskell
| 2021-03-29 17:59:22 | → | idhugo__ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-03-29 18:00:19 | × | xourt quits (d4c620ea@212-198-32-234.rev.numericable.fr) (Quit: Connection closed) |
| 2021-03-29 18:00:21 | ← | drakonis parts (~drakonis@unaffiliated/drakonis) ("WeeChat 3.1") |
| 2021-03-29 18:01:25 | <infinisil> | I have a GADT like `data Method i o where IsRoot :: Method Int Bool GetName :: Method Int String` |
| 2021-03-29 18:02:40 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 2021-03-29 18:03:00 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:b98b:75b0:1d5d:7be4) |
| 2021-03-29 18:03:05 | <infinisil> | Now I want to be able to have a `Show` instance for something like `ReqResp (Method i o) i o` |
| 2021-03-29 18:03:28 | <infinisil> | data ReqResp i o = ReqResp (Method i o) i o |
| 2021-03-29 18:03:32 | → | pupuupup_ joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 2021-03-29 18:04:36 | <tomsmeding> | infinisil: use StandaloneDeriving, write 'deriving instance Show (Method i o)', and attach 'deriving (Show)' to ReqResp? |
| 2021-03-29 18:04:39 | <infinisil> | Now I can't just `derive Show`, but that gives me an `instance (Show i, Show o) => Show (ReqResp i o)` |
| 2021-03-29 18:04:44 | <infinisil> | s/can't/can |
| 2021-03-29 18:06:39 | <infinisil> | I want an instance like `Show (ReqResp i o)`, without any dependent constraints |
| 2021-03-29 18:06:39 | <tomsmeding> | infinisil: I don't think you can derive an unconstrained Show instance for ReqResp automatically |
| 2021-03-29 18:06:46 | <infinisil> | Hmm |
| 2021-03-29 18:07:08 | <infinisil> | Yeah currently I'm doing it manually. My question indeed would've been how that could be automated |
| 2021-03-29 18:07:08 | → | electricityZZZZ joins (~electrici@135-180-3-82.static.sonic.net) |
| 2021-03-29 18:07:36 | <Gurkenglas> | tomsmeding, isn't the following absence of overlapping instances just the injective type classes you want? |
| 2021-03-29 18:07:39 | <Gurkenglas> | @let class Gurk a; instance Gurk Int; instance Gurk b => Gurk (a -> b) |
| 2021-03-29 18:07:41 | <lambdabot> | Defined. |
| 2021-03-29 18:07:43 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-29 18:07:48 | <tomsmeding> | infinisil: well you could do it using generics but not sure whether that's better :p |
| 2021-03-29 18:07:57 | <Gurkenglas> | :t undefined :: Gurk (String -> Char) => () |
| 2021-03-29 18:07:59 | <lambdabot> | error: |
| 2021-03-29 18:07:59 | <lambdabot> | No instance for (Gurk Char) |
| 2021-03-29 18:07:59 | <lambdabot> | arising from an expression type signature |
| 2021-03-29 18:08:08 | <Gurkenglas> | As you see, it looked directly for the Gurk Char instance |
| 2021-03-29 18:08:14 | → | geekosaur joins (82650c7a@130.101.12.122) |
| 2021-03-29 18:08:40 | ← | dmoerner parts (~dmoerner@fedora/dmoerner) ("WeeChat 1.9.1") |
| 2021-03-29 18:08:41 | <tomsmeding> | :t undefined :: Gurk (a -> b) => () |
| 2021-03-29 18:08:43 | <lambdabot> | error: |
| 2021-03-29 18:08:43 | <lambdabot> | • Overlapping instances for Gurk (a0 -> b0) |
| 2021-03-29 18:08:43 | <lambdabot> | Matching givens (or their superclasses): |
| 2021-03-29 18:08:48 | <tomsmeding> | that's the problem |
| 2021-03-29 18:09:00 | <tomsmeding> | wait what, why overlappign |
| 2021-03-29 18:09:14 | <tomsmeding> | anyway that doesn't work :p |
| 2021-03-29 18:09:33 | <Gurkenglas> | @let class Gurk2 a; instance Gurk2 b => Gurk2 (a -> b) |
| 2021-03-29 18:09:35 | <lambdabot> | Defined. |
| 2021-03-29 18:09:43 | <Gurkenglas> | :t undefined :: Gurk2 (a -> b) => () |
| 2021-03-29 18:09:44 | <lambdabot> | error: |
| 2021-03-29 18:09:44 | <lambdabot> | • Overlapping instances for Gurk2 (a0 -> b0) |
| 2021-03-29 18:09:44 | <lambdabot> | Matching givens (or their superclasses): |
| 2021-03-29 18:09:49 | <Gurkenglas> | ruh roh |
| 2021-03-29 18:10:18 | × | gitgood quits (~gitgood@80-44-12-39.dynamic.dsl.as9105.com) (Remote host closed the connection) |
| 2021-03-29 18:10:29 | → | DTZUZU_ joins (~DTZUZO@207.81.119.43) |
| 2021-03-29 18:10:36 | <tomsmeding> | wait now I can't reproduce it locally, let me have a look |
| 2021-03-29 18:11:38 | <Gurkenglas> | @let class Gurk4 a; instance Gurk4 (a -> b) |
| 2021-03-29 18:11:39 | <lambdabot> | Defined. |
| 2021-03-29 18:11:41 | <tomsmeding> | okay apparently the introduction of GADTs complicates the matter |
| 2021-03-29 18:11:47 | <Gurkenglas> | :t undefined :: Gurk4 (a -> b) => () |
| 2021-03-29 18:11:48 | <lambdabot> | error: |
| 2021-03-29 18:11:48 | <lambdabot> | • Overlapping instances for Gurk4 (a0 -> b0) |
| 2021-03-29 18:11:48 | <lambdabot> | Matching givens (or their superclasses): |
| 2021-03-29 18:11:50 | <Gurkenglas> | RUH ROH |
| 2021-03-29 18:12:12 | <tomsmeding> | @let data Thing a where Tup :: a -> b -> Thing (a -> b) |
| 2021-03-29 18:12:14 | <lambdabot> | Defined. |
| 2021-03-29 18:12:28 | <tomsmeding> | @let foo :: Gurk4 a => a -> Int ; foo = undefined |
| 2021-03-29 18:12:29 | <lambdabot> | Defined. |
| 2021-03-29 18:12:41 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 246 seconds) |
| 2021-03-29 18:12:43 | <tomsmeding> | @let bar :: Gurk4 a => Thing a -> Int ; bar (Tup x y) = foo y |
| 2021-03-29 18:12:44 | <lambdabot> | .L.hs:174:17: error: |
| 2021-03-29 18:12:45 | <lambdabot> | • Could not deduce (Gurk4 b) arising from a use of ‘foo’ |
| 2021-03-29 18:12:45 | <lambdabot> | from the context: Gurk4 a |
| 2021-03-29 18:13:02 | <tomsmeding> | this is the exact issue I'm talking about, not sure what the "overlapping instances" is about |
| 2021-03-29 18:14:20 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-03-29 18:14:36 | <infinisil> | Maybe I could derive a Show instance automatically for |
| 2021-03-29 18:14:38 | <infinisil> | data ReqResp m = forall i o. m ~ Method i o => ReqResp m i o |
| 2021-03-29 18:14:50 | <infinisil> | Something with QuantifiedConstraints |
| 2021-03-29 18:16:08 | <infinisil> | Or maybe for |
| 2021-03-29 18:16:10 | <infinisil> | data ReqResp (m :: Method i o) = ReqResp i o |
| 2021-03-29 18:16:44 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 2021-03-29 18:16:49 | <infinisil> | That kinda works |
| 2021-03-29 18:16:51 | × | shailangsa quits (~shailangs@host86-186-136-70.range86-186.btcentralplus.com) (Ping timeout: 246 seconds) |
| 2021-03-29 18:16:53 | <infinisil> | deriving instance Show (ReqResp 'IsRoot) |
| 2021-03-29 18:16:59 | <infinisil> | deriving instance Show (ReqResp 'GetName) |
| 2021-03-29 18:17:11 | <infinisil> | The method is lifted to the type level, but maybe that's fine for me |
| 2021-03-29 18:17:13 | × | rajivr quits (uid269651@gateway/web/irccloud.com/x-nlktifqfsuwtyuzw) (Quit: Connection closed for inactivity) |
| 2021-03-29 18:17:17 | <tomsmeding> | infinisil: the problem is that if the Method is on the value level, you need to explicitly pattern match on it to obtain the Show dictionaries |
| 2021-03-29 18:17:37 | <tomsmeding> | in fact, at runtime, that's _necessary_, because otherwise the runtime doesn't know what 'show' method to call |
| 2021-03-29 18:17:55 | <infinisil> | Yeah, but it could theoretically be derived automatically still |
| 2021-03-29 18:20:26 | <Gurkenglas> | dolio, what do you mean by Σ? I can find Ω on https://ncatlab.org/nlab/show/truth+value but not Σ |
| 2021-03-29 18:27:50 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-29 18:30:41 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 2021-03-29 18:31:04 | → | dpl_ joins (~dpl@77.121.78.163) |
| 2021-03-29 18:31:22 | <tomsmeding> | Gurkenglas: I believe the "overlapping instances" error is a side effect of writing a context mentioning variables 'a', 'b', without the constrained type (here '()') also mentioning them |
| 2021-03-29 18:31:33 | → | gitgood joins (~gitgood@80-44-12-39.dynamic.dsl.as9105.com) |
| 2021-03-29 18:32:56 | × | kuribas quits (~user@ptr-25vy0i9nyhjns61vpxg.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2021-03-29 18:33:03 | <infinisil> | I want to write `makeRequest :: forall (method :: Method i o) i o. ...` |
| 2021-03-29 18:33:21 | <infinisil> | So that I can e.g. do `makeRequest @IsRoot` |
| 2021-03-29 18:33:37 | <infinisil> | But this doesn't work, because `i` and `o` aren't in scope when `method` is defined |
| 2021-03-29 18:33:57 | <infinisil> | And if I do `forall i o (method :: Method i o)`, I won't be able to do `makeRequest @IsRoot` |
| 2021-03-29 18:34:05 | <infinisil> | Is there a solution for this? |
| 2021-03-29 18:34:17 | <dolio> | Gurkenglas: Σ is the Sierpinski space. |
| 2021-03-29 18:34:21 | <Gurkenglas> | dolio, can't one see () as Ω? One need merely admit that () is the terminal object, and then true: * -> Ω is id, and every (mono)morphism m: U -> X is the pullback of true and (\x:X -> if x is above m ⊥ then () else ⊥), yes? |
| 2021-03-29 18:34:51 | → | knupfer joins (~Thunderbi@dynamic-046-114-145-192.46.114.pool.telefonica.de) |
| 2021-03-29 18:36:00 | <dolio> | If () is Ω then it isn't also the terminal object. |
| 2021-03-29 18:36:29 | <tomsmeding> | infinisil: makeRequest @_ @_ @IsRoot, or do `makeRequest :: Proxy (Method i o) -> ...` and write `makeRequest (Proxy @IsRoot) ...` |
| 2021-03-29 18:36:57 | <infinisil> | Yeah that's a workaround, but I wonder if `makeRequest @IsRoot` can be made to work |
| 2021-03-29 18:37:15 | <infinisil> | Seems so simple |
| 2021-03-29 18:37:45 | <dolio> | Anyhow, domain theory is not the right setting for having these kind of distinctions, I think. |
All times are in UTC.