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

131–140 of 197 posts

Re: Types as Interfaces

#131

Post by taeric »

mason55 wrote: post #90
ryangs wrote: post #80

Earlier quoted context omitted.

The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.

Yeah - in theory they are the same thing. You can have a dependent type that's an array with a length of 5 or you can create a type called ArrayLengthFive, and in both cases the type checker ensures that you don't accidentally use an unbounded array. But the difference is that with a dependent type, you get more guarantees (e.g. my ArrayLengthFive type could actually allow for arrays of length 20!). And the type chec…

Parsing a string into an email, of course, is already fraught with peril. Is it valid HTML? Or did you mean the email address? Is it a well formed email, or a validated address that you have received correspondence with? How long ago was it validated? Fun spin on the, "It's an older code, sir, but it checks out."

I've seen attempts at solving each of those issues using types. I am not even positive they aren't solvable.

Re: Types as Interfaces

#132

Post by joshlemer »

ryangs wrote: post #80
turboponyy wrote: post #54

Earlier quoted context omitted.

I empathize with this point of view - if not in any other way then in principle. However, as a counterpoint, I'd suggest that encoding all known invariants as types may be prohibitively cumbersome and time-consuming - to the point where writing the program becomes more of an exercise in proofs rather than producing something useful. Often the invariants of a program are implied or can be easily inferred by the reader…

The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.

But then ironically, the problem with relying on programming language type systems is that they don't scale (beyond the boundaries of a single process). As soon as you are crossing a wire you have to go back to runtime validations.

Re: Types as Interfaces

#134

Post by fellowniusmonk »

platz wrote: post #133
fellowniusmonk wrote: post #123

Primitive types and schemas. Complex types and objects don't exist. Embrace Mereological Nihilism. It's fun at meetups to tell everyone your programming paradigm is Nihilism.

What is fundamental, types of bytes?

Yeah, very roughly speaking.

In the philosophic position of mereological nihilism only "simples" exist when discussing objects, etc, simples are akin to byte types for sure and primitive types maybe.

Nothing complex, like objects, higher level types, etc. exist.

Composition of simples in time and space is what determines everything other than simples. Anything that isn't a simple is just emergent from the space/time arrangement of the simples.

So if the implications are that nothing is real outside of time/space/simples, then calling something higher level a "type" is to label something as discrete and real when it isn't, so now you are using language and models that are wrong to reason about things, which means your model will have frustrating drift from reality that you can't rectify.

That's where schemas come in, we are just labeling common arrangements of simples for semantic reasons but they don't really exist so they shouldn't be elevated to the position of a type as that is a wrong abstraction and causes divergence and mess.

Re: Types as Interfaces

#135

Post by skybrian »

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…

Protobufs are an interesting hybrid. They assume a common, linear history of schema versions, where all data generators had access to an arbitrary version in that history. The schemas define field ids and types, but not which combinations of fields can show up.

If you can upgrade all the data then you don’t need to worry about versioning,

Or you can do it like HTTP headers and hope for the best.

Re: Types as Interfaces

#136

Post by skybrian »

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

This is true when you can’t upgrade all the data and all the data generators. But there are smaller systems where you can actually upgrade everything you have and set some new requirements for everything coming in.

Re: Types as Interfaces

#137

Post by tinix »

klysm wrote: post #108
tinix wrote: post #23

types are not interfaces. interfaces describe behavior, types describe shape and structure. the difference is subtle but important.

Depends on the language. In typescript and interface can absolutely encode shape. In C# you can encode shape in interfaces via properties. Interfaces don’t even describe behavior, it’s just that we typically associate them with a man implicit contract. Strictly speaking they are just a shape.

fair, maybe i should have said "protocols define behavior" instead of interface

Re: Types as Interfaces

#138

Post by TuringTest »

ryangs wrote: post #80
turboponyy wrote: post #54

Earlier quoted context omitted.

I empathize with this point of view - if not in any other way then in principle. However, as a counterpoint, I'd suggest that encoding all known invariants as types may be prohibitively cumbersome and time-consuming - to the point where writing the program becomes more of an exercise in proofs rather than producing something useful. Often the invariants of a program are implied or can be easily inferred by the reader…

The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.

There's where good documentation and training pays off.

Some invariants that are too complex to express purely in code, requiring numerous separate low level bookkeeping functions throughout the system, can be concisely expressed as a high level idea in natural language (wether as comments or at an external technical document).

Make sure that your developers are exposed to those documents, throw in a few tests for the most obvious cases to ensure that newcomers are learning the invariants by heart, and if they're competent you should not have problems but in the most obscure cases (that could appear anyway even if you try to formalize everything in code).

Re: Types as Interfaces

#139

Post by kelseyfrog »

moomin wrote: post #125
kelseyfrog wrote: post #104

Earlier quoted context omitted.

I wish it were possible, but I have a sneaking suspicion that types like PrimeNuber or TotalProgram, are beyond the realm of possibility.

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.

Re: Types as Interfaces

#140

Post by zdragnar »

taeric wrote: post #131
mason55 wrote: post #90

Earlier quoted context omitted.

Yeah - in theory they are the same thing. You can have a dependent type that's an array with a length of 5 or you can create a type called ArrayLengthFive, and in both cases the type checker ensures that you don't accidentally use an unbounded array. But the difference is that with a dependent type, you get more guarantees (e.g. my ArrayLengthFive type could actually allow for arrays of length 20!). And the type chec…

Parsing a string into an email, of course, is already fraught with peril. Is it valid HTML? Or did you mean the email address? Is it a well formed email, or a validated address that you have received correspondence with? How long ago was it validated? Fun spin on the, "It's an older code, sir, but it checks out." I've seen attempts at solving each of those issues using types. I am not even positive they aren't solvab…

Validation is an event, with it's own discrete type separate from the address itself. This is no different than a physical address.

    123 Somewhere Lane
    Somewhereville, NY 12345
is a correctly formatted address but is almost certainly not one that physically exists.

Validation that it exists isn't solvable in the type system because, as I mentioned, it is an event. It is only true for the moment it was verified, and that may change at any point in the future, including immediately after verification.

Post reply on HN