4 ms·

I dislike concepts because it seems to be a half measure; one that is already causing them pains in the design. For example the issues with, implied constraint

by zbobet2012 8y ago

I dislike concepts because it seems to be a half measure; one that is already causing them pains in the design. For example the issues with, implied constraints, infinite types, and parametric methods could be solved by using something more properly founded in type theory. Concepts are effectively refinement types[1] and a properly founded implementation from type theory would mitigate these issues. [1] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type

phillipcarter 8y ago
What "properly founded implementation" would you suggest? Concepts are not "effectively" refinement types.
- zbobet2012 8y ago
  Combative a bit are we? I mean something properly founded in type theory, like say _refinement types_ as implemented in liquid haskell: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/LiquidHaskell_ICFP14.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... . Constraints of course are _not_ refinement types, but very close to a _subset_ of refinement types. Specifically they have deep similarity to Refined Type Classes from the above paper. Having used Idris, LiquidHaskell, and F* to implement provable algorithms for some distributed systems I _don't_ think Go should go down that route. The techniques are simply not simple or clean enough for more general purpose languages. But having a type system which has a subset of those feature, and which stands on firmer mathematical firmament lets you reason about stuff like "which of these two programs is okay: ``` // OK type List(type T) struct { elem T next List(T) } // NOT OK - Implies an infinite sequence of types as you follow .next pointers. type Infinite(type T) struct { next Infinite(Infinite(T)) }``` Which the go authors see as problematic: > "It is unclear what the algorithm is for deciding which programs to accept and which to reject." Idris certainly has no problem choosing which ones should and should not be used.
  - ianlancetaylor 8y ago
    I don't think there is any lack of clarity about your List example; that is clearly forbidden. The example that is less clear is the one that generates a million types and then stops. A similar issue arises in C++; the C++ standard says that there is an implementation defined limit on the total depth of recursive instantiations. Perhaps Go should do something similar.
    - zbobet2012 8y ago
      C++'s method is certainly a practical way to limit expansion on inductively defined data types. I think a better way would be to construct a type system _opposite_ of most constructed today (which focus on the ability to express problems) and instead intentionally limit the types we are able to construct to those with "easy to use" and computationally efficient properties. Consider this sample. We want to be able to define inductive types such as `List(T)`, but not `InfiniteList(T)` or `BigArray(T)`. While `BigArray(T)` is an interesting construct (it's effectively a dependent type)* it jumps past the "can I keep it in my head" smell test for me. As soon as a I have to reason deeply about what a type constructor does it just doesn't feel like Go to me. So we want to be able to construct types which are inductive but can only calculate a single type. List{T} calculates one type, BigArray calculates _n_ types, and InfiniteList calculates an infinite number of types. * In Idris one would write something like: data BigArray : (n : Nat) -> (l : List m) -> Type where Z l : Vect Z v n l : Vect n l
  - phillipcarter 8y ago
    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.
- johncolanduoni 8y ago
  In some dependently typed languages they can be easily implemented via refinement types, where the “refinements” are the implementations of the typeclass requirements. Idris is a good example of this approach. It has the advantage of making typeclasses first-class, and of enabling a lot of additional functionality without additional fundamental constructs. It is however very antithetical to what someone means when they say Go is minimalistic.

phillipcarter 8y ago

What "properly founded implementation" would you suggest? Concepts are not "effectively" refinement types.

zbobet2012 8y ago
Combative a bit are we? I mean something properly founded in type theory, like say _refinement types_ as implemented in liquid haskell: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/LiquidHaskell_ICFP14.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... . Constraints of course are _not_ refinement types, but very close to a _subset_ of refinement types. Specifically they have deep similarity to Refined Type Classes from the above paper. Having used Idris, LiquidHaskell, and F* to implement provable algorithms for some distributed systems I _don't_ think Go should go down that route. The techniques are simply not simple or clean enough for more general purpose languages. But having a type system which has a subset of those feature, and which stands on firmer mathematical firmament lets you reason about stuff like "which of these two programs is okay: ``` // OK type List(type T) struct { elem T next List(T) } // NOT OK - Implies an infinite sequence of types as you follow .next pointers. type Infinite(type T) struct { next Infinite(Infinite(T)) }``` Which the go authors see as problematic: > "It is unclear what the algorithm is for deciding which programs to accept and which to reject." Idris certainly has no problem choosing which ones should and should not be used.
- ianlancetaylor 8y ago
  I don't think there is any lack of clarity about your List example; that is clearly forbidden. The example that is less clear is the one that generates a million types and then stops. A similar issue arises in C++; the C++ standard says that there is an implementation defined limit on the total depth of recursive instantiations. Perhaps Go should do something similar.
  - zbobet2012 8y ago
    C++'s method is certainly a practical way to limit expansion on inductively defined data types. I think a better way would be to construct a type system _opposite_ of most constructed today (which focus on the ability to express problems) and instead intentionally limit the types we are able to construct to those with "easy to use" and computationally efficient properties. Consider this sample. We want to be able to define inductive types such as `List(T)`, but not `InfiniteList(T)` or `BigArray(T)`. While `BigArray(T)` is an interesting construct (it's effectively a dependent type)* it jumps past the "can I keep it in my head" smell test for me. As soon as a I have to reason deeply about what a type constructor does it just doesn't feel like Go to me. So we want to be able to construct types which are inductive but can only calculate a single type. List{T} calculates one type, BigArray calculates _n_ types, and InfiniteList calculates an infinite number of types. * In Idris one would write something like: data BigArray : (n : Nat) -> (l : List m) -> Type where Z l : Vect Z v n l : Vect n l
- phillipcarter 8y ago
  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.
johncolanduoni 8y ago
In some dependently typed languages they can be easily implemented via refinement types, where the “refinements” are the implementations of the typeclass requirements. Idris is a good example of this approach. It has the advantage of making typeclasses first-class, and of enabling a lot of additional functionality without additional fundamental constructs. It is however very antithetical to what someone means when they say Go is minimalistic.