Newest at the top
| 2025-05-03 22:30:16 +0200 | <haskellbridge> | <loonycyborg> and treat them like two different sublanguages working in concert :P |
| 2025-05-03 22:30:00 +0200 | <haskellbridge> | <loonycyborg> I think it's better just to embrace this separation between term-level and type-level |
| 2025-05-03 22:29:46 +0200 | P1RATEZ | (piratez@user/p1ratez) P1RATEZ |
| 2025-05-03 22:26:31 +0200 | <EvanR> | maybe education will improve though |
| 2025-05-03 22:26:04 +0200 | <EvanR> | fundamental activities possible with dependent types won't be different |
| 2025-05-03 22:25:54 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-05-03 22:25:47 +0200 | <hellwolf> | *quit |
| 2025-05-03 22:25:44 +0200 | <hellwolf> | DT induced rage quite |
| 2025-05-03 22:25:24 +0200 | r-sta | (~r-sta@206-122-61-5.reverse.tnp.net.uk) (Quit: Client closed) |
| 2025-05-03 22:25:21 +0200 | <r-sta> | cioa! |
| 2025-05-03 22:25:19 +0200 | <r-sta> | sheesh, ill just check in in *another* few years to check the status of all this. |
| 2025-05-03 22:24:14 +0200 | <r-sta> | ("no types at runtime!! or else!! do you want this to compile or not!?) |
| 2025-05-03 22:23:51 +0200 | <r-sta> | ie im made to do the erasure myself! |
| 2025-05-03 22:23:39 +0200 | <r-sta> | i have to just use Vertex :: Type |
| 2025-05-03 22:23:12 +0200 | <r-sta> | if you can forgive the use of || at type level with that meaning |
| 2025-05-03 22:22:59 +0200 | <r-sta> | i have like, flipFromFlat) :: Vertex Flat -> (Vertex Up || Vertex Down) |
| 2025-05-03 22:21:56 +0200 | <hellwolf> | Not sure if I am explaining it well. I kept it brief. |
| 2025-05-03 22:21:56 +0200 | <hellwolf> | when bridging with runtime, you just provide some witness to the otherwise already type checked DT code. |
| 2025-05-03 22:21:47 +0200 | <r-sta> | like Vertex :: MarketMode -> Type |
| 2025-05-03 22:21:33 +0200 | <r-sta> | and there is a Vertex UP |
| 2025-05-03 22:21:24 +0200 | <r-sta> | hmm, like if my trader flips between up flat and down |
| 2025-05-03 22:20:54 +0200 | <hellwolf> | no, that's not how it works. Need some inspirational example I guess. |
| 2025-05-03 22:20:46 +0200 | <r-sta> | nah, singletons im fine with |
| 2025-05-03 22:20:36 +0200 | <r-sta> | sounds like python... |
| 2025-05-03 22:20:32 +0200 | <hellwolf> | if you use Nat/SNat, which I find very useful, that's already a tiny bit of DT. |
| 2025-05-03 22:20:27 +0200 | <r-sta> | like, how does it even make sense, if i could choose to output a different type depending on runtime conditions |
| 2025-05-03 22:19:49 +0200 | <r-sta> | type applications is good, not sure if i like dependant types in haskell, i found idris unusable |
| 2025-05-03 22:19:44 +0200 | <hellwolf> | it reminded me to add to TODO to remove SNat usage in places I could. |
| 2025-05-03 22:19:08 +0200 | <r-sta> | idk, i was ok with @ |
| 2025-05-03 22:18:38 +0200 | <r-sta> | that appear on the lhs of the constraint arrow, are just treated as arguments as if they were specified on the rhs of the constraint arrow |
| 2025-05-03 22:18:33 +0200 | <hellwolf> | it's nice to use. |
| 2025-05-03 22:18:03 +0200 | <r-sta> | mySizeOf a = sizeOf a |
| 2025-05-03 22:18:03 +0200 | <r-sta> | mySizeOf :: forall a -> Sized a => Int |
| 2025-05-03 22:18:01 +0200 | <r-sta> | its weird because even "arguments" (type level sytax at term level!!! :-/) |
| 2025-05-03 22:16:53 +0200 | <r-sta> | https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst |
| 2025-05-03 22:16:45 +0200 | <r-sta> | "Visible forall in types of terms, and types in terms" |
| 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 |