[zasdffaa]

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!

[uryga]

good luck! it's quite fun :)

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:

  class Foo<T> {
    private Foo(...)
    static Foo<int> Bar() { ... }
    static Foo<string> Zap() { ... }
  }

(or sth like that, i don't really do C#!)

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).