Newest at the top
| 2025-05-03 22:16:02 +0200 | <r-sta> | errrr... idk which proposal is implemented, it might have just liked the dependant proposal for reference, i have too many new tabs open sorry |
| 2025-05-03 22:15:49 +0200 | <hellwolf> | which ones, I have used visible forall only |
| 2025-05-03 22:15:29 +0200 | <hellwolf> | I can use in 9.12? |
| 2025-05-03 22:14:59 +0200 | <r-sta> | yeah it was accepted in 9.12 thats why im reading it |
| 2025-05-03 22:14:48 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2025-05-03 22:13:02 +0200 | <hellwolf> | I still think Haskell should slowly but surely add these ... despite many push backs |
| 2025-05-03 22:12:36 +0200 | <hellwolf> | is the proposal still being worked on? |
| 2025-05-03 22:12:33 +0200 | erdem | (~null@user/erdem) erdem |
| 2025-05-03 22:12:11 +0200 | <r-sta> | im still not used to these visible quantifiers, especially in a continuation like that |
| 2025-05-03 22:12:01 +0200 | <int-e> | Note that I'm not really aware of what these proposals are. I'm just pretty good at skimming on demand :P |
| 2025-05-03 22:11:34 +0200 | hammond | (proscan@gateway04.insomnia247.nl) (Ping timeout: 276 seconds) |
| 2025-05-03 22:11:24 +0200 | <hellwolf> | int-e: thanks, that makes sense.I guess, sometimes AllowAmbiguousTypes forces to specify too if not enough injectivity around :p But that's besides the point. |
| 2025-05-03 22:11:19 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-03 22:11:19 +0200 | <int-e> | r-sta: I don't think so; you'll still have to use the Church trick for that, expressing an existential as (for(all|each) a -> r) -> r |
| 2025-05-03 22:10:19 +0200 | pavonia | (~user@user/siracusa) siracusa |
| 2025-05-03 22:10:10 +0200 | <r-sta> | int-e: does the new syntax allow that i can return differently annotated types depending on runtime behaviour? |
| 2025-05-03 22:10:06 +0200 | <int-e> | hellwolf: "We call a quantifier visible when the parameter must be specified at use sites, and invisible when the compiler tries to infer it at use sites." (So it's related to TypeApplications but different) |
| 2025-05-03 22:09:24 +0200 | <r-sta> | rather than expecting it to work "for all" types, i guess.... |
| 2025-05-03 22:09:08 +0200 | <r-sta> | you specify Nat as an argument |
| 2025-05-03 22:09:00 +0200 | <r-sta> | type TVis = PVis Nat 15 -- no inference |
| 2025-05-03 22:09:00 +0200 | <r-sta> | type TInv = PInv 15 -- infer (k~Nat) from (a::k)~(15::Nat) |
| 2025-05-03 22:08:44 +0200 | <r-sta> | hellwolf: type PVis :: forall k -> k -> Type -- visible quantification of 'k' |
| 2025-05-03 22:08:20 +0200 | <r-sta> | what the dependent outcome would be |
| 2025-05-03 22:08:13 +0200 | <r-sta> | because i couldnt infer from the types |
| 2025-05-03 22:08:10 +0200 | <hellwolf> | what does visibility mean here? since you can also use type variables without vdq? |
| 2025-05-03 22:07:59 +0200 | <r-sta> | ie i could return Vertex, but not Vertex Down |
| 2025-05-03 22:07:39 +0200 | <r-sta> | i had to erase them. like, it would return up or down from flat, but these couldnt have different type annotations |
| 2025-05-03 22:07:13 +0200 | <int-e> | yes |
| 2025-05-03 22:07:12 +0200 | <r-sta> | i had like a flippy thing for trading, it had 3 states up down flat, but i couldnt make a class with the singletons appearing at the output |
| 2025-05-03 22:06:44 +0200 | <r-sta> | type erasure is what means we dont need types at runtime right? |
| 2025-05-03 22:05:42 +0200 | Square | (~Square@user/square) (Remote host closed the connection) |
| 2025-05-03 22:05:39 +0200 | <r-sta> | int-e: ok cool thanks |
| 2025-05-03 22:05:34 +0200 | <r-sta> | like you have to specify the type... |
| 2025-05-03 22:05:08 +0200 | <int-e> | https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rs… says "The forall vs foreach part governs erasure: foralls are erased, while foreachs are retained." |
| 2025-05-03 22:04:08 +0200 | <r-sta> | "visible dependent quantification" |
| 2025-05-03 22:02:24 +0200 | Square | (~Square@user/square) Square |
| 2025-05-03 22:01:36 +0200 | <r-sta> | (i also dont understand what the arrow is doing there) |
| 2025-05-03 22:01:23 +0200 | <r-sta> | eg. foreach a -> ty |
| 2025-05-03 22:01:18 +0200 | Square | (~Square@user/square) (Remote host closed the connection) |
| 2025-05-03 22:01:08 +0200 | <r-sta> | i have never seen this before |
| 2025-05-03 22:01:02 +0200 | <r-sta> | it mentions foreach |
| 2025-05-03 22:00:58 +0200 | <r-sta> | im trying to read this https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst |
| 2025-05-03 22:00:58 +0200 | r-sta | (~r-sta@206-122-61-5.reverse.tnp.net.uk) |
| 2025-05-03 21:57:03 +0200 | la1n2 | (~la1n@176.59.162.120) (Read error: Connection reset by peer) |
| 2025-05-03 21:54:14 +0200 | la1n2 | (~la1n@176.59.162.120) |
| 2025-05-03 21:53:56 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-05-03 21:39:21 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-03 21:39:01 +0200 | euleritian | (~euleritia@dynamic-176-000-010-081.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-03 21:36:24 +0200 | euleritian | (~euleritia@dynamic-176-000-010-081.176.0.pool.telefonica.de) |
| 2025-05-03 21:35:27 +0200 | euleritian | (~euleritia@dynamic-176-006-129-007.176.6.pool.telefonica.de) (Ping timeout: 268 seconds) |