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

181–190 of 197 posts

Re: Types as Interfaces

#181

Post by taeric »

nucleardog wrote: post #178
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. Let me put on my straightest face. Schemaless tools have no benefits.* As soon…

So you have mainly straw-manned on the word "schemaless" to make an argument. This is akin to attacking dynamic typing by pointing out that most things can be type inferred by the code.

That is, you are not wrong in that most data stored is structured in some way; but you are ignoring a ton of the benefit of the schemaless world. As I pointed out, there are benefits to specifying schema. In parts, you /have/ to do so. Specifically if you want your DB to do any work on the data. Indexing/filtering and the like.

Now, you do hit largely on the benefits of the "schemaless" world. And that is that it is not undefined how it will store whatever schema you throw at it. You will have restrictions on keys, but otherwise it will store whatever you throw at it.

At large, this means you can skip out on a lot of the formality of specifying all schema shapes during development and can take a much more flexible approach in your code than you are forced to if the data layer can't work with you.

Re: Types as Interfaces

#182

Post by yencabulator »

shepherdjerred wrote: post #95
the8thbit wrote: post #82

Earlier quoted context omitted.

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

     // This can go all the way back to the smallest common type:

     listenForEvent("mouse", (event: {}) => { });
Typescript {} is a trap that means "any container of things is fine" (including objects), it's not the empty struct. One of the very ugly oddities of the language.. `Record` or something like that is the closest equivalent to an empty struct.

https://github.com/typescript-eslint/typescript-eslint/issue...

Re: Types as Interfaces

#183

Post by moomin »

kelseyfrog wrote: post #139
moomin wrote: post #125

Earlier quoted context omitted.

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.

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

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.

Re: Types as Interfaces

#184

Post by betenoire »

randomdata wrote: post #103
betenoire wrote: post #99

Earlier quoted context omitted.

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.

There is nothing to suggest that 1..100 understands math.

I think the whole point of a type fully understanding the constraints of your data suggests it would ideally.

Typescript is able to do this with strings when using templates.

  type Suit = "C" | "D" | "H" | "S";
  type Rank = "A" | "2" | "3" | "4";
  type Card = `${Suit}${Rank}`;

  const club = "D";
  const ace = "A";

  const aceOfClubs: Card = `${club}${ace}`;
Even though I have not declared the club or ace as a Suit or Rank, it still infers the Card correctly in the last line. This is a stronger form of typing than what you are settling for where 1..100 doesn't know its own range.

This is the difference I'm referring to.

Re: Types as Interfaces

#185

Post by randomdata »

betenoire wrote: post #184
randomdata wrote: post #103

Earlier quoted context omitted.

There is nothing to suggest that 1..100 understands math.

I think the whole point of a type fully understanding the constraints of your data suggests it would ideally. Typescript is able to do this with strings when using templates. type Suit = "C" | "D" | "H" | "S"; type Rank = "A" | "2" | "3" | "4"; type Card = `${Suit}${Rank}`; const club = "D"; const ace = "A"; const aceOfClubs: Card = `${club}${ace}`; Even though I have not declared the club or ace as a Suit or Rank, i…

The difference you are referring to was already asserted in your first comment. I'm afraid whatever you were trying to add here is being lost. Unless you were, strangely, straight up repeating yourself for no reason?

Re: Types as Interfaces

#186

Post by betenoire »

randomdata wrote: post #185
betenoire wrote: post #184

Earlier quoted context omitted.

I think the whole point of a type fully understanding the constraints of your data suggests it would ideally. Typescript is able to do this with strings when using templates. type Suit = "C" | "D" | "H" | "S"; type Rank = "A" | "2" | "3" | "4"; type Card = `${Suit}${Rank}`; const club = "D"; const ace = "A"; const aceOfClubs: Card = `${club}${ace}`; Even though I have not declared the club or ace as a Suit or Rank, i…

The difference you are referring to was already asserted in your first comment. I'm afraid whatever you were trying to add here is being lost. Unless you were, strangely, straight up repeating yourself for no reason?

let me say in fewer words:

>There is nothing to suggest that 1..100 understands math.

That's like, your opinion man. I'd like it.

Re: Types as Interfaces

#187

Post by auggierose »

agentultra wrote: post #175
auggierose wrote: post #157

Earlier quoted context omitted.

I don't rely on the type system for my specification. I just rely on it to significantly reduce the number of bugs I inadvertently introduce into the implementation of my specification.

How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?

I have trouble parsing your sentence, to be honest. What are you asking?

Are you asking how am I sure that/if my specification is correct?

Are you asking how do I make sure I have no bugs without a proof?

Maybe you are asking something else entirely?

Re: Types as Interfaces

#188

Post by randomdata »

betenoire wrote: post #186
randomdata wrote: post #185

Earlier quoted context omitted.

The difference you are referring to was already asserted in your first comment. I'm afraid whatever you were trying to add here is being lost. Unless you were, strangely, straight up repeating yourself for no reason?

let me say in fewer words: >There is nothing to suggest that 1..100 understands math. That's like, your opinion man. I'd like it.

You'd like what? For the type checker to understand math? We know that already. You said that in your first comment. And the second one. And the third one. And now seemingly the fourth one. But let it be known, whatever new information you are trying to add here is getting lost in translation.

Re: Types as Interfaces

#189

Post by agentultra »

auggierose wrote: post #187
agentultra wrote: post #175

Earlier quoted context omitted.

How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?

I have trouble parsing your sentence, to be honest. What are you asking? Are you asking how am I sure that/if my specification is correct? Are you asking how do I make sure I have no bugs without a proof? Maybe you are asking something else entirely?

Because the type system is unsound, you could add an error to your implementation and the type system will not catch it. It will happily tell you that everything type checks.

How do you use that to prevent errors?

Re: Types as Interfaces

#190

Post by stouset »

galkk wrote: post #105
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.

Requirements change, things evolve. Having bounds in the type system is too restrictive. Even history of "required", rather simple restriction on the value, is showing that putting that logic into type system is too much of a burden. https://capnproto.org/faq.html#how-do-i-make-a-field-require...

If the requirements change, you can update the definition in the type system once. And then you immediately know the locations where this new bound is violated.
Post reply on HN