2025/04/28

Newest at the top

2025-04-28 02:34:57 +0200 <monochrom> Someone wrote a prime factorization algorithm in C++ that takes O(1) time. How: The factorization happened at compile time, the generated code just needs to print the answer.
2025-04-28 02:34:01 +0200 <monochrom> You are reminding me of that joke (or true story) about C++ back then.
2025-04-28 02:30:10 +0200 <monochrom> s/pass n and v/pass n and the vector/
2025-04-28 02:27:28 +0200 <monochrom> Or you can do an implicit church encoding like I described. You don't construct a pair for the sigma type, you pass n and v "separately" to a function foo :: (n::Nat) -> Vec n Bool -> IO ().
2025-04-28 02:24:47 +0200 <monochrom> If you have n::Nat coming from user input, for example the user inputs n booleans and you store them in an index-safe vector, i.e., the vector type includes the length n, i.e., Vec n Bool, then generically speaking you now have a sigma type: v :: Σn::Nat. Vec n Bool. You can call that dynamic; it's a sigma, it's OOP now.
2025-04-28 02:24:26 +0200 <haskellbridge> <loonycyborg> unless it'sJIT
2025-04-28 02:24:22 +0200 <haskellbridge> <loonycyborg> because compiler doesn't know anything about actual data that will be read
2025-04-28 02:24:06 +0200 <haskellbridge> <loonycyborg> Probably if your program operates on such types then it wouldn't be too optimized
2025-04-28 02:23:38 +0200 <haskellbridge> <loonycyborg> Practical case would be serialization: can you construct your data entirely based on something you de-serialize with dependent types?
2025-04-28 02:19:34 +0200OftenFaded(~OftenFade@user/tisktisk) OftenFaded
2025-04-28 02:18:37 +0200__jmcantrell__(~weechat@user/jmcantrell) jmcantrell
2025-04-28 02:18:20 +0200 <monochrom> Yeah "type-level 0::Nat as opposed to term-level 0::Nat" is a GHC invention, proving that GHC does not have dependent typing. In dependent typing there is just one 0::Nat; you can use it anywhere you want, in a term or in a type, but it's the same 0::Nat used in both sites, not two different versions.
2025-04-28 02:17:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 02:13:56 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
2025-04-28 02:10:17 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds)
2025-04-28 02:07:26 +0200 <EvanR> (for whatever reason)
2025-04-28 02:07:16 +0200 <EvanR> the program itself can be well typed while still juggling types at runtime
2025-04-28 02:06:55 +0200 <EvanR> that wouldn't happen
2025-04-28 02:06:48 +0200 <EvanR> python's dynamic types cause the program to crash if a type check fails
2025-04-28 02:06:41 +0200 <haskellbridge> <loonycyborg> * typed
2025-04-28 02:06:25 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-28 02:06:15 +0200 <haskellbridge> <loonycyborg> So I'm thinking that going fully dependent typing would either result in some weird inconsistencies or push the language into becoming fully dynamic like python
2025-04-28 02:05:30 +0200 <EvanR> you can read chars or Word8 from stdin I would believe that
2025-04-28 02:04:58 +0200jespada_(~jespada@r186-49-245-168.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds)
2025-04-28 02:04:17 +0200 <haskellbridge> <loonycyborg> Yes, but if it's made fully dependent typed then potentially could read any sort of types from stdin, even those that aren't haskell specific hacks
2025-04-28 02:01:47 +0200 <EvanR> outside haskell
2025-04-28 02:01:35 +0200 <EvanR> you don't want to do this
2025-04-28 02:01:21 +0200 <EvanR> the conflation between arithmetic on literal types is a haskell thing because it's weird type level hacks
2025-04-28 01:59:21 +0200 <haskellbridge> <loonycyborg> EvanR: ye I actually meant dependent type arithmetic :P
2025-04-28 01:59:07 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-04-28 01:56:53 +0200 <mange> I've also seen https://dl.acm.org/doi/10.1145/3341692, which is kind of about deferring type checking until runtime. It's not exactly what you're looking for, but it feels in the same ballpark.
2025-04-28 01:55:26 +0200 <EvanR> -- oh, compile time arithmetic at runtime, that would be JIT
2025-04-28 01:54:13 +0200 <EvanR> not a DataKind
2025-04-28 01:54:02 +0200 <EvanR> the Nat used at type level can be the same Nat used at value level
2025-04-28 01:53:17 +0200 <EvanR> and compile time arithmetic at runtime sounds like a contradiction
2025-04-28 01:52:54 +0200 <EvanR> if this is mainstreet dependent types you wouldn't have a separate type level Nat
2025-04-28 01:51:33 +0200 <haskellbridge> <loonycyborg> And if we can then how it works :P
2025-04-28 01:51:13 +0200 <haskellbridge> <loonycyborg> What I'm really wondering about are things like: if we read something from stdin and make a type level Nat from it then can we make arbitrary compile time arithmetic on it?
2025-04-28 01:50:39 +0200fantom(~fantom@2.219.56.221)
2025-04-28 01:47:37 +0200 <EvanR> or why you would want to
2025-04-28 01:47:33 +0200 <EvanR> I don't see how you would even erase a type that is generated at runtime
2025-04-28 01:47:01 +0200xff0x(~xff0x@2409:251:9040:2c00:8240:4eb8:4326:3de4) (Ping timeout: 248 seconds)
2025-04-28 01:46:41 +0200 <haskellbridge> <loonycyborg> like need to explicitly figure out what is supported and what isn't
2025-04-28 01:46:28 +0200 <mange> Idris 2 lets you be precise about which types you expect to be erased from the program, using multiplicities: https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html#erasure
2025-04-28 01:46:26 +0200 <haskellbridge> <loonycyborg> if you explicitly don't support it then it's unlikely that it's a localized case
2025-04-28 01:46:18 +0200 <EvanR> you can remove them like a compiler is expected to remove terms that aren't doing anything
2025-04-28 01:46:03 +0200 <haskellbridge> <loonycyborg> But still there is the case of reading of arbitrary type from stdin :P
2025-04-28 01:44:54 +0200 <EvanR> once you get to a phase where the types aren't doing anything, then keeping them around can only waste resources
2025-04-28 01:43:48 +0200 <haskellbridge> <loonycyborg> so to get proper dependent types in a compiled language would have to drop type erasure, perhaps replacing it by something else
2025-04-28 01:43:19 +0200 <EvanR> because e.g. constant folding at compile time etc