4 ms·

I wish it were possible, but I have a sneaking suspicion that types like PrimeNuber or TotalProgram, are beyond the realm of possibility.

• 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 ago
      see 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 ago
      HaltingProgram 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 ago
      There is a fascinating result about types that they have a one to one correspondence with proofs. Dependent type systems leverage that to the hilt.