Thanks, yeah, did a big search for DT stuff this morning and found this one. The S/Z is the zero/successor. I need to study it. Perhaps closer to what I originally saw was this https://gist.github.com/bradphelan/26c0e84197092620359a (edit: it's not closer. Still worth a peruse though)
I need to sit and read and butt heads with these if I can find the time.
It's so odd there are so few examples of C# DT. The one good one I found a year ago seems to have disappeared. Maybe a conspiracy?
Looking forward to Idrisizing or Agdicating some time!
another term that might be useful is "GADT" - it's kinda like a weaker form of DT, more easily expressible in, uh, normal languages. the C# one i linked is really more like a GADT, bc it all stays at the type level w/o bringing "normal" values into it. another way to do it would be a sealed class with a private constructor + static methods:
so that way you can have the type param and use it to track something, but limit what can be put there - in this case, only int or string. type-safe syntax trees are a common case for sth like this (though in that case you'd probably go for an abstract base + subclasses, like in the link).
I need to sit and read and butt heads with these if I can find the time.
It's so odd there are so few examples of C# DT. The one good one I found a year ago seems to have disappeared. Maybe a conspiracy?
Looking forward to Idrisizing or Agdicating some time!