Newest at the top
| 2025-05-03 22:35:40 +0200 | <monochrom> | haha |
| 2025-05-03 22:35:31 +0200 | <EvanR> | n is unknown until runtime, but is erased |
| 2025-05-03 22:35:23 +0200 | <EvanR> | works in C xD |
| 2025-05-03 22:35:01 +0200 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) |
| 2025-05-03 22:34:47 +0200 | <monochrom> | Really, "g :: IO (Sigma n:Nat . Vec n Foo)" is no different. If n is unknown until runtime and performing I/O, of course it can't be erased. |
| 2025-05-03 22:34:44 +0200 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) (Quit: β reduced) |
| 2025-05-03 22:31:50 +0200 | <monochrom> | Then they speak like "f :: X -> Sigma b:bool. F b, where F False = Foo, F True = Bar, makes no sense because type erase, this is Python again". But it's isomorphic to the Either version. |
| 2025-05-03 22:31:03 +0200 | <EvanR> | like a weak form of C where all these typed functions are exactly the same except for the type, because they don't have polymorphism |
| 2025-05-03 22:30:47 +0200 | <monochrom> | People don't speak like "f :: X -> Either Foo Bar makes no sense because type erasure, this is Python again". |
| 2025-05-03 22:30:30 +0200 | <EvanR> | with a lot of overlap |
| 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 |