News for hackers. Stuff that matters.

A comment on Types as Interfaces. Parent comment

Re:Types as Interfaces by kelseyfrog on Tuesday July 23, 2024 @02:46PM (#41049433)
> 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.

[ Parent | on HN ]
Re:Types as Interfaces by mrkeen on Tuesday July 23, 2024 @05:40PM (#41051241)
see the 'total' keyword in Idris

https://docs.idris-lang.org/en/latest/proofs/patterns.html

[ Parent | on HN ]
Re:Types as Interfaces by xmgplays on Wednesday July 24, 2024 @04:05AM (#41054661)
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.
[ Parent | on HN ]
Re:Types as Interfaces by moomin on Wednesday July 24, 2024 @12:09PM (#41058505)
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.
[ Parent | on HN ]