Logs: liberachat/#haskell
| 2021-07-31 08:44:17 | × | hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-07-31 08:45:46 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-31 08:45:59 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-31 08:48:15 | <Drew[m]> | Say you want `F t` to be type `X` when `t` is in class `A`, and type `Y` when `t` is in class `B`... what happens when it is in both? |
| 2021-07-31 08:48:31 | × | nate3 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 2021-07-31 08:49:01 | <mastarija> | Drew[m], I get the first class? |
| 2021-07-31 08:49:28 | <mastarija> | Sorry, first type |
| 2021-07-31 08:50:31 | → | Gurkenglas joins (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) |
| 2021-07-31 08:52:11 | <mastarija> | Drew[m], I was thinking in terms of how pattern matching work. Basically, which class matches first, I get it's related type |
| 2021-07-31 08:53:07 | <mastarija> | type family Typer e where Typer (e instanceof Show) = Int; Typer (e instanceof Monoid) = Char; etc... |
| 2021-07-31 08:55:21 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2021-07-31 08:55:46 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-31 08:55:53 | → | Vajb joins (~Vajb@2001:999:62:1d53:26b1:6c9b:c1ed:9c01) |
| 2021-07-31 08:56:35 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-31 08:56:58 | × | agua quits (~agua@2804:18:70:7597:1:0:6e99:2d6f) (Ping timeout: 240 seconds) |
| 2021-07-31 08:57:09 | → | curiousgay joins (~curiousga@77-120-186-48.kha.volia.net) |
| 2021-07-31 08:57:18 | <Drew[m]> | So with associated type families you can ofc make a class with an associated type family and make an instance of that type family for a whole class buut there is problems with that, since all it takes is a second instance for a whole class to get ambiguity |
| 2021-07-31 08:57:40 | × | Codaraxis quits (~Codaraxis@user/codaraxis) (Remote host closed the connection) |
| 2021-07-31 08:57:55 | <Drew[m]> | I'm currently reading up on non-associated type families because I'm rusty |
| 2021-07-31 08:58:00 | → | Codaraxis joins (~Codaraxis@user/codaraxis) |
| 2021-07-31 08:58:21 | <mastarija> | Associated ones are defined withing the Class, right? |
| 2021-07-31 08:58:30 | <Drew[m]> | Yes |
| 2021-07-31 08:59:31 | → | agua joins (~agua@2804:14c:8793:8e2f:ecd5:11e0:50a0:f2fe) |
| 2021-07-31 09:00:05 | <mastarija> | Btw, it says (if I'm reading it correctly) in the GHC manual that type variables declared in instance scope over the methods. |
| 2021-07-31 09:00:15 | <mastarija> | But for my case it doesn't seem to work |
| 2021-07-31 09:00:35 | <mastarija> | instance forall k. Applicative (Wrong k) where pure = mypure @k |
| 2021-07-31 09:00:42 | <mastarija> | mypure :: forall k a. k => a -> Wrong k a |
| 2021-07-31 09:01:11 | <tomsmeding> | ScopedTypeVariables? |
| 2021-07-31 09:01:17 | <mastarija> | Enabled |
| 2021-07-31 09:01:45 | <mastarija> | tomsmeding, it says "Could not deduce: k arising from a use of `mypure'" |
| 2021-07-31 09:02:29 | <tomsmeding> | what happens if you write 'mypure @_ @k' instead of 'mypure @k' |
| 2021-07-31 09:02:54 | <tomsmeding> | i.e. are you sure about the type variable order in the forall of mypure :p |
| 2021-07-31 09:03:06 | × | neceve quits (~quassel@2a02:c7f:607e:d600:f762:20dd:304e:4b1f) (Ping timeout: 240 seconds) |
| 2021-07-31 09:03:06 | <mastarija> | Expected a type, but `k' has kind `Constraint' |
| 2021-07-31 09:03:16 | <mastarija> | Which is what I'd expect... |
| 2021-07-31 09:03:18 | <tomsmeding> | ah yes |
| 2021-07-31 09:03:30 | <tomsmeding> | do you have a small reproducing example? |
| 2021-07-31 09:03:37 | <mastarija> | Sure, just a sec |
| 2021-07-31 09:03:58 | <tomsmeding> | (sounds like just the definition of Wrong and that instance) |
| 2021-07-31 09:05:12 | <mastarija> | tomsmeding, https://gist.github.com/mastarija/af03154c0d85fd78782f07ff6aeef98e |
| 2021-07-31 09:08:31 | <tomsmeding> | error disappears if I change the kind of 'k' to Type |
| 2021-07-31 09:08:58 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-31 09:09:11 | <mastarija> | yes, but I want k to be a Constraint... |
| 2021-07-31 09:09:18 | <tomsmeding> | I know :p |
| 2021-07-31 09:09:30 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-31 09:09:51 | <mastarija> | xD |
| 2021-07-31 09:10:02 | → | neceve joins (~quassel@2a02:c7f:607e:d600:f762:20dd:304e:4b1f) |
| 2021-07-31 09:10:10 | <tomsmeding> | error also disappears if you remove the 'k =>' in the signature of mypure |
| 2021-07-31 09:10:20 | <tomsmeding> | (at the cost of introducing an error in its body, of course) |
| 2021-07-31 09:10:45 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-31 09:11:01 | <tomsmeding> | error also disappears if you _add_ 'k =>' in the instance head! |
| 2021-07-31 09:11:34 | <tomsmeding> | which makes perfect sense -- ghc can't deduce k because, indeed, it cannot satisfy the constraint -- not because it can't find an instance of the type variable |
| 2021-07-31 09:11:45 | <mastarija> | oohh... |
| 2021-07-31 09:11:49 | <tomsmeding> | and then you don't even need the @k anymore |
| 2021-07-31 09:12:05 | <tomsmeding> | and you can also just write 'pure = Inert' |
| 2021-07-31 09:12:06 | <mastarija> | Oooooooohhhhhhh.... |
| 2021-07-31 09:12:25 | <mastarija> | Damn, how did I miss that :D |
| 2021-07-31 09:12:28 | <tomsmeding> | :) |
| 2021-07-31 09:12:37 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-07-31 09:13:38 | → | __monty__ joins (~toonn@user/toonn) |
| 2021-07-31 09:14:00 | <tomsmeding> | (and the 'forall k.' is unnecessary in the instance head, for completeness) |
| 2021-07-31 09:15:51 | <tomsmeding> | the error message has unfortunate overlap with the error message indicating that ghc can't figure out what a particular type variable should be, though |
| 2021-07-31 09:15:59 | <tomsmeding> | or at least, I was deceived for a while :p |
| 2021-07-31 09:16:07 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-07-31 09:16:13 | <tomsmeding> | or would that be 'ambiguous type variable'... |
| 2021-07-31 09:16:58 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-31 09:18:05 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-31 09:18:12 | <mastarija> | tomsmeding, do you know if there is a way to write a constraint which says that a kind of something is a Type? |
| 2021-07-31 09:18:35 | <mastarija> | something like (kind e ~ Type) |
| 2021-07-31 09:18:43 | <tomsmeding> | mastarija: how would that even sort-check |
| 2021-07-31 09:18:55 | <mastarija> | Not sure what that is D: |
| 2021-07-31 09:19:03 | <mastarija> | Oh.. sort |
| 2021-07-31 09:19:08 | <tomsmeding> | type kind sort |
| 2021-07-31 09:19:17 | <mastarija> | yes, I remembered now :D |
| 2021-07-31 09:19:49 | <tomsmeding> | hm, isn't Constraint really equal to Type in ghc haskell |
| 2021-07-31 09:19:57 | <tomsmeding> | and there is TypeInType |
| 2021-07-31 09:20:21 | <mastarija> | Now that you mention it... |
| 2021-07-31 09:20:28 | <tomsmeding> | I don't think there is a 'kind' function like you wrote, but using a well-placed kind signature, you should be able to get the kind as a variable in scope |
| 2021-07-31 09:20:32 | <tomsmeding> | and then you can just use ~ I think |
| 2021-07-31 09:26:46 | × | azeem quits (~azeem@176.200.191.24) (Ping timeout: 250 seconds) |
| 2021-07-31 09:27:46 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-31 09:27:55 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-31 09:28:46 | → | azeem joins (~azeem@176.200.191.24) |
| 2021-07-31 09:30:08 | → | burnsidesLlama joins (~burnsides@dhcp168-019.wadham.ox.ac.uk) |
| 2021-07-31 09:32:19 | → | dunj3 joins (~dunj3@2001:981:9d95:1:886d:656c:9636:23f4) |
| 2021-07-31 09:33:54 | × | curiousgay quits (~curiousga@77-120-186-48.kha.volia.net) (Ping timeout: 265 seconds) |
| 2021-07-31 09:34:07 | <mastarija> | So yeah... why doesn't this work? (((c:: Type -> Constraint) (e::Type)) ~ Constraint) |
| 2021-07-31 09:37:09 | <mastarija> | Nwm |
| 2021-07-31 09:40:37 | → | nate3 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-31 09:41:08 | × | azeem quits (~azeem@176.200.191.24) (Ping timeout: 272 seconds) |
| 2021-07-31 09:44:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-31 09:45:34 | × | nate3 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-31 09:46:05 | → | euouae joins (~euouae@user/euouae) |
| 2021-07-31 09:46:35 | <nshepperd2> | forall k (t :: k). (k ~ Type) => ...? |
| 2021-07-31 09:48:43 | <mastarija> | nshepperd2, huh.. didn't know about that syntax, thx |
| 2021-07-31 09:52:03 | <euouae> | What's the tunes.org-style logging? |
| 2021-07-31 09:52:07 | <euouae> | It's in the /topic |
| 2021-07-31 09:53:10 | <nshepperd2> | i think even just k being inhabited (t :: k) implies that k is necessarily TYPE r for some r :: RuntimeRep |
| 2021-07-31 09:53:52 | <nshepperd2> | wait no, that's wrong nvm |
| 2021-07-31 09:54:09 | <nshepperd2> | it's t being inhabited that implies that :D |
All times are in UTC.