Concepts and type-checking generics

[Araq]

Concept redesign

Goals:

• Empower concepts to make generic code type-checkable at declaration time,
  not only at instantiation time.
• Make concepts easier to understand and easier to implement.
• Provide an escape hatch in generic code so that e.g. adding a
  debug echo or log statement does not require a far reaching type
  constraint addition.
• Old code with unconstrainted generic parameters keeps to work.
• Do not base concept's implementation on system.compiles which is
  under-specified in Nim, very tied to the current implementation, and
  finally, slow.

Non goals:

• Support every little detail that the old concept design supported. For this
  we have the escape hatch plus the fact that you can leave your T
  underspecified.
• Support accidentical features. ("Look! With this hack I can specify that the
  proc needs a cdecl calling convention!")
• Support "cross parameter" constraints like "sizeof(a) == sizeof(b)". I have
  yet to see convincing examples of these cases. In the worst case, we could
  add enableif for this without bloating the concept's design.
• Turning concepts into "interfaces". This can already be accomplished with
  macros. Having said that, since these concepts are declarative, they are
  easier to process with tooling and arguably easier to process with macros
  as well.

Atoms and containers

Concepts come in two forms: Atoms and containers. A container is a generic
concept like Iterable[T], an atom always lacks any kind of generic
parameter (as in Comparable).

Syntactically a concept consists of a list of proc and iterator
declarations. There are 3 syntatic additions:

• Self is a builtin type within the concept's body stands for the
  current concept.
• each is used to introduce a generic parameter T within the
  concept's body that is not listed within the concept's generic
  parameter list.
• either orelse is used to provide basic support for optional
  procs within a concept.

We will see how these are used in the examples.

Atoms

  type
    Comparable = concept # no T, an atom
      proc cmp(a, b: Self): int

    ToStringable = concept
      proc `$`(a: Self): string

    Hashable = concept
      proc hash(x: Self): int
      proc `==`(x, y: Self): bool

    Swapable = concept
      proc swap(x, y: var Self)

Self stands for the currently defined concept itself. It is used to avoid
a recursion, proc cmp(a, b: Comparable): int is invalid.

Containers

A container has at least one generic parameter (most often called T). The
first syntactic usage of the generic parameter specifies how to infer and bind T.
Other usages of T are then checked to match what it was bound to.

  type
    Indexable[T] = concept # has a T, a collection
      proc `[]`(a: Self; index: int): T # we need to describe how to infer 'T'
      # and then we can use the 'T' and it must match:
      proc `[]=`(a: var Self; index: int; value: T)
      proc len(a: Self): int

Nothing interesting happens when we use multiple generic parameters:

  type
    Dictionary[K, V] = concept
      proc `[]`(a: Self; key: K): V
      proc `[]=`(a: var Self; key: K; value: V)

The usual ": Constraint" syntax can be used to add generic constraints to
the involved generic parameters:

  type
    Dictionary[K: Hashable; V] = concept
      proc `[]`(a: Self; key: K): V
      proc `[]=`(a: var Self; key: K; value: V)

each T

Note: each T is currently not implemented.

each T allows to introduce generic parameters that are not part of a
concept's generic parameter list. It is furthermore a special case to
allow for the common "every field has to fulfill property P" scenario:

  type
    Serializable = concept
      iterator fieldPairs(x: Self): (string, each T)
      proc write(x: T)


  proc writeStuff[T: Serializable](x: T) =
    for name, field in fieldPairs(x):
      write name
      write field

either orelse

Note: either orelse is currently not implemented.

In generic code it's often desirable to specialize the code in an ad-hoc manner.
system.addQuoted is an example of this:

  proc addQuoted[T](dest: var string; x: T) =
    when compiles(dest.add(x)):
      dest.add(x)
    else:
      dest.add($x)

If we want to describe T with a concept we need some way to describe optional
aspects. either orelse can be used:

  type
    Quotable = concept
      either:
        proc `$`(x: Self): string
      orelse:
        proc add(s: var string; elem: self)

  proc addQuoted[T: Quotable](s: var string; x: T) =
    when compiles(s.add(x)):
      s.add(x)
    else:
      s.add($x)

More examples

system.find

It's straight-forward:

  type
    Findable[T] = concept
      iterator items(x: Self): T
      proc `==`(a, b: T): bool

  proc find(x: Findable[T]; elem: T): int =
    var i = 0
    for a in x:
      if a == elem: return i
      inc i
    return -1

Sortable

Note that a declaration like

  type
    Sortable[T] = Indexable[T] and T is Comparable and T is Swapable

is possible but unwise. The reason is that Indexable either contains
too many procs we don't need or accessors that are slightly off as they don't
offer the right kind of mutability access.

Here is the proper definition:

  type
    Sortable[T] = concept
      proc `[]`(a: var Self; b: int): var T
      proc len(a: Self): int
      proc swap(x, y: var T)
      proc cmp(a, b: T): int

Concept matching

A type T matches a concept C if every proc and iterator header
H of C matches an entity E in the current scope.

The matching process is forgiving:

• If H is a proc, E can be a proc, a func, a method, a template,
  a converter or a macro. E can have more parameters than H as long
  as these parameters have default values. The parameter names do not have
  to match.

• If H has the form proc p(x: Self): T then E can be a public
  object field of name p and of type T.

• If H is an iterator, E must be an iterator too, but E's parameter
  names do not have to match and it can have additional default parameters.

Escape hatch

Generic routines that have at least one concept parameter are type-checked at declaration time. To disable type-checking in certain code sections an untyped block can be used:

proc sort(x: var Sortable) = 
   ... 
   # damn this sort doesn't work, let's find out why:
   untyped:
      # no need to change 'Sortable' so that it mentions '$' for the involved
      # element type!
      echo x[i], " ", x[j]

EDITED 2021/03/09 self was renamed to Self and is what the experimental implementation uses.

[andreaferretti]

I would like to understand how to write the concepts in Emmy under this proposal. Currently they look like

type
  AdditiveMonoid* = concept x, y, type T
    x + y is T
    zero(T) is T
  AdditiveGroup* = concept x, y, type T
    T is AdditiveMonoid
    -x is T
    x - y is T
  MultiplicativeMonoid* = concept x, y, type T
    x * y is T
    id(T) is T
  MultiplicativeGroup* = concept x, y, type T
    T is MultiplicativeMonoid
    x / y is T
  Ring* = concept type T
    T is AdditiveGroup
    T is MultiplicativeMonoid
  EuclideanRing* = concept x, y, type T
    T is Ring
    x div y is T
    x mod y is T
  Field* = concept type T
    T is Ring
    T is MultiplicativeGroup

I guess they would become like this?

type
  AdditiveMonoid* = concept
    proc `+`(x, y: self): self
    proc zero(T: typedesc[self]): self
  AdditiveGroup* = concept
    self is AdditiveMonoid # will concept refinement be allowed?
    proc `-`(x: self): self
    proc `-`(x, y: self): self
  MultiplicativeMonoid* = concept
    proc `*`(x, y: self): self
    proc id(T: typedesc[self]): self
  MultiplicativeGroup* = concept
    self is MultiplicativeMonoid
    proc `/`(x, y: self): self
  Ring* = AdditiveGroup and MultiplicativeMonoid
  EuclideanRing* = concept
    self is Ring
    proc `div`(x, y: self): self
    proc `mod`(x, y: self): self
  Field* = Ring and MultiplicativeGroup

[Araq]

I guess they would become like this?

Yes.

self is AdditiveMonoid # will concept refinement be allowed?

I thought about it and we could support it via type AdditiveGroup = concept of AdditiveMonoid. I don't know if it is important enough that we really need it.

[mratsim]

I like the proposal. Can it deal with recursivity? That's important for my needs (mratsim/Arraymancer#299)

In Arraymancer I define a deep learning trainable layer like this but I don't use them at the moment as it's too brittle:

https://github.com/mratsim/Arraymancer/blob/bde79d2f73b71ece719526a7b39f03bb100784b0/src/nn_dsl/dsl_types.nim#L63-L81

type
  Variable[T] = object
    value: Tensor[T]
    gradient: Tensor[T]

  Tensor[T] = object
    data: seq[T]

  TrainableLayer*[TT] = concept layer
    block:
      var trainable: false
      for field in fields(layer):
        trainable = trainable or (field is Variable[TT])
      trainable

  Conv2DLayer*[TT] = object
    weight*: Variable[TT]
    bias*: Variable[TT]
  LinearLayer*[TT] = object
    weight*: Variable[TT]
    bias*: Variable[TT]
  GRULayer*[TT] = object
    W3s0*, W3sN*: Variable[TT]
    U3s*: Variable[TT]
    bW3s*, bU3s*: Variable[TT]
  EmbeddingLayer*[TT] = object
    weight*: Variable[TT]

#########
# sanity check

var convolution: Conv2DLayer[float32]
echo convolution is TrainableLayer[float32] # Why false?

#########
# user-defined

type
  MyNonLayer = object
    foo: int
    bar: float32
  MyLayer[TT] = object
    metadata: MyNonLayer
    weight: Variable[TT]

var x: MyNonLayer
var y: MyLayer[float32]

echo x is TrainableLayer[float32]
echo y is TrainableLayer[float32] # Why false

[Araq]

What does that even mean though? "Somewhere in the object type there must be a field of type Variable[T]"? How do you know which one? What if you have more than one?

[zah]

A) How come I must repeat in every discussion about concepts that any proposal must cover the requirements of associated types and constants? I guess it would have to be:

type Foo = concept
  proc ElemType(_: typedesc[self]): typedesc
  proc compressedSize(_: typedesc[self]): static[int]

I find it a bit funny how these result in syntax that is outlawed in regular Nim. And hey, why was proc chosen here? Isn't using func the recommended way for new Nim code?

---

B) A "container concept" must be able to infer static parameter values as well. For example

type FixedSizeMatrix[M, N: static[int]; T] = concept
  # How do I infer M and N here from a non-generic type?
  # In the current design it's done with:
  x.Rows == M
  x.Cols == N 

Please not that Rows and Cols can be templates defined over a non-generic type in order to adapt it to the concept requirements:

template Rows(T: type Matrix4x4): int = 4

Having the FixedSizeMatrix concept above, how do I define a different concept called SquareMatrix (where the rows and columns must be the same)? There are some algorithms that work only on square matrices.

---

C) The VTable types are a very important feature in the current concepts design, but I would agree that they can be delivered as a library.

---

D) I'd really like to have the converter type classes though and these require custom code in semcall/sigmatch.

---

E) Regarding the main idea here, mainly the type checking of generic functions, I would approach this with a lot of caution. The internal compiler structures can be defined and derived from the current concept syntax. I think it makes a lot of sense to try to experiment with the approach before making any major decisions about removing the existing concepts-related code in the compiler.

In particular, a lot of attention has to be put into code like the following:

https://github.com/status-im/nim-beacon-chain/blob/master/beacon_chain/ssz/types.nim#L85-L101

func isFixedSize*(T0: type): bool {.compileTime.} =
  mixin toSszType, enumAllSerializedFields

  when T0 is openarray|Option|ref|ptr:
    return false
  else:
    type T = type toSszType(default T0)

    when T is BasicType:
      return true
    elif T is array:
      return isFixedSize(ElemType(T))
    elif T is object|tuple:
      enumAllSerializedFields(T):
        when not isFixedSize(FieldType):
          return false
      return true

Notice how the function accepts an underspecified type, but it discovers a more detailed type using the is operator. Then the function is able to use operations defined over this more detailed type. This is a very convenient construct enabled by the current lax rules of Nim and we should not lose it.

[mratsim]

What does that even mean though? "Somewhere in the object type there must be a field of type Variable[T]"? How do you know which one? What if you have more than one?

I don't care which field, but as long as there is a "Variable[T]" field, the user-defined type constitutes a TrainableLayer indeed. All deep-learning libraries work like that, except that they use dynamic dispatch and inheritance from a Layer class.

[Araq]

How come I must repeat in every discussion about concepts that any proposal must cover the requirements of associated types and constants?

Because it's covered by the proposal as you noticed yourself.

Isn't using func the recommended way for new Nim code?

func could be allowed but then require func'ness in the matching process. Though I think it doesn't matter. ;-)

Static T could be done like so:

type FixedSizeMatrix[M, N: static[int]; T] = concept
  proc rows(x: self): M
  proc cols(x: self): N

I'd really like to have the converter type classes though and these require custom code in semcall/sigmatch.

Well the proposal implies that we have dedicated, custom code for concept matching, moreso than currently.

I think it makes a lot of sense to try to experiment with the approach before making any major decisions about removing the existing concepts-related code in the compiler.

Of course.

In particular, a lot of attention has to be put into code like the following:

That code is not affected, under-constrained generics continue to exist and your isFixedSize does not use a concept. I should stress that only real concepts that use the concept keyword trigger the type-checking for generics. Of course, we could also come up with a different rule when exactly this checking is triggered, we need to tinker with it -- a lot.

[zah]

  proc rows(x: self): M
  proc cols(x: self): N

Hrm, you are using a static value as a return type. Seems like an irregularity to me.

---

My underspecified code shouldn't be ruled out as "non using concepts". I could have easily constrained the input type with a concept such as SszSeriazable (or any other type class for that matter). It's just a lucky coincidence that this particular example is not doing this. My general remark is that the pattern of using when X is Y inside generics is a very nice alternative to overloading in many situations and the type checking engine should accommodate it.

[Araq]

Well the eternal question is "is static[int] a type or a value?". ;-) My RFC assumes it's actually a type.

[Araq]

My underspecified code shouldn't be ruled out as "non using concepts". I could have easily required a concept such as SszSeriazable in place of the auto type there (or any other type class for that matter).

Well no, under this RFC it couldn't "easily require" such a thing. If you cannot be precise about the generic type constraints, don't fake it with an imprecise concept, use an unconstrained generic instead. If you don't like this, fine, but that it is what this RFC says.

[zah]

Well the eternal question is "is static[int] a type or a value?". ;-) My RFC assumes it's actually a type.

I've never understood why you insist that values bound to static parameters are "types". Can they be passed to functions accepting regular values - yes. When you initialize a constant from a static[int] parameter, what's the type of the constant - it's int. Where should be the compilation error in the following code:

proc foo(N: static int) =
  const N2 = N
  proc bar(a: N) = discard
  proc baz(a: N2) = discard

For me, the "eternal" question has a very definitive answer. The static parameters are values having tyStatic as a modifier (just like the var parameters are values having tyVar as a modifier).

[zah]

Here is some more fun. If we continue with the "static parameters are types" thinking, we reach the following:

type 3DTransform = concept
  self is FixedSizeMatrix 
  proc cols(x: self): 4
  proc rows(x: self): 4

[Araq]

Here is some more fun...

I'm not sure you're asking the right question. You are thinking about whether these alternative concepts can support what the current concepts can. But the real question is why does it matter to infer the value 4 in order to type-check a generic? And how often does it matter to be able to do this?