Hi Guys,
I need your help. In the past two weeks I spent roughly 30 hours debugging the compiler to add proper concept[T] support. It feels like I'm at half of the work. Now I'm stuck at a language design question, how to find out T in concept[T]. I don't have a good proposal. Please take some time to think about this. I really should go back to push my regular work, so I'm trying to close this issue as soon as possible.
When you read the following examples then you might think that these are easy questions, and the compiler should be smart enough. Please keep in mind that we eventually want to use concept[T] for types like Map[ Map[int, string], Map[seq[Map[int, int]], float]]. Also, the main motivation is to create a function like proc getKeyWithLowestValue[K,V]( map: Map[K,V] ): K which could work on multiple map implementation (like HashMap, TreeMap in Java).
So let's start with the current stage. If you write this:
type StrangeConcept[T] = concept c
c is T # Equivalent to "c is any", which is true
float(c) is T # Equivalent to "float(c) is any", which is true
$c is T # Equivalent to "$c is any", which is true
when int is StrangeConcept:
echo "Yes, it is" # this is printed
type NewConcept[T] = concept c
c is seq[T]
...
type YouCanAddOne[T] = concept c
c is T
c+1 is T
Let's continue the examples:
type MixWithFunctions1[T] = concept c
f[T](c)
...
type MixWithFunctions2[T] = concept c
f(c, (new T)[])
...
Somewhat cleaner approach:
type ShouldBeClearConcept[T] = concept c
type T = type( c[0].getFirstValue() )
...
What's your opinion?
Now I'm stuck at a language design question, how to find out T in concept[T]
Congratulations. you're definitely on the right track! :-) That's the tough nut. I have the following proposal, but I'm not sure it answers every one of your questions. The idea is that concept[T, ...] is always used for containers and thus the T should always be the container's element type. This means that concepts like Comparable cannot have a T since int is Comparable, but not a container.
Let's assume these definitions:
type
One[T] = concept
...
Two[S, T] = concept
...
The body is not relevant, since the body is not used to infer S and T.
After the inference rules, the concept body is checked and if that matches too, we have a match, otherwise we don't.
Let's go through your examples now.
type StrangeConcept[T] = concept c
c is T # Equivalent to "c is any", which is true
float(c) is T # Equivalent to "float(c) is any", which is true
$c is T # Equivalent to "$c is any", which is true
when int is StrangeConcept:
echo "Yes, it is" # this is printed
Nope, it should be:
type StrangeConcept = concept c
c is type(c) # Equivalent to "c is any", which is true
float(c) is type(c) # Equivalent to "float(c) is any", which is true
$c is type(c) # Equivalent to "$c is any", which is true
No container, hence no T. As a workaround you need to write type(c). A clean solution IMO.
type NewConcept[T] = concept c
c is seq[T]
...
Works.
type YouCanAddOne[T] = concept c
c is T
c+1 is T
Doesn't work this way, numbers are not containers. type(c) is the workaround.
type MixWithFunctions1[T] = concept c
f[T](c)
...
type MixWithFunctions2[T] = concept c
f(c, (new T)[])
...
Maybe this implies the inference rules need to cover proc (S, ...): T too? Oh well, you can extend them. But I don't think this needs to be supported for version 1 of the concepts implementation.
@Araq I feel that restricting Concept[T] to containers is very limiting and will in fact make it impossible to define many abstractions.
Let me give an example. In emmy I have more or less the following defition of a field.
type Field = concept x, y
x + y is type(x)
zero(type(x)) is type(x)
-x is type(x)
x - y is type(x)
x * y is type(x)
id(type(x)) is type(x)
x / y is type(x)
Here a field is defined as a type that admits the usual four operations and their identity elements - no need for generic concepts here (and in fact i works, more or less).
Say that now I want to define a vector space over a field. The obvious definition would be
type VectorSpace[K] = concept x, y
x + y is type(x)
zero(type(x)) is type(x)
-x is type(x)
x - y is type(x)
var k: K
k * x is type(x)
and this requires generic concepts.
Now the problem is: how does one infer K in this example (or T in any of the examples above)?
My proposal would be to make the compiler only test for concepts when all types are fully specialized. This is the same that happens for generics right now.
So, there would be no way to check that a type T belongs to VectorSpace[K] for some K, but we could check that it belongs to VectorSpace[float].
But we can still write generic functions having such constraint as T: VectorSpace[K]. The only problem is that the compiler will bail out at this point because K cannot be inferred. This can be easily fixed by
static:
assert T is VectorSpace[float]
or whatever we come up with. The compiler will then accumulate such facts and use them to resolve K in such situations as above.
What do you think?
This works:
type
Node* = concept n
`==`(n, n) is bool
Graph* = concept g
var x: Node
distance(g, x, x) is float
Applying it to your example yields:
type VectorSpace = concept x, y
x + y is type(x)
zero(type(x)) is type(x)
-x is type(x)
x - y is type(x)
var k: Field
k * x is type(x)
Thanks for taking the time to reply.
Just a quick reply, I didn't have time to think about the answers too much.
@Araq: I think that your proposal would work not only for containers. It would probably work for channels, streams, files as well.
@andrea: I understand the motivation, I'll think about this.
I can think of an example where the concept = container logic fails. Let's assume that we have Set[T] concept, and one would like to implement it for T=char by using a bitfield (that's 4 times 64-bit int, so it is an array[4, int]). This could be Set[char], however, there is no char in this type's syntax.
Also, Andrea, you are right. You would like to have several concept types with a small difference, where the difference is in one of the types. And that is what generics is for.
Repeating the obvious, these are the two cases we would like to have:
proc giveFirstValue[K,V](m : Map[K,V]): V = ... # here Map[K,V] defines K, V
proc RandomLinearCombination(x, y: VectorSpace[float]): auto = ... # here VectorSpace[T] needs to know T
How about having both of these? We could introduce the generic symbols within the concept, they would be the given types, or if no type is available, then the default value would be a type which doesn't match to anything. And they would be mutable.
For example
type ThisRequiresType[T] = concept c
c[0][0].foo[0] is T
c + c is int
The other example:
type ContainerWithAddableElements[T] = concept c
T = type(c[0])
c[0] + c[0] is T
So again, the steps would be: we introduce symbols for every generics at the beginning of the concept, they are mutable, and their values are the given ones, or if we cannot infer them, then they would be a type which matches nothing. The evaluation needs to be successful to continue, and then we check the values of these type symbols, and match them with any generics if we are in a function declaration.
What do you think?
Peter
I can think of an example where the concept = container logic fails. Let's assume that we have Set[T] concept, and one would like to implement it for T=char by using a bitfield (that's 4 times 64-bit int, so it is an array[4, int]). This could be Set[char], however, there is no char in this type's syntax.
I don't understand this example at all. Besides, you can always introduce helper types to perform the matching as you please type Swapper[T,S] = Cont[S, T].
proc RandomLinearCombination(x, y: VectorSpace[float]): auto = ... # here VectorSpace[T] needs to know T
Since a VectorSpace[float] is exactly the same as float, there still is no need to parametrize VectorSpace.
What do you think?
Seems to be more complex than my solution, but it also seems to me that you described Zahary's solution (I skyped with him about it), so it could be fine. ;-)
So my Set[T] example wasn't clear enough. I wanted to have a mathematical set of unsigned bytes (like {3,4,5}, which becomes {1,3,4,5} after adding 1). This can be implemented with array[4, int]. I can't see how this could match for Seq[byte] with your trick, because array[4, int] contains no bytes.
The VectorSpace[float] has generators, dimension, subspace, all the nice math properties (it can be float, array[3, float], array[N, float], etc).
I don't know Zahary, but he must be a smart guy :P
Let's sleep a couple of days on this, then if everybody is on the same page, then I'll try to put together a PR.
Peter
I don't know Zahary, but he must be a smart guy
lmao <3
I really don't know much about type inference. I feel like the naive solution would be enough for the common cases and manually adding type annotations would cover the rest, though. Even if it does compute the wrong result it would error out like a normal generic, or do another check for generics after the first pass to get a better error message.
It probably would be possible to collect type constraints before anything else and solve them without exponential runtime explosions? Anyway, that seems like something that could be added at in a later version?.
A naive implementation that goes through all possibilities via backtracking probably wouldn't be too bad either as long as there aren't any procs with huge numbers of overloads and the implementation throws mismatches out early. In that case there probably should be a sanity limit at which the compiler gives up, though, or you get stuff like swift's hours of compile time for seemingly simple expressions.
This is a long shot but I figured I'd ask if only to provide an interesting use-case for concepts.
How far is the current design (& implementation) from supporting the definition of Tuple-like structure? Here's a sketch of what it could look like:
type Tuple[T: static[varargs]] = concept c
for i in 0 .. T.arity-1:
c[i] is T[i]
There's a few assumptions here which I'll call out:
Thoughts? Is the current design forward-compatible to eventually express such concepts?
Hi @boia01,
It will be possible to create concepts based on type lists, but I don't consider this a feature of the concepts per se, but rather a general support for variadic generics. You can take a look at this github issue:
https://github.com/nim-lang/Nim/issues/1019
As explained in the issue, type lists can be emulated right now with a single parameter, expecting a tuple type. Then within the concept, you can have a static: block containing arbitrary code for the actual checks. I tried to put something together quickly as an example, but I ran into several issues, so this explanation will have to do for now, sorry.
@zahary It becomes more and more obvious that I won't have time to work on Nim nowadays. It is my regular job which put more load on me.
Coming back to Concept[T], I can see 3 possible ways to continue.
1.: allow inference only if its unique. So c.push(T) only works if there is one push function, or we already know what T type is (e.g., we know that it is string).
2.: allow inference to metatypes. So c.push(T) can lead to T being string|int. I recommend an extra check at the end. That is if you have a match (e.g., T is int and S is int), then reevaluate the concept's body again just to be sure. (Just for the record, the reason for this extra check is an example above somewhere in this thread.)
3.: allow some extremely smart logic which infers everything which is possible. This needs to involve some backtrack logic.
@andrea, see this log from gitter
Anatoly Galiulin @vegansk Nov 30 17:03
Hi to all. It was a long road back to Nim I have a question about generic-concepts branch (https://github.com/nim-lang/Nim/tree/generic-concepts). Is it dead? GitHub says "836 commits behind devel".
From IRC (bridge bot) @FromIRC Nov 30 17:04
<Araq> I reviewed it once and it seemed merge-able
<Araq> I know zahary never stops developing nim, so it's not dead either
<Araq> but progress is SLOW ;-)