4 ms·

Although I don't think they called out refinement types as a possibility (I only skimmed near the end), I wouldn't be surprised if they quickly determined that

Although I don't think they called out refinement types as a possibility (I only skimmed near the end), I wouldn't be surprised if they quickly determined that tackling undecidability is not a goal of the Go type system. Especially since every attempt at refinement types (or even nontrivial constraints) ends up with a compiler that gets really slow, and fast compilations are one of the tenets of the language. Go contracts as-written, or "accept a T that can do a thing and have a default implementation", is orthogonal to refinement types. N.B. I'd really love to see refinement types break past the acceptable threshold of compilation time, since they're really neat and are easy to explain to people in terms of their usefuless.

zbobet2012 8y ago
My thoughts here are based on this section of the generics draft: > We would like to understand better if it is feasible to allow any valid function body as a contract body. A generic function to compute a type is _very much_ in the realm of both refinement and dependent types. The BigArray example (as mentioned in a sister thread) is just a dependent type. > The hard part is defining precisely which generic function bodies are allowed by a given contract body. .. We are most uncertain about exactly what to allow in contract bodies, to make them as easy to read and write for users while still being sure the compiler can enforce them as limits on the implementation. That is, we are unsure about the exact algorithm to deduce the properties required for type-checking a generic function from a corresponding contract. My proposal/goal here is to define a type system, or set of constructors which has nice, formally provable limits on what can be constructed. Those constructs should be both easy to grasp _and_ computationally simple. As you say _general_ refinement types are not suited for a compiler focused on speed; however, a subset can very well be.
- pjmlp 8y ago
  Yes, I would already be more than happy with what CLU allowed for.

zbobet2012 8y ago

My thoughts here are based on this section of the generics draft: > We would like to understand better if it is feasible to allow any valid function body as a contract body. A generic function to compute a type is _very much_ in the realm of both refinement and dependent types. The BigArray example (as mentioned in a sister thread) is just a dependent type. > The hard part is defining precisely which generic function bodies are allowed by a given contract body. .. We are most uncertain about exactly what to allow in contract bodies, to make them as easy to read and write for users while still being sure the compiler can enforce them as limits on the implementation. That is, we are unsure about the exact algorithm to deduce the properties required for type-checking a generic function from a corresponding contract. My proposal/goal here is to define a type system, or set of constructors which has nice, formally provable limits on what can be constructed. Those constructs should be both easy to grasp _and_ computationally simple. As you say _general_ refinement types are not suited for a compiler focused on speed; however, a subset can very well be.

pjmlp 8y ago
Yes, I would already be more than happy with what CLU allowed for.