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

111–120 of 197 posts

Re: Types as Interfaces

#111

Post by nyssos »

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).

> What do you gain from an unsound type system?

The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.

Re: Types as Interfaces

#112

Post by rictic »

prmph wrote: post #94
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.

To check these types would then require possibly infinite time, and the checking may never halt, per the halting problem. Useful types are a compromise between expressiveness and practicality.

It's true that there are valid programs which don't type check in the same way that for any mathematical system there are truths which can't be proven.

In practice though, almost any program you'd want to write can be type checked, in the same way that few proofs get tied into Gödelian knots.

Re: Types as Interfaces

#113

Post by [deleted] »

paulddraper wrote: post #79
vbezhenar wrote: post #74

Earlier quoted context omitted.

I'm surprised that most popular languages don't even do simple type constraints. Like x: 1..100 y: "yes" | "no" I feel that there are lots of low hanging fruits when it comes to typing which would improve both program readability and correctness.

TypeScript does the latter. The former is difficult to track through arithmetic operations.

[deleted]

Re: Types as Interfaces

#114

Post by keybored »

spankalee wrote: post #110

This is a lot of complication for in what most OOP languages with interfaces would simply be something like: interface Timestamped { timestamp: UTCTime; } interface Msg { sender: PlayerId; } class Quote implements Timestamped, Msg { timestamp: UTCTime; sender: PlayerId; } Why is this so hard in Haskell? It doesn't have interface polymorphism?

I think TFA is talking about nesting fields in whatever order and also being able to extract the fields without ceremony like `get(get(get...))`—just allow `get(...)`. If you wanted an example more close to the submission you would have a multi-field class inside that class. Then you would perhaps solve the nested field access boilerplate by manually implementing it in the interface methods.

Re: Types as Interfaces

#115

Post by rictic »

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'm optimistic that improved proof search using modern AI can make working with dependent type systems much more productive and practical.

A future programmer may be spending more time formally describing the invariants of the system.

Re: Types as Interfaces

#117

Post by nyssos »

the8thbit wrote: post #82
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…

What does "soundness" mean here? I love typescript's type system, except for the quirks that are inherited from javascript, which I sometimes find infuriating, and I'm wondering if you're talking about the same thing. For example, the fact that typescript- through javascript- only exposes a single `number` type is so annoying. Sometimes that's fine, but other times it would be nice to be able to say "No, this isn't j…

Informally, a sound type system is one that never lies to you.

Formally, the usual notion of soundness is defined with respect to an evaluation strategy: a term-rewriting rule, and a distinguished set of values. For pure functional programs this is literally just program execution, whereas effects require a more sophisticated notion of equivalence. Either way, we'll refer to it as evaluating the program.

There are two parts:

- Preservation: if a term `a` has type `T` and evaluates to `b`, then `b` has type `T`.

- Progress: A well-typed term can be further evaluated if and only if it is not a value.

Re: Types as Interfaces

#118

Post by spankalee »

keybored wrote: post #114
spankalee wrote: post #110

This is a lot of complication for in what most OOP languages with interfaces would simply be something like: interface Timestamped { timestamp: UTCTime; } interface Msg { sender: PlayerId; } class Quote implements Timestamped, Msg { timestamp: UTCTime; sender: PlayerId; } Why is this so hard in Haskell? It doesn't have interface polymorphism?

I think TFA is talking about nesting fields in whatever order and also being able to extract the fields without ceremony like `get(get(get...))`—just allow `get(...)`. If you wanted an example more close to the submission you would have a multi-field class inside that class. Then you would perhaps solve the nested field access boilerplate by manually implementing it in the interface methods.

I guess I'm missing why you would model these interfaces as nested, when obviously nesting has the ordering issue.

Re: Types as Interfaces

#119

Post by wwweston »

thesuperbigfrog wrote: post #109
taeric wrote: post #77

Earlier quoted context omitted.

I regret to say that every type level Gordian knot that I have ever been exposed to came from attempts to do this. I think a lot of the problem is that many of the constraints and acceptable values for data are not determined until well after first deployment. The "knot" comes in when you are explicitly changing data and code to add a feature that you didn't anticipate at the start. This is a lot like schemaless data…

>> This is a lot like schemaless databases. The flexibility of not having to fully specify the full schema does not mean that you don't benefit from specifying parts of it? Indeed, if you are indexing things, you have to specify those parts. But it is hard to argue with a straight face that schemaless tools don't have some strong benefits. This is very similar to what Rich Hickey argued in "Simplicity Matters": https…

Sometimes I’ve wondered if versioned types might be a help in bringing coexistence to a typed setup, and if this is part of where the benefits of a service oriented architecture come from. But given how versioning snarls can play out in dependency management I expect this idea has some tradeoffs in the best case.

Re: Types as Interfaces

#120

Post by nyssos »

spankalee wrote: post #118
keybored wrote: post #114

Earlier quoted context omitted.

I think TFA is talking about nesting fields in whatever order and also being able to extract the fields without ceremony like `get(get(get...))`—just allow `get(...)`. If you wanted an example more close to the submission you would have a multi-field class inside that class. Then you would perhaps solve the nested field access boilerplate by manually implementing it in the interface methods.

I guess I'm missing why you would model these interfaces as nested, when obviously nesting has the ordering issue.

Because you don't want to have to enumerate every possible combination up front. Mixins are probably the closest OO concept.
Post reply on HN