3 ms·
> 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 expressi
by 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.