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

171–180 of 197 posts

Re: Types as Interfaces

#171

Post by BugsJustFindMe »

CyberDildonics wrote: post #153
BugsJustFindMe wrote: post #145

Earlier quoted context omitted.

> You don't need to know how a database lays out memory You do, however, need to know what logical columns are in a table and the types of those columns to be able to effectively query against the table. And you need to know what the types of the inputs to a query wrapper function are to be able to call it properly. Memory layout has nothing to do with type, because physical memory layout is completely separate from…

And you need to know what the types of the inputs to a query wrapper function are to be able to call it properly. That's the interface. Memory layout has nothing to do with type, So float, int, unint64, int8 and a vector/array don't have specific memory layouts? the semantic logical layout and form represented by the bits This is nonsense and doesn't mean anything.

> So float, int, unint64, int8 and a vector/array don't have specific memory layouts?

The memory layouts don't need to be known to the user. Different hardware architectures can have the concept of floats and ints and code can be written using them the same way while the underlying representations are distinct. I promise that IEEE754 is not the only way to represent floating point values handed down from god to man on a golden scroll.

> > And you need to know what the types of the inputs to a query wrapper function are to be able to call it properly.

> That's the interface.

Funny, I recall you not very long ago saying "interfaces describe behavior, types describe shape and structure". Now you acknowledge that the interface necessarily includes the types of the arguments?

Re: Types as Interfaces

#173

Post by wredue »

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 is no world where the added time here for the developers is with the trade off, and if you look through my history, you will see that I largely reject “dev time trade off” as a notion a company should ever seriously entertain as a significant burden.

Re: Types as Interfaces

#174

Post by nightski »

joshlemer wrote: post #132
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.

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.

Throwing out type safety simply because you have unverified input is a little silly. It's trivial in most statically typed languages to safely turn input into a concrete type (or an error if it is invalid) at the edge and meanwhile maintain type safety throughout the rest of the code.

Re: Types as Interfaces

#175

Post by agentultra »

auggierose wrote: post #157
agentultra wrote: post #64

Earlier quoted context omitted.

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

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?

Re: Types as Interfaces

#176

Post by CyberDildonics »

BugsJustFindMe wrote: post #171
CyberDildonics wrote: post #153

Earlier quoted context omitted.

And you need to know what the types of the inputs to a query wrapper function are to be able to call it properly. That's the interface. Memory layout has nothing to do with type, So float, int, unint64, int8 and a vector/array don't have specific memory layouts? the semantic logical layout and form represented by the bits This is nonsense and doesn't mean anything.

> So float, int, unint64, int8 and a vector/array don't have specific memory layouts? The memory layouts don't need to be known to the user . Different hardware architectures can have the concept of floats and ints and code can be written using them the same way while the underlying representations are distinct. I promise that IEEE754 is not the only way to represent floating point values handed down from god to man…

The memory layouts don't need to be known to the user.

This isn't relevant one way or another.

Different hardware architectures can have the concept of floats and ints

This also isn't relevant. Data types aren't expected to be cross platform unless they are specifically made for that, like file formats.

Funny, I recall you not very long ago saying "interfaces describe behavior, types describe shape and structure"

I never said that.

Also just because two things work together doesn't mean they are the same thing.

Re: Types as Interfaces

#177

Post by xmgplays »

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.

HaltingProgram and MaybeHalting is expressible(or vice versa), if you want to cover all programs in one of two types. If you want specifically HaltingProgram and NotHaltingProgram then you need a third category of MayOrMayNotHaltingProgram.

Re: Types as Interfaces

#178

Post by nucleardog »

taeric wrote: post #77
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 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 as you start _doing_ anything with your data, it has a schema. You may not have declared it to your data store, to a specific piece of code, etc, but your application logic almost definitely makes assumptions about the shape of the data--what fields are and aren't present, the types of values in those fields, and what those values mean.

Every piece of your system must either accept undefined behaviour in the face of data which doesn't fit this implicit schema (there are very few non-trivial problems where you can define a meaningful, valid output for all possible inputs), or essentially treat the schemaless parts as hostile and assert its assumptions before every action.

The only thing you've done by going "schemaless" is distributing your schema across your systems and pushed the schema validation out to each thing interacting with the schemaless components instead of centralizing it.

* Yes, literally storing raw, unstructured data. But as soon as you need to _do_ anything with the data besides regurgitate it you're back to it having some sort of schema.

Re: Types as Interfaces

#179

Post by BugsJustFindMe »

CyberDildonics wrote: post #176
BugsJustFindMe wrote: post #171

Earlier quoted context omitted.

> So float, int, unint64, int8 and a vector/array don't have specific memory layouts? The memory layouts don't need to be known to the user . Different hardware architectures can have the concept of floats and ints and code can be written using them the same way while the underlying representations are distinct. I promise that IEEE754 is not the only way to represent floating point values handed down from god to man…

The memory layouts don't need to be known to the user. This isn't relevant one way or another. Different hardware architectures can have the concept of floats and ints This also isn't relevant. Data types aren't expected to be cross platform unless they are specifically made for that, like file formats. Funny, I recall you not very long ago saying "interfaces describe behavior, types describe shape and structure" I n…

> > The memory layouts don't need to be known to the user.

> This isn't relevant one way or another.

What needs to be known to the user of an interface is the most relevant aspect of describing that interface.

> Data types aren't expected to be cross platform unless they are specifically made for that, like file formats.

It's going to be difficult to reconcile that position with https://en.wikipedia.org/wiki/Abstract_data_type

Data types can optionally specify machine representation but need not. They specify behavior (i.e. possible values and operations) first and foremost. In programming, nearly every use of data type is in the abstract, entirely separate from its hardware representation. The "Int", the "Bool", the "2", the "UTCTime" being specified in TFA don't care about bit arrangements. They're describing valid values and operations, not hardware.

> I never said that.

You're right. Apologies. It was the other poster at the top of the thread. But it still seems apt to the thread and to your specific portrayal.

Re: Types as Interfaces

#180

Post by CyberDildonics »

BugsJustFindMe wrote: post #179
CyberDildonics wrote: post #176

Earlier quoted context omitted.

The memory layouts don't need to be known to the user. This isn't relevant one way or another. Different hardware architectures can have the concept of floats and ints This also isn't relevant. Data types aren't expected to be cross platform unless they are specifically made for that, like file formats. Funny, I recall you not very long ago saying "interfaces describe behavior, types describe shape and structure" I n…

> > The memory layouts don't need to be known to the user. > This isn't relevant one way or another. What needs to be known to the user of an interface is the most relevant aspect of describing that interface. > Data types aren't expected to be cross platform unless they are specifically made for that, like file formats. It's going to be difficult to reconcile that position with https://en.wikipedia.org/wiki/Abstract…

don't care about bit arrangements.

Not every scenario cares about bit arrangements but they are still there.

You seem to just be shifting around and coming up with new, more abstract arguments that drift further from whatever point you originally had.

You said

"Shape and structure are behavior."

One is data, one is execution. These are two different things.

The more they are conflated together, the more problems people have with their programs.

Not separating them and letting them mix is a huge part of bad software architecture and leads to lots of unnecessary complexity.

Post reply on HN