Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 381 382 383 384 385 386 387 388 389 390 391 .. 5022
— 502,152 events total
2020-10-03 04:41:45 <hololeap> ski: what does that mean?
2020-10-03 04:42:14 → day_ joins (~Unknown@unaffiliated/day)
2020-10-03 04:42:16 <ski> it means that you could possibly have `Bar T0 = Bar T1', for two different types `T0' and `T1'
2020-10-03 04:42:19 <c_wraith> instance Foo Int where Bar Int = () ; instance Foo Bool where Bar Bool = ()
2020-10-03 04:43:14 <ski> so, if you're passing something of type `Bar T0' to `foo', and say that `Bar T0 = String'. then it you also have `Bar T1 = String', and so it doesn't know whether to use the `Foo T0' or the `Foo T1' instance (which may give different implementations for `foo')
2020-10-03 04:43:36 <hololeap> so, since there could be multiple instances of Foo which define the same Bar, there is no way to determine the Foo, given a Bar?
2020-10-03 04:43:50 <ski> (that is, you're actually passing `String' to `foo', and it can't decide whether you mean `Foo T0' or `Foo T1')
2020-10-03 04:43:53 <c_wraith> Not by inference, anyway
2020-10-03 04:43:55 × borne quits (~fritjof@200116b86454500007933c164a08810c.dip.versatel-1u1.de) (Ping timeout: 240 seconds)
2020-10-03 04:44:08 <c_wraith> You can use -XTypeApplications
2020-10-03 04:44:14 <hololeap> c_wraith: it yells at me just with the class definition
2020-10-03 04:44:15 <ski> you could declare `Bar' to be an associated `data' type. then it'd be injective
2020-10-03 04:44:36 <c_wraith> yes, you need to allow the class, too
2020-10-03 04:44:42 <ski> or, you could add an FD on it, to declare that it must be injective (prohibiting having both `Foo T0' and `Foo T1' as instances)
2020-10-03 04:45:05 × day quits (~Unknown@unaffiliated/day) (Ping timeout: 240 seconds)
2020-10-03 04:45:05 day_ is now known as day
2020-10-03 04:45:10 <hololeap> ski: what would that look like in this case?
2020-10-03 04:46:04 → borne joins (~fritjof@200116b864ada80031152e74c90dd565.dip.versatel-1u1.de)
2020-10-03 04:46:29 <hololeap> are you saying have something like `class Foo a bar | a -> bar ...`
2020-10-03 04:47:06 <ski> class Foo a where {type Bar a = b | b -> a; foo :: Bar a -> Maybe Bool}
2020-10-03 04:47:31 <hololeap> oh, i didn't know you could use functional dependencies on type families in a class
2020-10-03 04:47:31 × da39a3ee5e6b4b0d quits (~textual@n11211935170.netvigator.com) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-03 04:48:04 → da39a3ee5e6b4b0d joins (~textual@n11211935170.netvigator.com)
2020-10-03 04:49:02 <ski> (if one could use the usual FD syntax, it would have looked like `class Foo a | (Bar a) -> a where ..'. but that's not allowed syntax. an FD `x y -> z' means `z' is functionally determined by `x' and `y', not by `x' applied to `y')
2020-10-03 04:49:36 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-10-03 04:49:43 <ski> anyway, of course you could instead use `class Foo a bar_a | bar_a -> a where bar :: bar_a -> Maybe Bool', if you want to go for MPTC with FD
2020-10-03 04:51:00 <hololeap> so `b -> a` in FD terms means that each `b` must have exactly one `a` (thus ensuring injectivity)
2020-10-03 04:51:51 <ski> (and, as i said, you could have done `class Foo a where data Bar a; foo :: Bar a -> Maybe Bool}'. but then you couldn't make synonyms in some instances)
2020-10-03 04:52:01 <ski> hololeap : no, at most one
2020-10-03 04:52:25 <hololeap> right, since some b's may not have a typeclass associated with them
2020-10-03 04:52:44 <hololeap> or, that particular typeclass
2020-10-03 04:53:06 <hololeap> they may not have an instance of the given typeclass associated with them
2020-10-03 04:53:59 <ski> if you have `class Blah a b c | a -> b where ...', then the FD here logically means `forall a. unique b. exists c. Blah a b' (by `unique' i mean "exists at most one"), which is logically equivalent to `forall a b0 b1 c0 c1. (Blah a b0 c0,Blah a b1 c1) => b0 = b1'
2020-10-03 04:54:29 → nan` joins (nan`@gateway/vpn/privateinternetaccess/nan/x-47321016)
2020-10-03 04:54:42 <ski> iow, if two instances of `Blah' agrees in the `a' parameter position, then they've got to also agree in the `b' parameter position (or else you're not allowed to have both instances at the same time)
2020-10-03 04:55:27 × da39a3ee5e6b4b0d quits (~textual@n11211935170.netvigator.com) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-03 04:56:18 <hololeap> so, `class Foo a b | b -> a ...` `instance Foo Int String` `instance Foo Bool String`
2020-10-03 04:56:21 <hololeap> would not be allowed
2020-10-03 04:56:25 × elliott_ quits (~elliott_@pool-108-28-204-229.washdc.fios.verizon.net) (Ping timeout: 240 seconds)
2020-10-03 04:56:27 <ski> right
2020-10-03 04:57:25 <hololeap> okiedoke. this opens up a new world of GHC yelling at me. thanks :)
2020-10-03 04:57:55 <hololeap> (not sarcastic, though tongue in cheek)
2020-10-03 04:58:01 <ski> so practical effects of FDs are two. (a) not being allowed to have such instances at the same time, which would violate the FD; and (b), if during type inference/checking, it has derived that `Blah a b0 c0' and also `Blah a b1 c1' holds, then it knows that `b0' and `b1' must be equal, so it goes on to unify them directly
2020-10-03 04:58:43 <ski> if there's no `c' part, then that in turns means that it can simplify the constraint `(Blah a b0,Blah a b1)' to just `Blah a b'
2020-10-03 04:59:10 → raul782 joins (~raul782@190.237.41.123)
2020-10-03 04:59:44 <ski> and, this unification of `b0' and `b1' typically manifests itself as getting less ambiguous types, less need for explicitly informing the type system that, yes, you'd like this `b' over here to actually be the same as that `b' over there
2020-10-03 05:00:03 → xerox_ joins (~xerox@unaffiliated/xerox)
2020-10-03 05:00:04 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds)
2020-10-03 05:00:43 <ski> or, in your case, as allowing a signature that would otherwise be illegal, due to being ambiguous (no way to determine `a' from the argument and result type of `foo')
2020-10-03 05:00:50 → isovector1 joins (~isovector@172.103.216.166.cable.tpia.cipherkey.com)
2020-10-03 05:01:09 → elliott_ joins (~elliott_@pool-108-28-204-229.washdc.fios.verizon.net)
2020-10-03 05:01:36 × Jeanne-Kamikaze quits (~Jeanne-Ka@68.235.43.94) (Quit: Leaving)
2020-10-03 05:02:19 <hololeap> ski, why did you write `forall. a` earilier? wouldn't this signify that every possible type needs to have an instance of this class?
2020-10-03 05:02:33 <ski> no
2020-10-03 05:02:54 <ski> are you thinking about the `forall a. unique b. exists c. Blah a b' formulation, or the `forall a b0 b1 c0 c1. (Blah a b0 c0,Blah a b1 c1) => b0 = b1' formulation ?
2020-10-03 05:03:18 <hololeap> `forall a. unique b. exists c.`
2020-10-03 05:03:36 <hololeap> i put the period in the wrong place
2020-10-03 05:04:03 <ski> that reads as : for each type `a', there can be at most one type `b', such that for (at least) one type `c', we have an instance `Blah a b c'
2020-10-03 05:04:21 <hololeap> ok
2020-10-03 05:04:34 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
2020-10-03 05:04:46 <hololeap> i see what you're saying
2020-10-03 05:05:15 <ski> note that `unique b. ..b..'/"there can be at most one type `b', ..`b'.." is contravariant in `..b..'. so it's not demanding that `..b..' should hold, but rather placing a constraint on situations in which it does hold
2020-10-03 05:06:37 <ski> `unique b. ..b..' means `forall b0 b1. (..b0..,..b1..) => b0 = b1'. so `unique b. exists c. Blah a b c' means `forall b0 b1. (exists c. Blah a b0 c,exists c. Blah a b1 c) => b0 = b1'
2020-10-03 05:07:16 <hololeap> and `exists c.` just means that c needs to be defined, no other constraints
2020-10-03 05:07:18 <ski> so, `Blah ...' ends up not in the consequent (after the `=>'), but in the antecedent (before the `=>'), of the implication
2020-10-03 05:08:05 <hololeap> got it
2020-10-03 05:08:12 <hololeap> never had it explained that way before
2020-10-03 05:08:19 <ski> (and, in turn, `(exists c. Blah a b0 c,exists c. Blah a b1 c) => b0 = b1' becomes `(exists c0 c1. (Blah a b0 c0,Blah a b1 c1)) => b0 = b1', which becomes `forall c0 c1. (Blah a b0 c0,Blah b1 c1) => b0 = b1')
2020-10-03 05:09:05 <ski> "and `exists c.` just means that c needs to be defined, no other constraints" -- exactly. there just has to be some `c', we don't care which (can be different, for the two different instances that we're considering). `c' is irrelevant to the FD `a -> b'
2020-10-03 05:10:40 <ski> the same interpretation of FDs applies to relations/tables, in relational data base design (usually one thinks of this, when doing normalization of relations)
2020-10-03 05:12:54 <ski> (one can, similarly, do normalization of MPTCs with FDs. and i suppose also if you have ATs with injectivity annotations)
2020-10-03 05:13:25 × Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 240 seconds)
2020-10-03 05:14:38 → p0a joins (~user@unaffiliated/p0a)
2020-10-03 05:14:39 <p0a> Hello
2020-10-03 05:14:49 <p0a> is there a way to view documentation of the Main module in haddock?
2020-10-03 05:16:08 × raul782 quits (~raul782@190.237.41.123) (Read error: Connection reset by peer)
2020-10-03 05:16:27 × urodna quits (~urodna@unaffiliated/urodna) (Read error: Connection reset by peer)
2020-10-03 05:16:32 → ym555 joins (~ym@156.199.76.92)
2020-10-03 05:16:43 → raul782 joins (~raul782@190.237.41.123)
2020-10-03 05:17:14 → urodna joins (~urodna@unaffiliated/urodna)
2020-10-03 05:17:26 × JLP1 quits (~JLP@185.204.1.185) (Remote host closed the connection)
2020-10-03 05:17:54 × Saukk quits (~Saukk@2001:998:f1:3966:96a6:dee2:2e9:fdf3) (Remote host closed the connection)
2020-10-03 05:23:46 × ryansmccoy quits (~ryansmcco@156.96.151.132) (Ping timeout: 272 seconds)
2020-10-03 05:23:56 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-03 05:24:16 → ryansmccoy joins (~ryansmcco@193.37.254.27)
2020-10-03 05:26:13 → mmohammadi98126 joins (~mmohammad@2.178.147.205)
2020-10-03 05:28:25 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds)
2020-10-03 05:28:34 × nan` quits (nan`@gateway/vpn/privateinternetaccess/nan/x-47321016) (Quit: leaving)
2020-10-03 05:34:26 <p0a> I can see how the compiler catches bugs now with the type system
2020-10-03 05:34:50 <p0a> for example when you add fields to a type, the constructor will no longer match the signature
2020-10-03 05:35:16 <p0a> whereas in C you can get silent compilations with uninitialized data
2020-10-03 05:35:35 <p0a> and even if the code is correct, you still need to dig up all such occurences and fix them.
2020-10-03 05:35:36 → skorgon joins (~skorgon@217.146.82.202)
2020-10-03 05:36:17 <dsal> You can totally have uninitialized fields in haskell types. :)
2020-10-03 05:36:34 <dsal> It's a bad idea, but occasionally it's useful.
2020-10-03 05:37:33 × urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna)
2020-10-03 05:38:25 → CMCDragonkai1 joins (~Thunderbi@124.19.3.250)
2020-10-03 05:38:56 → snakemasterflex joins (~snakemast@213.100.206.23)
2020-10-03 05:40:39 × CMCDragonkai1 quits (~Thunderbi@124.19.3.250) (Client Quit)
2020-10-03 05:40:55 <p0a> dsal: Okay but (X y z) messes up when you change X to three fields, right? :)
←Prev  Next→
Page 1 .. 381 382 383 384 385 386 387 388 389 390 391 .. 5022

All times are in UTC.