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

151–160 of 197 posts

Re: Types as Interfaces

#151

Post by carapace »

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.

> a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value

That's a programming language. In other words, now your type system needs a type system.

Re: Types as Interfaces

#152

Post by platz »

fellowniusmonk wrote: post #134
platz wrote: post #133

Earlier quoted context omitted.

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…

oh I made a a typo. Meant "types" OR "bytes"

Re: Types as Interfaces

#153

Post by CyberDildonics »

BugsJustFindMe wrote: post #145
CyberDildonics wrote: post #144

Earlier quoted context omitted.

Shape and structure are behavior. They shouldn't be. Conflating two things that can be separated is just compounding complexity. You don't need to know how a database lays out memory or the structure behind a web server.

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

Re: Types as Interfaces

#154

Post by LudwigNagasena »

tinix wrote: post #23

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

Interfaces are usually understood as a subset of types. Interfaces specifically describe method signatures. Nevertheless, the distinction is murky because any structure can be interpreted in terms of getters and setters which can be considered methods.

Re: Types as Interfaces

#155

Post by valcron1000 »

fungiblecog wrote: post #150

Rich Hickey would say "just use maps" and avoid all this navel-gazing

It does not solve the problem. Would you rather have a function that takes a map and puts additional keys in it (ex. `timestamp`) or a function that takes a map and stores it in a new map alongside the additional keys? In any case, how would you write a generic function that works on those additional keys?

Re: Types as Interfaces

#156

Post by zdragnar »

taeric wrote: post #146
zdragnar wrote: post #140

Earlier quoted context omitted.

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 th…

I think I get your point. I would add reconciliation to validation. In that sometimes you cannot validate something without doing it, and are instead storing a possibly out of band reconciliation of result. I'm curious, though, in how this argument does not apply to many other properties people try and encode into the types? It is one thing if you are only building envelopes and payloads. And, I agree that that gets…

There are things that can embed a bit of temporal logic into types, such as a linear type that can statically guarantee a file handler has been closed exactly once, or error.

For the most part, what I think people really want are branded types. F# has a nice example of unit, where a float can be branded Fahrenheit or Celsius or Kelvin, and functions can take one of those types as parameters.

You then have some function that can parse user input into a float and brand it one of those types. The compiler doesn't make any guarantees about the user input, only that the resulting branded value cannot be used where a different one is expected. Other good examples are degrees and radians, or imperial and metric, etc.

Depending on what you are doing, knowing at a type level that some number can never be negative (weight in pounds) can save you a lot of hassle. If one part of the system doesn't brand a value, and it feeds into another part of the system that is branded, you're stuck with extraneous runtime checks all over the place or a lot of manual unit tests. Instead, the compiler can point out exactly, and in every instance, where you assumed you had a validated value but instead did not.

Re: Types as Interfaces

#157

Post by auggierose »

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

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.

Re: Types as Interfaces

#158

Post by taeric »

zdragnar wrote: post #156
taeric wrote: post #146

Earlier quoted context omitted.

I think I get your point. I would add reconciliation to validation. In that sometimes you cannot validate something without doing it, and are instead storing a possibly out of band reconciliation of result. I'm curious, though, in how this argument does not apply to many other properties people try and encode into the types? It is one thing if you are only building envelopes and payloads. And, I agree that that gets…

There are things that can embed a bit of temporal logic into types, such as a linear type that can statically guarantee a file handler has been closed exactly once, or error. For the most part, what I think people really want are branded types. F# has a nice example of unit, where a float can be branded Fahrenheit or Celsius or Kelvin, and functions can take one of those types as parameters. You then have some functi…

Some of these are why I would add reconciliation to the idea. Linear types, specifically. You can encode that you only send a message once. But, without doing reconciliation with the destination, you can not be sure that it was received.

I'm torn, as the examples from small programs make a ton of sense and I largely like them. I just cannot escape that every attempt I've seen at doing these in large programs is often fairly painful. I cannot claim they are more error prone than the ones that skip out on it. I can say they are far more scarce. Such that the main error condition appears to be to stall out on delivery.

Re: Types as Interfaces

#159

Post by VTimofeenko »

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 am cheating a bit by naming a non-general purpose language, but Nickel[1] does that, for example through composing contracts.

[1]: https://nickel-lang.org/

Re: Types as Interfaces

#160

Post by mrkeen »

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.

see the 'total' keyword in Idris

https://docs.idris-lang.org/en/latest/proofs/patterns.html

Post reply on HN