> Is that the separation you wanted?
You just tried to achieve separation with inclusion, look at your imports. But
additional boilerplate code does not address the problem:
> # should probably have been `v.b = v.a + 5` in the original code
You got the point and missed it at the same time.
I intentionally wrote : `v.b = v.b + 5`
because it is the wrong translation of the original assignment given in
oopnv(T,int) where T stands for the intrinsic type, being an existential Type.
It should better be written xT for that purpose.
If I now rewrite mdlprog:
proc oopn(obj : TCon , x : int) : TCon =
result = obj
result.b = result.b + x
proc run() =
var v : Tcon = con(5)
v = oopn(v, 5)
oprint(v)
Run
it would look that I can do the same thing in mdlprog as in mdlimpl, it looks
similar, but it isn't.
At the same time, I had redefined the underlying type, because I changed the
operations that can be run over it.
So I gave evidence for:
* A[xT] |= B[T]
That is possible because I could "open" (reify) the underlying nominal type of
the existential Type xT , given in mdlabst, at the top level mdlprog and build
my own function on it. Therefore, I can make a B of a A or an X for an U.
But logically, this is not derivable, neither in classic logic nor intuistic
logic.
What then? Well, let's call it "Nim logic" within recent Nim.
This might change in the future. Or, it is a generational problem.
