RFC: Weak Distincts

[beef331]

Generic aliases are practically useless, the idea here is to make them a weak distinct.
Take the following example:

type
  A[T] = int
proc doOtherStuff(a: int) = discard
proc doStuff(a: A[int]) = discard
var 
  a: A[string] = 100
  b: A[int] = 200
doStuff(a) # errors `doStuff` expects `A[int]` but got `A[string]`
doStuff(b) # compiles fine calling `doStuff`

doOtherStuff(a) # weak distinct -> int is implicit
doOtherStuff(b)

a = A[int](b) # Requires conversion to weak distinct from distinct
a = int(b) # Though converting to the base first impliclty convetes

The rules of this are as follows:

• Weak distincts are what are presently what are generic aliases type A[T] = SomeType
• Weak distinct -> weak distinct requires explict conversion, though base -> weak distinct is implicit, as is weak distinct -> base
• When dispatching the weak distinct is preferred to the base (overriding is possible)
• If the base is an object any fields that are accessible on the object in this scope are accessible on the weak distinct

[saem]

Thanks for writing this up.

I'm putting my thinking cap on and seeing if this is sufficiently sound. I think a big issue is how sloppy the language is in discriminating between a new type vs an alias. Though perhaps that's ok in a structurally (distinguished by structure) typed language which Nim really isn't and it's more nominal (distinguished by name).

My understanding is as follows, structural equivalence can represent nominal equivalence by saying that the type (not memory, but the thing in the type expression language) has the name a part of the type itself. This means two otherwise equivalent structures with differing names will not match. So the type int = int would translate to singing like { name: "int", memory: { int } }, hopefully that makes sense. A generic would get a name based on some mangling or whatever I guess.

So the above approach is a hybrid of nominal and structural and I'm concerned that's not sound or were not thinking of edge cases. Imma as my type system friend for advice.

[saem]

Discussed with @j14159, they pointed out that this will result in an error:

type A[T] = int

proc identity(i: int): int = i

var a: A[int] = 200

a = identity(a)

The issue being that we lose type information. It's not the worst, but didn't feel great either.

[beef331]

In what way would it error? Regardless implict rule could be dropped to Weak -> Base and not the other way around, but I do not really see the issue with the loss in the above, you know A[int] is internally an int and anything on the right of = it has to be either int or A[int]. So a proc that returns a weak distinct needs to be converted, but a proc that returns the base is no issue as far as I can see.

[saem]

Because a base should not convert to a weak distinct, as the weak might be used to convey information, such as a nim node that is known to be a procdef, we could make a weak version, but we don't want to allow arbitrary nimnode assignment to such a weak.

I think the bigger thing here is that a weak going into a base's proc, like identity above, means we really can't guarantee anything, as in the conditions that made it a weak might not be true any longer. Only time that is likely to hold is with perhaps a strict func. 🤔

[j14159]

@saem somewhat successfully nerd-sniped me here. Please forgive any abuse of Nim syntax on my part, I'm new to it. It's also very likely I'm at least subtly wrong (or out of my depth) in some of what follows.

There are two potential issues I can see related to information loss, and I'll frame it in terms of subtyping. For clarity, when I say "subtyping" I mean nothing more than:

• I'm defining a relationship between pairs of types, e.g. A[int] and int.
• Any specific order of pairing works in one direction, e.g. A[int] is a subtype of int does not imply the opposite.
• I'll use the shorthand A[int] <: int to mean "A[int] is a subtype of int", which means nothing more than "we can use A[int] anywhere int is required."

The potential issues are:

1. Transparent and maybe undesirable conversion between different "weak distincts".
2. Losing type information that impacts dispatch, possibly in undesirable ways.

Your second rule states:

Weak distinct -> weak distinct requires explicit conversion, though base -> weak distinct is implicit, as is weak distinct -> base

If we frame this in terms of subtyping, we might say that given:

type
  A[T] = int

Then we can say that A[int] <: int, meaning "A[int] is a subtype of int". Rewriting your rule then gives us:

A[int] <: int
int <: A[int]

So I can use A[int] anywhere a type signature says int should be used, and vice-versa.

Now if subtyping is transitive, we could say:

A[int] <: int <: A[int]

If @saem's example is correct, meaning that we do get an error from a = identity(a), then subtyping is not transitive. Only my first rewrite applies, but the rules perhaps should make that explicit.

If @saem's example does not give an error, then subtyping is transitive and we run into larger problems. For example, given:

type
  A[T] = int
  A[string] = int
  A[int] = int

So we have A[int] <: int, A[string] <: int, and the reverse of both. What then prevents A[int] <: int <: A[string]?

The typer might then have to accept the following:

proc f(x : A[int]): int = ...
proc g(x : int): int = ...
proc h(x : A[string]): int = ...
var a: A[int] = ...
h(g(f(a)))

If this is true (meaning subtyping is transitive), then probably the first part of rule 2 is broken:

Weak distinct -> weak distinct requires explicit conversion ...

Because there was no explicit cast. Perhaps I'm being pedantic, but I think that given your rules, you are intending to say "A[int] <: A[string] cannot and should not be allowed unless done through an explicit cast."

I think @saem's saying subtyping is not transitive, and @beef331 is saying it is. You could probably block this by adding a side condition that allows transitive-but-not-different, e.g.

A[T] <: int <: A[U], iff T = U

But I think in that case you may be dealing with a bit of a memory explosion in the typer because you'll likely end up tracking much longer chains than the above (my framing is profoundly naive/over-simplified, and possibly has bugs).

The dispatch problem is basic information loss and related to subtyping, again please forgive my abuse of Nim syntax. Given:

type
  A[T] = int
  A[int] = int
# er...does overloading work this way?
proc f(i: int) = ...
proc f(a: A[int]) = ...
# ...
proc h(i: int) = i.f()
# ...
h(5) # Which `f` dispatches inside `h`?
var a: A[int] = 12
h(a) # Same or different to the dispatch above?

This is solvable, but requires more machinery, and as previously may lead to a lot more memory use. I'll also repeat my opener that it's also very likely I'm at least subtly wrong (or out of my depth).

[beef331]

Ah, I believe I see the concern. Given the overload example it would call f(i: int) , in dispatching the preference would be to stay to your current type, so the only time you'd dispatch an int as an A[int] is when there is no other overload, and vice versa for the base. If you want to dispatch based off the weak distinct you have to use the weak distinct in the procedure otherwise it's the base.
Given:

type
  A[T] = int
proc f(a: A[int]) = discard
f(100) # No match as an int so check all overloads and see if there is only one weak distinct. Finds the `f(a: A[int])` and call it
proc f(a: A[string]) = discard
f(100) # No match as an int so checks overloads and finds there are 2 weak distincts, so cannot call either.
proc f(i: int) = discard
f(100) # Gets match as int so dispatches on that

Though I guess there's also the issue of implict conversion on assignment, so maybe implict conversion is just bad for this all together.

[juancarlospaco]

I think that distinct has very little real world usage in Nim ecosystem in general,
see TaintedString, so I dont know if it worth the effort in the long run... 🤔

[saem]

First thing is first, this isn't Nim, please see the readme in terms of direction and refrain from bringing it into the discussion.

We use distinct plenty and are running into short comings of implementation. Broadly speaking as far as type systems and languages design goes they're a well explored and sound.

[juancarlospaco]

I am referring to the same thing.

[juancarlospaco]

" Nimskull-flavored Nim " ?, I think we all understand that we are talking about anyways...

[beef331]

Distincts are very desirable, they're much better than the struct NotString{ string data} simply cause they maintain the type information of where they're from. The main issue with TaintedString is that it was a distinct that noobs could run into and as such got confused by the difference. For a more sensible usage: https://github.com/beef331/truss3d/blob/master/src/truss3D/shaders.nim#L5-L10
The point of a type system is to give your data meaning and distincts are atleast one mechanism that accomplish this, they allow you to do "Hey this is an 'int', but I'll define how it can dance". For instance what I do with the GPIO pins in the picostdlib. You also can use distincts as an alternative to passing flags like I do for Nimscripter, i use NimscriptFile to pass a raw string and NimscriptPath to pass a path to file, allowing me not to have to pass isFile or have a loadFromFile. They have plenty of use and dismissing usage of them due to TaintedString is a diservice to the type system in my book.

[juancarlospaco]

Ok, given that explanation I understand and I agree with it.

[alaviss]

Here is a crazy idea that I came up with: How about we get rid of type aliases altogether and replace them with weak distincts?

And a small amendment to the weak distinct rule:

• weak distinct can be implicitly converted to base
• base cannot be implicitly converted to weak distinct

  • Here is a bit of a special sauce however:

    Treat all functions like they were borrowed from a prototype where the base type is fully converted to the weak distinct, for example:

    type X = int
    proc foo(x: int): int = x
    
    foo(X(10)) is X

    Of course, in case of an unrelated generic parameter (in this case, the seq is seq[int]), don't convert:

    type X = int
    var s = @[1, 2, 3]
    
    s[X(1)] is int

    So I guess the rule is: if a function take a parameter of base type of which is not the result of generics binding, and if the return type is also the base type and not a result of generics binding, promote it to the weak distinct.