Hi Ian, I'm actually not in favor of dependent types -- this might have come wrong "over the line". I find them limiting and confusing in practice (but I have limited experience, mostly in C++ if you could call template hacks really dependent types...).
I expect most applications to need wider family of behavioral contracts -- and I doubt that Go would ever support them natively lest there's a decision to sacrifice simplicity for modeling correct programs*.* At the company I work at we are currently pretty happy with run-time enforcement of the contracts and I'm not even sure whether a static checker would be a huge benefit. Having something like Optional type would be probably the most important contribution to the correctness to prevent nil pointer errors (and make writing a static checker easier), but I suppose that would be possible with any sort of generic types in Go2. I'd suggest somebody starts a different thread on behavioral contracts if there is interest and we leave this discussion to people interested in type contracts. On Tue, 27 Nov 2018 at 16:11, Ian Denhardt <i...@zenhack.net> wrote: > Odd that the paper you chose to link to is one specifically addressing a > difficulty integrating the ideas with Java's class hierarchies -- while > the broader subject may be relevant to Go, I don't think that paper is. > > Wrt Dan's question of doing static checks, I'll quote the paper: > > > In principle, one could try to prove the correctness of behavioral > > contracts. For example, the Extended Static Checking group at > > Digital has developed verification tools for Java and Modula 3 [3]. > > In general, however, the languages used to express behavioral con- > > tracts are rich enough that it is not possible to verify statically > > that the contracts are never violated. > > So it's not talking about a compile-time mechanism. > > To make Tamas's idea work you'd need to (a) have numbers encoded in the > type system somehow, and (b) actually be able to relate them to the size > of the arrays. You can do this with dependent types, but integrating > those into a practical programming language is still a very open > research topic. > > You can hack around this in some circumstances; there are tricks you can > play to represent numbers at the type level in a somewhat limited, > clumsy way. But most of the trickery I've seen relies on one feature or > another that Go doesn't have, and the result is always somewhat > cumbersome. > > -Ian > -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
