2 ms·
PrimeNumber is definitely possible in pretty much any dependent type language. Indeed, it would be pretty impossible to get any work done in Lean without it. T
by moomin 2y ago
PrimeNumber is definitely possible in pretty much any dependent type language. Indeed, it would be pretty impossible to get any work done in Lean without it.
TotalProgram: possible in some, not in others, I think.
- kelseyfrog 2y ago> PrimeNumber is definitely possible in pretty much any dependent type language. That's awesome! Thank you. I didn't know type systems were capable of expressing that level of sophistication. Would HaltingProgram and NonHaltingProgram be expressible? I hope it's clear what I'm trying to convey, but the technical wording escapes me today.
- mrkeen 2y agosee the 'total' keyword in Idris https://docs.idris-lang.org/en/latest/proofs/patterns.html https://docs.idris-lang.org/en/latest/proofs/patterns.html
- xmgplays 2y agoHaltingProgram and MaybeHalting is expressible(or vice versa), if you want to cover all programs in one of two types. If you want specifically HaltingProgram and NotHaltingProgram then you need a third category of MayOrMayNotHaltingProgram.
- moomin 2y agoThere is a fascinating result about types that they have a one to one correspondence with proofs. Dependent type systems leverage that to the hilt.