Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Types as Interfaces

two-wrongs.com

Post reply on HN
Print view View original

61–70 of 197 posts

Re: Types as Interfaces

#61

Post by unstruktured »

pydry wrote: post #37
user3939382 wrote: post #33

I’ve come to believe that a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value. The only real implementations of this I see are mostly academic with a dependent type system like Idris. We’re many years from that becoming mainstream, if it ever will be.

I think there's a sharp rule of diminishing returns the stronger you make type systems. Type safety comes at a cost and that cost has to come with an associated payoff. This is why ultra strong type systems end up being little more than academic toys - the payoff when you dial type safety up to an extreme doesn't match the associated cost. Types and tests should meet somewhere in the middle because the same law of di…

What, to you, is an ultra strong type system? Both OCaml and Haskell are used in plenty of non academic contexts. Do you mean something like Coq or F*?

Re: Types as Interfaces

#62

Post by nyssos »

nottorp wrote: post #58
pmarreck wrote: post #38

Earlier quoted context omitted.

Idris is fascinating. I actually took the book about it on vacation with me. Software reliability is becoming increasingly important as we tie all these systems together because it multiplies the number of possible unanticipated failure modes. Regarding the ultimate utility of languages initially considered "academic," the languages Lisp, Haskell, Prolog, Scala, Erlang and OCaml would like to have a word ;)

But most of those don't have a real type system though? And definitely not a strict one.

Scala, OCaml, and Haskell all have very powerful type systems. OCaml and Haskell even have good ones.

Re: Types as Interfaces

#63

Post by zarzavat »

valenterry wrote: post #41
auggierose wrote: post #28

Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this. Typescript can't really be this language because it i…

Haskell’s type system isn’t sound either, there is unsafePerformIO.

Nobody actually wants a language with a sound type system, unless they’re writing mathematical proofs. Any time you need to do anything with the external environment, such as call a function written in another language, you need an escape hatch. That’s why every language that aspires to real world use has an unsound type system, and the more practical it aspires to be, the more unsound the type system is.

Soundness is only a goal if the consequences of a type error are bad enough: your proof will be wrong, or an airplane falls out of the sky, or every computer in the world boots to a blue screen.

For everybody else the goal should be to balance error rate with developer productivity. Sacrificing double digits of productivity for single digits of error rate is usually not worth it, since the extra errors that a very sound type system will catch will be dominated by the base rate of logic errors that it can’t catch.

Re: Types as Interfaces

#64

Post by agentultra »

auggierose wrote: post #46
valenterry wrote: post #41

Earlier quoted context omitted.

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this. Typescript can't really be this language because it i…

TypeScript's type foundations are not sound, and I would argue that this is a major factor why it is so good. I have yet to see a sound type system that is as pleasant to use as TypeScript's—certainly not Idris. I am not a fan of encoding all sorts of correctness statements into a static type system. I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory.

What do you gain from an unsound type system? Implicit casts still exist and one dependency returning Any means that your specification is meaningless (you can prove anything, including false).

Re: Types as Interfaces

#65

Post by valenterry »

zarzavat wrote: post #63
valenterry wrote: post #41

Earlier quoted context omitted.

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this. Typescript can't really be this language because it i…

Haskell’s type system isn’t sound either, there is unsafePerformIO. Nobody actually wants a language with a sound type system, unless they’re writing mathematical proofs. Any time you need to do anything with the external environment, such as call a function written in another language, you need an escape hatch. That’s why every language that aspires to real world use has an unsound type system, and the more practica…

I think there is a misunderstanding on your side. You seem to mix up the soundness of the type-system with the property of referential transparency. Those are two orthogonal things.

Re: Types as Interfaces

#66

Post by valenterry »

auggierose wrote: post #46
valenterry wrote: post #41

Earlier quoted context omitted.

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this. Typescript can't really be this language because it i…

TypeScript's type foundations are not sound, and I would argue that this is a major factor why it is so good. I have yet to see a sound type system that is as pleasant to use as TypeScript's—certainly not Idris. I am not a fan of encoding all sorts of correctness statements into a static type system. I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory.

Yes, I think that's what I said. The pragmatic approach makes to very ergonomic to use in most use cases. That it breaks on for edge-cases is not very relevant in practice usually.

> I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory.

Based on what then?

Re: Types as Interfaces

#67

Post by valenterry »

agentultra wrote: post #64
auggierose wrote: post #46

Earlier quoted context omitted.

TypeScript's type foundations are not sound, and I would argue that this is a major factor why it is so good. I have yet to see a sound type system that is as pleasant to use as TypeScript's—certainly not Idris. I am not a fan of encoding all sorts of correctness statements into a static type system. I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory.

What do you gain from an unsound type system? Implicit casts still exist and one dependency returning Any means that your specification is meaningless (you can prove anything, including false).

The point is that making a typesystem sound is really hard and requires trade-offs. I think Scala is a wonderful example. Check: https://www.baeldung.com/scala/dotty-scala-3

To quote from there: > Scala 3 has dropped some unsound and useless features to make the language smaller and more regular. It has added some new constructs to increase its expressiveness. Also, it has changed some constructs to remove warts and increase simplicity, consistency, and usability.

Some of the features they dropped because they were unsound were still useful (to me).

Typescript tries neither to make their typesystem (perfectly) sound, nor to make it as elegant as possible. That results in it to be very useful/pragmatic for everyday-programming tasks.

Re: Types as Interfaces

#68

Post by valenterry »

zarzavat wrote: post #63
valenterry wrote: post #41

Earlier quoted context omitted.

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this. Typescript can't really be this language because it i…

Haskell’s type system isn’t sound either, there is unsafePerformIO. Nobody actually wants a language with a sound type system, unless they’re writing mathematical proofs. Any time you need to do anything with the external environment, such as call a function written in another language, you need an escape hatch. That’s why every language that aspires to real world use has an unsound type system, and the more practica…

Oh and to your argument:

> For everybody else the goal should be to balance error rate with developer productivity. Sacrificing double digits of productivity for single digits of error rate is usually not worth it, since the extra errors that a very sound type system will catch will be dominated by the base rate of logic errors that it can’t catch.

I think you are missing my point.

You are merely looking at a single point in time. And yes, you are right - the balance you mention matters. But what also matters is the future. A language needs to be able to evolve. If it does not do that, it will eventually die and become replaced. If the typesystem is well made with good foundations, the language will be able to evolve and adapt faster and causing less problems for its users.

Re: Types as Interfaces

#69

Post by cxr »

jddj wrote: post #24
brabel wrote: post #2

Is this something professional programmers are having trouble with?? This is the kind of problem you face in your first year working, no? I am honetly curious what others think. Do you have trouble deciding when to use an interface (assuming your language has that), or a type wrapper (I don't think that's the brightest idea), or a function to extract the field to sort by (most languages do that)??

Your confidence that there is an obviously optimal way to model something reads as either brilliance or hubris and brilliance is a lot rarer. Typically there are subtle trade-offs and compromises which only prove themselves to be useful/detrimental as the software changes over time. You can place bets based on experience but you can only really be cocky about your choices when looking back not looking forward

> Your confidence that there is an obviously optimal way to model something

You're imagining things (uncharitably); that's not in the comment you replied to.

Re: Types as Interfaces

#70

Post by BiteCode_dev »

unstruktured wrote: post #61
pydry wrote: post #37

Earlier quoted context omitted.

I think there's a sharp rule of diminishing returns the stronger you make type systems. Type safety comes at a cost and that cost has to come with an associated payoff. This is why ultra strong type systems end up being little more than academic toys - the payoff when you dial type safety up to an extreme doesn't match the associated cost. Types and tests should meet somewhere in the middle because the same law of di…

What, to you, is an ultra strong type system? Both OCaml and Haskell are used in plenty of non academic contexts. Do you mean something like Coq or F*?

"plenty" is relative.

You don't see many GAFAM products created in either, and that's because of the trade off OP talks about.

Post reply on HN