Newest at the top
| 2025-05-03 22:41:20 +0200 | <geekosaur> | that isn't the whine I most often see, tbh |
| 2025-05-03 22:41:15 +0200 | <EvanR> | loonycyborg: such as (++x) + (x++) |
| 2025-05-03 22:41:11 +0200 | <monochrom> | hahaha that's great |
| 2025-05-03 22:41:00 +0200 | <monochrom> | No, geekosaur, this is me whining about people whining about dependent typing. |
| 2025-05-03 22:40:51 +0200 | <int-e> | monochrom: The Church is always happy to step in in moments of an existential crisis. |
| 2025-05-03 22:40:47 +0200 | <haskellbridge> | <loonycyborg> C can be like haskell if you write program in one single expression :P |
| 2025-05-03 22:40:26 +0200 | <monochrom> | Yeah also "negate :: Num a => a -> a, is the type erased or not? Are you cheating?" |
| 2025-05-03 22:39:43 +0200 | <monochrom> | Oh yeah if someone scaremongers about existential types, my next move is to cite the double ->r version. |
| 2025-05-03 22:39:11 +0200 | <int-e> | (n is erased, but the KnownNat dictionary isn't, problem solved) |
| 2025-05-03 22:39:05 +0200 | <geekosaur> | is this a follow-up to conal's "C is a FP language"? |
| 2025-05-03 22:38:48 +0200 | <int-e> | . o O ( IO (forall r. (forall n. KnownNat n => Vec n Foo -> r) -> r) ) |
| 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 @ |