I'm looking for a computer langauge with "dependent types" but...

The problem with it having a full implementation is that you end up having to write formal type proofs to get even anything simple done. (Agda/Iris). These are fine if you are writing a proof checker but not for general programming.

As a compromise it would be nice to have a language that would allow "unsafe" dependent type casting where you don't have to give a proof. e.g. you might have a type "PrimesBiggerThan3" and a type "OddNumbers" and you could cast from the first to the second without having to give a formal Type Proof. The proof could just say "TrustMeOnThis".

Does such a language exist, or is there one like this that is useful?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.