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

41–50 of 197 posts

Re: Types as Interfaces

#41

Post by valenterry »

auggierose wrote: post #28

Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this.

Typescript can't really be this language because it is impeded by having to work with the javascript runtime, which makes this task much much harder to do.

Re: Types as Interfaces

#42

Post by indulona »

problem of known types, or interfaces, as values is that conditions for the value format or validation changes based on context. so you might have a price that is valid in one context but not in another(like a negative value). the problem then occurs on the input where you might let in value that is valid on higher level but not on deeper level and by the time you detect it it might be too late(you have committed a transaction with invalid data).

Re: Types as Interfaces

#43

Post by h1fra »

auggierose wrote: post #28

Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.

Foo and Bar are now compatible with FooBar which can create a lot of issues even in strict mode. Typescript is amazing, but interfaces not being struct are a footgun in many places

Re: Types as Interfaces

#44

Post by valenterry »

pmarreck wrote: post #39
valenterry wrote: post #36

Earlier quoted context omitted.

Sadly this is true and I 100% agree. After reading and working through type-level programmin in Idris, this is the conclusion I came to.

What made it seem too restrictive to you? Or what were your experiences trying to apply it to real-world scenarios?

I'm not sure what you mean. I don't find Idris restrictive (except for the lack of union types with subtyping). Rather I find any mainstream language very restrictive - or is that what you meant?

Re: Types as Interfaces

#45

Post by thwarted »

brabel wrote: post #19
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…

The Ceylon language allowed you to do that sort of thing with types. If you "added" two maps together of types `Map ` and `Map `, you would get back a `Map ` (or, equivalently, `Map | Map `). But for some slightly complex reasons, most language designers find adhoc union types (which are required for this to work) a bad idea. See the Kotlin work related to that, they explicitly want to keep that out of the language (…

> you would get back a `Map` (or, equivalently, `Map | Map`)

How are these equivalent? Wouldn't the latter result in {foo:1, foo:"two"}, where the former wouldn't?

Re: Types as Interfaces

#46

Post by auggierose »

valenterry wrote: post #41
auggierose wrote: post #28

Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this. Typescript can't really be this language because it i…

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.

Re: Types as Interfaces

#47

Post by williamdclt »

h1fra wrote: post #43
auggierose wrote: post #28

Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.

Foo and Bar are now compatible with FooBar which can create a lot of issues even in strict mode. Typescript is amazing, but interfaces not being struct are a footgun in many places

What do you mean by "compatible"? You couldn't assign a `Foo` to a `FooBar` variable unless all `Bar` properties are optional

Re: Types as Interfaces

#48

Post by williamdclt »

auggierose wrote: post #28

Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.

Elixir is taking a similar direction if I'm understanding correctly (they seem to insist their type system is fundamentally from Typescript's, but to this day I cannot understand how, both are structural and based on set theory)

Re: Types as Interfaces

#49

Post by ParetoOptimal »

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.

Haskell has real world examples, for instance:

https://docs.servant.dev/en/stable/tutorial/ApiType.html

Re: Types as Interfaces

#50

Post by Quekid5 »

pydry wrote: post #37
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 think there's a sharp rule of diminishing returns the stronger you make type systems. Type safety comes at a cost and that cost has to come with an associated payoff. This is why ultra strong type systems end up being little more than academic toys - the payoff when you dial type safety up to an extreme doesn't match the associated cost. Types and tests should meet somewhere in the middle because the same law of di…

In Idris you get to choose how strict you want to make your types. E.g. you can choose to use "Vect n a" if you want a vector a's where the size is tracked by the type system. Or you can use e.g. "List a" if you want a list of a's where the size is not tracked by the type system.

Of course the problem comes when you have to interface some code which expects a "Vect n a" and you have a "List a", but that's solvable by simply checking the size (dynamically) and deciding what to do if your "List a" isn't of size exactly n. (Fail, or whatever.). Going from "Vect n a" to a "List a" is trivial, of course.

... but really, that's where most of the friction is: Boundaries between APIs where the types don't quite line up. (Which is often the case for other languages, tbf. We tend to just notice less at compile time since most languages are so bad at expressing constraints.)

Post reply on HN