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

51–60 of 197 posts

Re: Types as Interfaces

#51

Post by Xen9 »

Differences in foundational understanding & unteachability of foundational research causes inevitably ton of confusion in texts on formal science ideas outside a known academic context.

This text should not fascinate a programmer but create frustration of two types: (1) Frustration on one's lack of small pieces knowledge (2) Frustration that NOW you will not have the chance to invent this on your ow; your creative process takes damage.

Out of which the second type should be the one that makes majority of cases.

ALSO this should cause one to have respect of form: "hey, this programmer was probably at least smart enough to figure out this alone."

Perhaps most polite woule be to, for every text, in the situation to have notice at beginning: "For programmers who already have thought about what would happen were you to add X to Y but so that Z enough to probably not to get new ideas in this context."

Re: Types as Interfaces

#52

Post by kqr »

andsoitis wrote: post #40
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.

But these are only promised to be checked at runtime, even though the compiler can sometimes hint at things earlier.

Re: Types as Interfaces

#53

Post by docandrew »

kqr wrote: post #52
andsoitis wrote: post #40

Earlier quoted context omitted.

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

But these are only promised to be checked at runtime, even though the compiler can sometimes hint at things earlier.

With SPARK mode you can check them at compile-time with provers and elide the runtime checks. You can do _very_ sophisticated type predicates this way.

Re: Types as Interfaces

#54

Post by turboponyy »

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 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, which can actually make the program easier to understand for both the reader and the writer by leaving some things unsaid.

Of course, whether a program is easier to understand when its invariants are written down vs. when they are left to be inferred by the reader is probably a matter of circumstance, so different tools for different jobs and all that.

I've recently been writing a small program in Go - my first foray into the language - and I thoroughly enjoy how it gets out of my way. The lack of rigor is freeing if you don't stop to think about it too much.

Re: Types as Interfaces

#55

Post by packetlost »

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…

Go structs sorta behave this way if you put a "parent" struct in the first field of a struct definition. They are, of course, not maps though. But a map with statically defined keys/values/types is basically a struct.

Re: Types as Interfaces

#56

Post by pmarreck »

valenterry wrote: post #44
pmarreck wrote: post #39

Earlier quoted context omitted.

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?

ah, I think I misunderstood. Still getting through the Idris book :)

Re: Types as Interfaces

#57

Post by lenkite »

sltkr wrote: post #26
lenkite wrote: post #21

Earlier quoted context omitted.

Not sure whether this is what you intended, but Go structs can embed other structs type Foo struct { foo int } type Bar struct { bar string } type FooBar struct { Foo Bar }

This doesn't function as an interface though. You cannot pass a FooBar to a function that expects a Foo, for example, and although you can fairly easily reference the Foo-part of a FooBar instance (`foobar.Foo`) there is no way to pass e.g. an array of FooBar instances to a function that takes a slice of Foo[] as its argument. That's the problem to be solved.

Ok, Go generics is pretty limited but you can achieve this in C++ via concepts.

    #include 
    #include 
    #include 

    // Concept to check for 'foo' field of type int
    template 
    concept HasFooInt = requires(T t) {
        { t.foo } -> std::convertible_to;
    };

    // Concept to check for 'bar' field of type string
    template 
    concept HasBarString = requires(T t) {
        { t.bar } -> std::convertible_to;
    };

    // Generic function that accepts T with either 'foo' or 'bar'
    template 
    requires HasFooInt || HasBarString
    void printField(const T& t) {
        if constexpr (HasFooInt) {
            std::cout ) {
            std::cout

Re: Types as Interfaces

#58

Post by nottorp »

pmarreck wrote: post #38
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 ;)

But most of those don't have a real type system though? And definitely not a strict one.

Re: Types as Interfaces

#59

Post by harporoeder »

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.

With dependent types you still end up having to do dynamic checking of invariants for a substantial portion of real world code to construct the value with the properties you want. Anything coming from disk or network or a database etc. In practice I feel that it is far easier to just do manual dynamic checking with the constructor hidden from other modules such as `constructEmail :: string -> Email' which uses normal value level code, a common Haskell pattern. Obviously a little less flexible for the common dependent type examples of such as appending two vectors of a specific length.

Re: Types as Interfaces

#60

Post by posix_monad »

PoignardAzur wrote: post #27
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…

Ok, but why? I like the beauty of an expressive type system as much as the next guy, but is there any scenario where: type FooBar = mergeMaps Foo Bar Is better for solving real-world problems than type FooBar = { "_foo", Foo, "_bar", Bar } or whatever?

With mergeMaps, you don't have to write out all of the properties.
Post reply on HN