Logs: liberachat/#haskell
| 2021-06-22 16:07:09 | ArsenArsen | is now known as Arsen |
| 2021-06-22 16:07:42 | Arsen | is now known as ArsenArsen |
| 2021-06-22 16:07:53 | → | moet joins (~moet@172.58.35.6) |
| 2021-06-22 16:09:30 | pragma- | is now known as garp |
| 2021-06-22 16:09:34 | garp | is now known as pragma- |
| 2021-06-22 16:10:47 | _________ | is now known as noodly |
| 2021-06-22 16:10:51 | noodly | is now known as __________ |
| 2021-06-22 16:11:01 | __________ | is now known as _________ |
| 2021-06-22 16:12:26 | → | safinaskar joins (~safinaska@109.252.90.89) |
| 2021-06-22 16:12:39 | <safinaskar> | why this code doesn't compile? https://paste.debian.net/1202044/ |
| 2021-06-22 16:13:06 | <safinaskar> | I see error: "Illegal equational constraint a ~ a (Use GADTs or TypeFamilies to permit this)" |
| 2021-06-22 16:13:20 | <safinaskar> | how GADTs and TypeFamilies are related to my code? |
| 2021-06-22 16:14:01 | <Cale> | They both need type equalities to work |
| 2021-06-22 16:14:33 | <Cale> | It's possible that there ought to be a third extension TypeEqualities that they both imply, but there isn't. |
| 2021-06-22 16:14:47 | <tomsmeding> | % proof :: forall (a :: *). (forall (x :: a). x :~: x) -> (forall (x :: a). x :~: x); proof _ = error "" -- safinaskar |
| 2021-06-22 16:14:48 | <yahb> | tomsmeding: |
| 2021-06-22 16:14:57 | <tomsmeding> | (note the _) |
| 2021-06-22 16:15:51 | hrnz | is now known as Henselierung |
| 2021-06-22 16:15:56 | × | hiruji quits (~hiruji@user/hiruji) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-06-22 16:16:13 | → | hiruji joins (~hiruji@user/hiruji) |
| 2021-06-22 16:16:16 | <safinaskar> | Cale: thanks |
| 2021-06-22 16:16:25 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-22 16:16:33 | <safinaskar> | tomsmeding: thanks. i already enabled typeimpredicativity, and it works |
| 2021-06-22 16:17:13 | × | hiruji quits (~hiruji@user/hiruji) (Client Quit) |
| 2021-06-22 16:17:17 | → | hounded_woodstoc joins (~hounded@2603-7000-da43-eccc-0000-0000-0000-0cec.res6.spectrum.com) |
| 2021-06-22 16:17:29 | → | hounded_1969 joins (~hounded@2603-7000-da43-eccc-0000-0000-0000-0cec.res6.spectrum.com) |
| 2021-06-22 16:17:32 | → | hiruji joins (~hiruji@user/hiruji) |
| 2021-06-22 16:18:11 | × | hiruji quits (~hiruji@user/hiruji) (Client Quit) |
| 2021-06-22 16:18:29 | → | hiruji joins (~hiruji@user/hiruji) |
| 2021-06-22 16:18:46 | <thyriaen> | i thought that the point of reduce & fold to use it on monoids so it doesnt matter in which order the operation is applied, why is there foldl foldr foldt - when i use it for + for example i dont care bout the order |
| 2021-06-22 16:18:48 | × | hounded_1969 quits (~hounded@2603-7000-da43-eccc-0000-0000-0000-0cec.res6.spectrum.com) (Client Quit) |
| 2021-06-22 16:20:05 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 272 seconds) |
| 2021-06-22 16:23:00 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-06-22 16:23:35 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 2021-06-22 16:23:39 | <Cale> | thyriaen: Not necessarily |
| 2021-06-22 16:24:03 | <Cale> | There are plenty of cases where the type of the result does not even match the type of elements in the list |
| 2021-06-22 16:24:27 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-22 16:25:47 | ← | safinaskar parts (~safinaska@109.252.90.89) () |
| 2021-06-22 16:25:54 | → | safinaskar joins (~safinaska@109.252.90.89) |
| 2021-06-22 16:25:56 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-06-22 16:26:01 | <safinaskar> | why this doesn't compile? https://paste.debian.net/1202047/ |
| 2021-06-22 16:27:00 | <Cale> | safinaskar: Because 3868 still hasn't gotten merged ;) |
| 2021-06-22 16:27:42 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 252 seconds) |
| 2021-06-22 16:27:43 | → | xkuru joins (~xkuru@user/xkuru) |
| 2021-06-22 16:27:50 | <safinaskar> | Cale: please, give a link |
| 2021-06-22 16:27:52 | × | xkuru quits (~xkuru@user/xkuru) (Remote host closed the connection) |
| 2021-06-22 16:28:01 | <Cale> | https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3868/ |
| 2021-06-22 16:28:14 | → | xkuru joins (~xkuru@user/xkuru) |
| 2021-06-22 16:28:31 | <Cale> | (I need to update some test outputs, and rebase it right now, as it happens...) |
| 2021-06-22 16:29:21 | <Cale> | safinaskar: Note that regardless, pr would be dead code, since you could never actually satisfy its constraint in order to use it |
| 2021-06-22 16:29:38 | <Cale> | But it's probable that this should merely be a warning. |
| 2021-06-22 16:30:35 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2021-06-22 16:31:07 | <Cale> | Oh, actually, I'm not even sure 3868 will save you here |
| 2021-06-22 16:31:22 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2021-06-22 16:32:13 | <Cale> | Haven't thought much about the case with QuantifiedConstraints... |
| 2021-06-22 16:33:24 | <safinaskar> | i changed type to this: "pr :: forall a. (forall b. a ~ b) => Int", and i still get same error |
| 2021-06-22 16:33:48 | <safinaskar> | but not this constraint is satisfable! |
| 2021-06-22 16:34:27 | <Cale> | That's still not going to be satisfiable... there's no type which is equal to every other type |
| 2021-06-22 16:34:36 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-06-22 16:35:35 | <Cale> | Did you just want forall a b. (a ~ b) => Int ? This is merely ambiguous. |
| 2021-06-22 16:35:55 | <Cale> | (since a and b are unused by the rest of the type) |
| 2021-06-22 16:36:19 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-22 16:38:14 | <Cale> | What behaviour do you get if you turn on AllowAmbiguousTypes by the way? |
| 2021-06-22 16:38:43 | → | Guest75 joins (~Guest75@166.70.242.157) |
| 2021-06-22 16:38:44 | <safinaskar> | Cale: "Did you just want forall a b. (a ~ b) => Int" - of course, no. My final goal is to compile this code: https://paste.debian.net/1202048/ |
| 2021-06-22 16:39:10 | <safinaskar> | Cale: i want to compile it to prove functor law from applicative laws |
| 2021-06-22 16:39:27 | <safinaskar> | Cale: i am curious whether this is possible using haskell type system |
| 2021-06-22 16:39:55 | <safinaskar> | so now i go through ghc errors which are show when i try to compile this code |
| 2021-06-22 16:40:20 | <Cale> | If it was possible, I still wouldn't trust the result :P |
| 2021-06-22 16:40:49 | <safinaskar> | Cale: why? |
| 2021-06-22 16:42:42 | <dminuoso> | Why is a proof of type inequality not something we can express? |
| 2021-06-22 16:43:28 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 252 seconds) |
| 2021-06-22 16:43:33 | × | fef quits (~thedawn@user/thedawn) (Remote host closed the connection) |
| 2021-06-22 16:43:33 | <Cale> | Well, maybe that's a little unfair, but we're using a whole bunch of type system features which haven't been around very long, and GHC's type checker is a giant and complicated beast. There's no shortage of weird bugs. |
| 2021-06-22 16:43:42 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-06-22 16:44:10 | → | fef joins (~thedawn@user/thedawn) |
| 2021-06-22 16:44:44 | → | peterhil_ joins (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) |
| 2021-06-22 16:44:49 | <Cale> | dminuoso: You want something like (a :~: b) -> Void ? |
| 2021-06-22 16:45:19 | × | peterhil quits (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2021-06-22 16:45:40 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-22 16:45:52 | <dminuoso> | Cale: No, Im just curious why we dont have something like (a :!~: b) |
| 2021-06-22 16:46:01 | <dminuoso> | I dont have any acute need, it's just curiosity |
| 2021-06-22 16:46:24 | <Cale> | You typically can't do very much with the information that two types are not equal |
| 2021-06-22 16:47:52 | <Cale> | Knowing that two types *are* equal lets you apply functions that operate on one of the types to values of the other, for example. |
| 2021-06-22 16:47:57 | → | hexfive joins (~eric@50.35.83.177) |
| 2021-06-22 16:48:07 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-22 16:48:16 | <Cale> | But knowing that they aren't equal doesn't really give you any additional permission that you wouldn't have otherwise had. |
| 2021-06-22 16:49:11 | × | hexfive quits (~eric@50.35.83.177) (Client Quit) |
| 2021-06-22 16:50:25 | <dminuoso> | Cale: Well but at the same time I do have something like (==) so I can express: (a == b) ~ 'False => ... |
| 2021-06-22 16:50:48 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 252 seconds) |
| 2021-06-22 16:50:48 | <dminuoso> | Is that not the same amount of information? |
| 2021-06-22 16:51:29 | <Cale> | I suppose, but what do you do with that? |
| 2021-06-22 16:51:55 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-06-22 16:52:51 | <Cale> | For something like a promoted data type, where you're pretending that Haskell is dependently typed and doing some sort of type level computations, doing inequality tests at the type level might make sense. |
| 2021-06-22 16:52:59 | <safinaskar> | dminuoso: try to express type inequality using this: (forall x. (a ~ b) => x). this essentially means a is not equal to b |
| 2021-06-22 16:53:28 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:e846:fcb5:a54b:afb8) |
| 2021-06-22 16:53:47 | → | Morrow_ joins (~MorrowM_@bzq-110-168-31-106.red.bezeqint.net) |
| 2021-06-22 16:54:20 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 258 seconds) |
| 2021-06-22 16:55:13 | <tomsmeding> | Cale: perhaps to exclude a particular branch in a case expression? |
| 2021-06-22 16:55:24 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
All times are in UTC.