Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→
Page 1 .. 221 222 223 224 225 226 227 228 229 230 231 .. 17971
— 1,797,070 events total
2021-06-01 10:40:03 <dminuoso> I recall the ghc proposal
2021-06-01 10:40:23 <nshepperd> % :t C
2021-06-01 10:40:23 <yahb> nshepperd: forall {b} {ev :: b ~ Int}. b -> C b
2021-06-01 10:40:48 <dminuoso> % :t C String
2021-06-01 10:40:48 <yahb> dminuoso: ; <interactive>:1:3: error:; * Data constructor not in scope: String; * Perhaps you meant one of these: `StringL' (imported from Language.Haskell.TH), variable `string' (imported from Text.Parsec), `Strict' (imported from Control.Lens)
2021-06-01 10:40:51 <dminuoso> % :t C "foo"
2021-06-01 10:40:51 <yahb> dminuoso: C String
2021-06-01 10:40:58 <nshepperd> ???
2021-06-01 10:41:17 <boxscape> % :k C String
2021-06-01 10:41:17 <yahb> boxscape: (String ~ Int) => *
2021-06-01 10:41:32 <dminuoso> {ev :: b ~ Int}
2021-06-01 10:41:34 <dminuoso> What is that even saying?
2021-06-01 10:41:41 <boxscape> err
2021-06-01 10:42:01 <boxscape> pass a dictionary with an equality constraint?
2021-06-01 10:42:11 <boxscape> (I'm kind of wondering where the ev name comes from)
2021-06-01 10:42:22 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds)
2021-06-01 10:42:24 <dminuoso> boxscape: wouldn't that rather be written as `b ~ Int =>`?
2021-06-01 10:42:35 <boxscape> yeah but I guess that's sort of the same thing in core
2021-06-01 10:42:40 <dminuoso> this thing is quantified over ev, whose type is (!) b ~ Int
2021-06-01 10:42:44 <dminuoso> I have no clue what that means
2021-06-01 10:43:09 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-06-01 10:43:09 <boxscape> I mean you can't write it, so it's questionable whether it means anything
2021-06-01 10:43:16 <nshepperd> pass a promoted constraint evidence as a type variable, lol
2021-06-01 10:43:24 → haskman joins (~haskman@171.48.41.1)
2021-06-01 10:43:24 <dminuoso> lol
2021-06-01 10:44:12 <dminuoso> Well, but wouldnt I be able to write
2021-06-01 10:44:19 <nshepperd> also how does it even refer to b when the type variables in the declaration didn't even match up
2021-06-01 10:44:45 <dminuoso> nshepperd: that's not a problem
2021-06-01 10:44:52 <boxscape> okay "ev" means "evidence"
2021-06-01 10:45:10 <dminuoso> boxscape: So I guess your assumption about "pass a dictionary with an equality cosntraint" is right
2021-06-01 10:45:15 → thiross joins (~user@173.242.113.143.16clouds.com)
2021-06-01 10:45:17 <dminuoso> Or it seems reasonable
2021-06-01 10:45:21 <dminuoso> but the type signature still looks off
2021-06-01 10:45:27 <boxscape> oh yeah absolutely
2021-06-01 10:45:36 <nshepperd> except it's a promoted dictionary, which is nonsense
2021-06-01 10:45:39 <dminuoso> as that should rahter read `forall b. b ~ Int => b -> C b`
2021-06-01 10:46:06 → hmmmas joins (~chenqisu1@183.217.202.217)
2021-06-01 10:46:06 <dminuoso> Is this some subtle bug?
2021-06-01 10:47:08 <boxscape> probably
2021-06-01 10:47:12 <nshepperd> dminuoso: isn't it a problem? where is it getting that the type variable which has to be ~ Int, is the same type variable as the first parameter of C? that's not written anywhere
2021-06-01 10:47:25 <dminuoso> nshepperd: its from the standalone signature
2021-06-01 10:47:34 <dminuoso> % type C :: forall b -> (b ~ Int) => *; data C a = C a deriving Show
2021-06-01 10:47:34 <yahb> dminuoso:
2021-06-01 10:47:51 <nshepperd> right, b is not a
2021-06-01 10:47:54 <dminuoso> boxscape: curious, is the visible dependent qualifier necessary? why cant we use `forall b.`?
2021-06-01 10:47:58 <dminuoso> nshepperd: that's irrelevant
2021-06-01 10:48:07 <dminuoso> nshepperd: its not in the same scope
2021-06-01 10:48:14 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds)
2021-06-01 10:48:18 <nshepperd> that doesn't help
2021-06-01 10:48:25 <boxscape> nshepperd it's the same because it's the first parameter to C, in the standalone kind signature and in its definition
2021-06-01 10:48:32 <dminuoso> similar to how you could write: `id :: forall a. a -> a; id @b c = c`
2021-06-01 10:48:46 <boxscape> % type D :: forall b . (b ~ Int) => *; data D a = MkD a deriving Show
2021-06-01 10:48:46 <yahb> boxscape: ; <interactive>:57:38: error:; * Not a function kind: *; but extra binders found: a; * In the data type declaration for `D'
2021-06-01 10:48:53 <nshepperd> hmm
2021-06-01 10:48:59 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-06-01 10:49:08 <dminuoso> boxscape: this diagnostic reads really weird too
2021-06-01 10:49:12 <dminuoso> "not a function kind: *"
2021-06-01 10:49:29 <boxscape> % type D :: forall b . (b ~ Int) => *; data D @a = MkD a deriving Show -- I would almost expect this to work
2021-06-01 10:49:29 <yahb> boxscape: ; <interactive>:59:46: error:; Unexpected type application @a; In the data declaration for `D'
2021-06-01 10:49:32 <dminuoso> I think I understand why GHC says this.
2021-06-01 10:49:45 <dminuoso> Presumably with the chance, data declarations are *necessarily* visible dependent
2021-06-01 10:49:48 <dminuoso> *change
2021-06-01 10:49:53 × thiross quits (~user@173.242.113.143.16clouds.com) (Ping timeout: 252 seconds)
2021-06-01 10:51:24 <boxscape> hmm, not quite
2021-06-01 10:51:27 <boxscape> % :k Proxy
2021-06-01 10:51:27 <yahb> boxscape: k -> *
2021-06-01 10:51:36 × xff0x quits (~xff0x@2001:1a81:52ca:4f00:8a7f:8182:f670:e586) (Remote host closed the connection)
2021-06-01 10:51:43 <boxscape> this has both non-dependent visible and dependent invisible quantification
2021-06-01 10:51:52 → xff0x joins (~xff0x@2001:1a81:52ca:4f00:a77b:5731:d9ca:93c9)
2021-06-01 10:52:01 <boxscape> I think
2021-06-01 10:52:32 <boxscape> full kind is `forall k . k -> *`
2021-06-01 10:54:01 <dminuoso> % :set -fexplicit-forall
2021-06-01 10:54:01 <yahb> dminuoso: Some flags have not been recognized: -fexplicit-forall
2021-06-01 10:54:03 <dminuoso> uh
2021-06-01 10:54:17 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds)
2021-06-01 10:54:27 <dminuoso> % :set -fprint-explicit-foralls
2021-06-01 10:54:28 <yahb> dminuoso:
2021-06-01 10:54:30 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-06-01 10:54:31 <dminuoso> % :k Proxy
2021-06-01 10:54:31 <yahb> dminuoso: forall {k}. k -> *
2021-06-01 10:54:49 <dminuoso> boxscape: this looks very invisible to me
2021-06-01 10:55:02 <boxscape> yes, the k is inferred, invisible, and dependent
2021-06-01 10:55:05 <boxscape> the forall {k}
2021-06-01 10:55:12 <boxscape> but the `k ->` is visible and independent
2021-06-01 10:55:24 <dminuoso> uh
2021-06-01 10:55:26 <boxscape> or.. non-dependent, not sure
2021-06-01 10:55:43 × wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-06-01 10:55:52 <nshepperd> % :t Proxy
2021-06-01 10:56:13 <boxscape> I accidentally redefined the data constructor Proxy in a private yahb session I think fwiw :)
2021-06-01 10:56:22 <boxscape> but not sure why yahb isn't showing anything
2021-06-01 10:56:29 → aman joins (~aman@user/aman)
2021-06-01 10:56:54 <boxscape> % "yahb?"
2021-06-01 10:57:25 <nshepperd> RIP
2021-06-01 10:58:28 <dminuoso> 12:55:12 boxscape | but the `k ->` is visible and independent
2021-06-01 10:58:36 <dminuoso> boxscape: Are you sure here?>
2021-06-01 10:58:46 <boxscape> yep, 98%
2021-06-01 10:58:58 × yahb quits (xsbot@user/mniip/bot/yahb) (Ping timeout: 264 seconds)
2021-06-01 10:59:54 <boxscape> dminuoso from richard eisenberg's thesis: https://i.imgur.com/2XEl2Ls.png
2021-06-01 11:00:03 × favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat)
2021-06-01 11:01:19 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
←Prev  Next→
Page 1 .. 221 222 223 224 225 226 227 228 229 230 231 .. 17971

All times are in UTC.