> that's the only example in the article that seems to imply any kind of compile-time safety The type-checked example is this: var lst : List[Integer] :=

> that's the only example in the article that seems to imply any kind of compile-time safety The type-checked example is this: var lst : List[Integer] := List(Integer).new(); var i : Integer := lst.add(3) + 4; To me, this isn't so different from something like Java: List<Integer> lst = new List(); Integer i = lst.add(3) + 4; The major difference is the extra argument in `List(Integer)` (compared to `List()`). That's kind of unfortunate, but note that it's a value, not an annotation. It's still generic, since we could just as easily pass in some variable (e.g. `T2`) that we've received as an argument, or pulled out of some other method, etc. This extra argument (a run-time representation of the type) is actually to be expected. Values (including functions) which are generic (in the Java sense), also called "parametrically polymorphic", or as you say "type-dependent types", can be understood as taking those parameters as extra arguments (which is precisely what this article is talking about); although the value itself cannot change its behaviour depending on that argument. For example, `List<T> reverse(List<T> input)` cannot work different for, say, `List<Boolean>` compared to `List<Integer>`. This is really clear in Haskell. The Glasgow Haskell Compiler uses an intermediate language called "GHC Core", where generic values are literally represented in the same way as functions. There's a nice overview at https://alpmestan.com/posts/2013-06-27-ghc-core-by-example-episode-1.html https://alpmestan.com/posts/2013-06-27-ghc-core-by-example-e... (the "id'" example is the first generic one). > it does seem like normal generics could be a type-dependent type in a case like this Generics are definitely type-dependent types. However, when I said "dependent types" I was referring specifically to value-dependent types, e.g. https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type Note in that Wikipedia article's introduction "dependent types are used to encode logic's quantifiers like 'for all'". Compare that to the generic example in that GHC Core link above, where the keyword "forall" gets inserted by the compiler ;) The Wikipedia article also states "Deciding the equality of dependent types in a program may require computations". That's what I was getting at with the system described in this article: it doesn't seem to allow for type-level computations, without which we may end up getting errors that "expected type X, given type Y" when those types are 'obviously' the same (to us, but not the the checker, since it's not able to compute). I know Bracha is a fan of 'pluggable type systems', where we can use a variety of type systems to check things about the same program (perhaps requiring different annotations). However, I'm not sure if these 2 rules are enough to perform meaningful reductions on types (e.g. to spot that `Pair(T1, T2).secondType()` is equal to `T2`). I'd imagine we'd have to "lift" more and more expressions into the type level (e.g. `return`, then `if/then/else`, and so on) until we have a full-blown theorem prover like Agda!