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

161–170 of 197 posts

Re: Types as Interfaces

#161

Post by mrkeen »

spankalee wrote: post #110

This is a lot of complication for in what most OOP languages with interfaces would simply be something like: interface Timestamped { timestamp: UTCTime; } interface Msg { sender: PlayerId; } class Quote implements Timestamped, Msg { timestamp: UTCTime; sender: PlayerId; } Why is this so hard in Haskell? It doesn't have interface polymorphism?

> Why is this so hard in Haskell?

The challenge is composition. Adding Timestamped to something in a static, type-checked way, but not modifying the source code of that something.

> It doesn't have interface polymorphism?

This is besides the point, but its interface polymorphism is static, not dynamic. If you have a List which is IMappable, and you do some IMappable operations on it, in most OOP languages you get back an IMappable, but in Haskell you get back List.

Re: Types as Interfaces

#162

Post by prmph »

rictic wrote: post #112
prmph wrote: post #94

Earlier quoted context omitted.

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.

It's true that there are valid programs which don't type check in the same way that for any mathematical system there are truths which can't be proven. In practice though, almost any program you'd want to write can be type checked, in the same way that few proofs get tied into Gödelian knots.

True, but there is a difference between "can be type checked" and "can be type checked in a reasonable amount of time".

I get reminded of this everything I have to work with a certain large Typescript code-base of mine that makes heavy use of union and template literal types. The Typescript Language Server has a hard time with these types. Frequently, everything slows to a crawl in VSCode, and it take 10 minutes of more for intellisense to update after every type change, ouch.

Although in this case, I suspect it is Typescript's implementation of union types that is to blame (since other languages seem to handle complex union types with ease), this experience still shows that type checking can become quite expensive.

Re: Types as Interfaces

#163

Post by jdougan »

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…

The C ”type system", circa 1985.

Re: Types as Interfaces

#164

Post by yencabulator »

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.

Typed constraints don't scale either.

I eagerly await your implementation of a type describing my tax return. And to implement a compiler for the new programming language you'll inevitably have to construct, we're gonna need two types, one expressing all valid source programs, and the other all valid programs for the target platform.

Oh, can we also get updates to that for next year's taxes, new platforms, and other such future business needs? Of course the current requirements have to still remain supported.

Re: Types as Interfaces

#165

Post by yencabulator »

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

The other alternative is what protobuf did to solve the same pain: In proto3, all optionals have a default value. They're effectively required where the default value doesn't need to be encoded in the message.

The exact different between the two approaches is subtle. Technically you can fancier things with the framework exposing the optional values as set/not set, but in practice a lot of code is a lot simpler with default values.

https://protobuf.dev/programming-guides/proto3/#default

Re: Types as Interfaces

#166

Post by satvikpendem »

wwweston wrote: post #119
thesuperbigfrog wrote: post #109

Earlier quoted context omitted.

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

Sometimes I’ve wondered if versioned types might be a help in bringing coexistence to a typed setup, and if this is part of where the benefits of a service oriented architecture come from. But given how versioning snarls can play out in dependency management I expect this idea has some tradeoffs in the best case.

You might be interested in the Unison language then.

Re: Types as Interfaces

#167

Post by smackmybishop »

taeric wrote: post #149
skybrian wrote: post #135

Earlier quoted context omitted.

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.

Protobufs are also a fun place to look for how much debate people will get into regarding required versus optional fields. Your post is taking an implicit "everything is optional" view. But, it does allow you to be stricter. Common Lisp Object System also touched on all of these ideas years ago.

Everything has been `optional` for about a decade.

> The option to set a field to required is absent in proto3 and strongly discouraged in proto2.

https://protobuf.dev/overview/#syntax

Re: Types as Interfaces

#168

Post by yencabulator »

jerf wrote: post #89
AnimalMuppet wrote: post #83

Earlier quoted context omitted.

Slightly more optimistically: As we go along, small pieces go from "too expensive to actually use" to "usable on real projects, but nobody does yet", and then to "doesn't everybody do that?" This is the story of improvements in type systems over the last 70 years. But the progress is very slow. So this is only slightly more optimistic...

This is where I'd really be interested in seeing an AI system help. Don't write an AI system that helps me shovel out vast quantities of code, and then solves the problem of the resulting incomprehensible mass of code being impossible to work with by making it even easier to shovel out yet more masses of code to deal with the even larger masses of AI-generated code. It does not take a genius to see that this ends up…

Hell, even with agreeing to a very rigid world view, that'd be a dream. Imagine an AI proof assistant that does two things:

1. writes more proofs, focusing on the area I point at

2. makes small, atomic, incremental, suggestions to make it easier to prove something; once those pass proofs+tests, go back to #1

But hey, that would likely require some sort of artificial mental models and iterative reasoning, and not just slapping more compute+data together into a word generator...

Re: Types as Interfaces

#170

Post by taeric »

smackmybishop wrote: post #167
taeric wrote: post #149

Earlier quoted context omitted.

Protobufs are also a fun place to look for how much debate people will get into regarding required versus optional fields. Your post is taking an implicit "everything is optional" view. But, it does allow you to be stricter. Common Lisp Object System also touched on all of these ideas years ago.

Everything has been `optional` for about a decade. > The option to set a field to required is absent in proto3 and strongly discouraged in proto2. https://protobuf.dev/overview/#syntax

Ah, I dropped off protobuf a while back. I definitely remember a lot of uproar about it, at the time.
Post reply on HN