Types as Interfaces

Re:Types as Interfaces by moomin on Tuesday July 23, 2024 @01:40PM (#41048734)

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.

[ Parent | on HN ]

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 ]