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

91–100 of 197 posts

Re: Types as Interfaces

#91

Post by randomdata »

nu11ptr wrote: post #86
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.

How would you ensure that the values of the types doesn't invalidate the contract? Easy for basic assignment, but not sure how you would do that when doing arbitrary mutation.

You could prevent arbitrary mutation, pushing computation onto a more flexible type and allowing assignment back to the more constrained type only when first guarded by an appropriate conditional. The whole "parse, don't validate" thing.

Re: Types as Interfaces

#92

Post by c-hendricks »

mamcx wrote: post #75
posix_monad wrote: post #3

MLs require a lot of ceremony modelling simple record types. What we want to express here is an object with a map of properties (name to type): string Type map For the OOP minded: Map And also compose those: type Foo = { "_foo", int } type Bar = { "_bar", string } type FooBar = mergeMaps Foo Bar But at compile-time, of course. Have any languages achieved this? I know TypeScript can do some of these things, but it's c…

I raise the bar and say the relational model has it and can be made to work at type level. type Person = User DESELECT password type Invoice = Customer JOIN Inv

Something like this in TypeScript:

    type Person = Omit
    type Invoice = Customer & { invoice: Inv }
    // or
    type Invoice = Inv & { customer: Customer }

Re: Types as Interfaces

#93

Post by mason55 »

nu11ptr wrote: post #86
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.

How would you ensure that the values of the types doesn't invalidate the contract? Easy for basic assignment, but not sure how you would do that when doing arbitrary mutation.

You could prove to the type checker that you're only allowing input values that, when fed to your operation, results in outputs that remain in bounds. For example, if you're doing addition, you first check that each input is between 1 and 49, and you exhaustively handle the cases where the values are out of those bounds. Then the type checker can see that the output is always between 1 and 100.

For operations/mutations where it's more complex to validate the inputs, you could assign the result to an unbounded variable, and then prove to the type checker that you're exhaustively handling the output before you assign it to a bounded variable. For example, multiply two unbounded numbers, store the result in an unbounded variable, then do "if result >= 1 && result <= 100 then assign result to var[1..100] else .... end"

Re: Types as Interfaces

#94

Post by prmph »

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.

Re: Types as Interfaces

#95

Post by shepherdjerred »

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…

https://www.typescriptlang.org/docs/handbook/type-compatibil...

https://www.typescriptlang.org/play/?strictFunctionTypes=fal...

Re: Types as Interfaces

#96

Post by pydry »

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*?

I was thinking of Haskell and F#. Neither one is completely unused outside of academic contexts but it is rare.

Rust is an example where a stronger type system has an associated payoff and it's being used all over.

Re: Types as Interfaces

#97

Post by dgb23 »

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

It’s useful to examine fundamentals now and then.

Re: Types as Interfaces

#98

Post by wvenable »

duped wrote: post #76
harporoeder wrote: post #59

Earlier quoted context omitted.

With dependent types you still end up having to do dynamic checking of invariants for a substantial portion of real world code to construct the value with the properties you want. Anything coming from disk or network or a database etc. In practice I feel that it is far easier to just do manual dynamic checking with the constructor hidden from other modules such as `constructEmail :: string -> Email' which uses normal…

You should be parsing/validating any value coming from disk or the network

You never know when the file will just suddenly be all zeros.

Re: Types as Interfaces

#99

Post by betenoire »

randomdata wrote: post #88
paulddraper wrote: post #79

Earlier quoted context omitted.

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

Typescript also does the former, albeit with less friendly syntax. X: 1 | 2 | 3 // …

Kinda but not really. It actually handles type inference on string concatenation, but doesn't understand math.

  type N = 1 | 2

  const x1:N = 1
  const x2:N = 1
  
  const sum:N = x1 + x2
Typescript (the version running on my box) considers this an error.

Re: Types as Interfaces

#100

Post by jddj »

cxr wrote: post #69
jddj wrote: post #24

Earlier quoted context omitted.

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.

You might be right you know. I can't edit anymore but please mentally strike out that first paragraph.

I did read a lot into the '??' punctuation which might not have been intended.

Post reply on HN