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

31–40 of 197 posts

Re: Types as Interfaces

#31

Post by fmbb »

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…

> Have any languages achieved this?

”The MLs” solved it decades ago. Standard ML has very nice record types.

Re: Types as Interfaces

#33

Post by user3939382 »

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.

Re: Types as Interfaces

#34

Post by giraj »

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 construction of the type 'Map' is entirely standard in languages like Agda and Coq (and I bet Idris too). In these languages, Type is itself a type, and can be treated like any other type (like string or int). Nothing clunky about it. (If you're curious, Type is usually referred to as a "universe type" in type theory circles.)

Re: Types as Interfaces

#35

Post by BugsJustFindMe »

tinix wrote: post #23

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

> interfaces describe behavior, types describe shape and structure

Shape and structure are behavior. There's more to behavior than "abstractly produces X result". Behavior is "produces X result in Y form given Z in W form".

Re: Types as Interfaces

#36

Post by valenterry »

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.

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.

Re: Types as Interfaces

#37

Post by pydry »

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 diminishing returns affects tests in reverse. They tend to be good at what the other is bad at and if you rely too heavily on one at the expense of the other they will start fraying around the edges.

Re: Types as Interfaces

#38

Post by pmarreck »

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.

Idris is fascinating. I actually took the book about it on vacation with me. Software reliability is becoming increasingly important as we tie all these systems together because it multiplies the number of possible unanticipated failure modes.

Regarding the ultimate utility of languages initially considered "academic," the languages Lisp, Haskell, Prolog, Scala, Erlang and OCaml would like to have a word ;)

Re: Types as Interfaces

#39

Post by pmarreck »

valenterry wrote: post #36
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.

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?

Re: Types as Interfaces

#40

Post by andsoitis »

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.

> arbitrary rules a programmer knows about the bounds of a value

Ada's generalized type contracts using subtype predicates work pretty well for this: https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel...

You can use it for something as simple as expressing ranges, or to represent types with arbitrary constraints, including types with discontinuities.

Post reply on HN