Reflection / rules depending on type constructors

[nmushegian]

Thoughts on this? Allow pattern matching like this when used in a special 'reflect' term? I still don't understand the runtime enough to know if this info is always there for constant access or if it gets erased somehow. Maybe the purpose of the reflect op would be to capture and not erase this type tag, but I'm just freestyling.

(Reflect (x y)) = (Tag x)

want:   (Reflect (Pink (Val))  ->  (Tag (Pink))

[nmushegian]

So this original thing fails to compile,

Invalid left-hand side
On rule: `(Reflect (x y)) = (Tag x)`.

This lets me compile run the program (it does not complain about invalid pattern), but does not match.

(a (Reflect (x y))) = (Tag x)

(Main) = (1 (Reflect (Pink (Val))))

I do not understand this at all

[bsless]

IIRC you can't take constructors' value, the rule matches an application, I think, not a constructor

[nmushegian]

I understand that you can't, but what I am asking is whether maybe you can, like theoretically could a reflection feature be built in like this in the current HVM paradigm, or would it be equivalent to designing reflection in a higher level language that compiles down

[VictorTaelin]

That wouldn't be possible on HVM's paradigm :( on the interaction net view, that would imply you're pattern-matching on an application node, which isn't (and can't be) possible to do efficiently, sadly.