[zasdffaa]

Thanks! I guess what you are describing looks - from my very limited experience with scala - as a path-dependent type. If I'm right.

I'm actually talking about C# because I'm working in it and I'd like to make some compile-time guarantees if possible. Or at least know how to assure a method that they are getting a list with at least 2 values in it, for example. It may not be worth the effort but it would be nice to know how.

I've got books on DT, idris, and another DT lang, trouble is there's no call for any of this stuff in industry so they get repeatedly pushed to the bottom of the priority stack. Sickening, innit.

[uryga]

i haven't used scala, but from the looks of it, yeah, "path-dependent types" are a narrow subset of full dependent types, intended for stuff like this exact use case :D

there's things you can do to track list length at the type level, but it usually involves putting your data in a special-purpose linked-list thingy: https://docs.idris-lang.org/en/latest/tutorial/typesfuns.htm...

(the `S` and `Z` refer to peano-style natural numbers)

although if you go that way, you can actually get a lot of that without dependent types! here's an example i found of someone doing a similar construction in C#: http://www.javawenti.com/?post=631496

last but not least, in TS you can use the builtin support for arrays as tuples and just do:

  type AtLeastTwo<T> = [_1: T, _2: T, ...rest: T[]]

which looks very nice, but it's pretty much only doable because the type system has specific support for array stuff like this, so not a really general solution.

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