5 ms·

> If you have to specify the types everywhere, or don't have compile-time checks, it's not really generics. Specify which types everywhere? If you mean specify

> If you have to specify the types everywhere, or don't have compile-time checks, it's not really generics. Specify which types everywhere? If you mean specifying the concrete types (e.g. `Integer` and `List[Integer]`, then I'd agree. If you mean type variables (e.g. `T` and `List[T]`) then I disagree: that's a perfectly valid way to do generics, and having to annotate stuff is just a deficiency of inference (no worse than, say, Java). The key is that we're allowed to use the argument names and function/method names in our types, thanks to the 2 given rules. We don't need to lift those functions up to the type level, since we're only checking that the inputs and outputs line up. To me, this seems to be a form of dependent types. Note that "dependent types" only refers to the ability of having types refer to values, e.g. dependent function types like `(n : Int) -> Foo n` or dependent pairs like `(n : Int, Bar n)`. Most dependently typed languages also treat types as first-class language constructs, allow the type-checker to run arbitrary code (which usually implies that computations are pure and everything terminates/coterminates). Those latter aspects don't seem to apply here: it's just about using value-level names in our types. I think this works quite nicely, from a theoretical point of view; but I wonder what would happen in more complicated situations. When type checking is purely syntactic, we can easily get stuck with mismatched things like "should have type 'T', got type 'Pair[T, U].first()'". That's where we need type-level computation, to reduce things down to normal forms so that the syntactic checks (are more likely to) work.

Groxx 8y ago
>If you mean specifying the concrete types (e.g. `Integer` and `List[Integer]`, then I'd agree. Yep, that's exactly what I mean (since that's the only example in the article that seems to imply any kind of compile-time safety). re dependent types: interesting! yeah, it does seem like normal generics could be a type-dependent type in a case like this - I hadn't really thought about that before. though that also seems like a "shadow type" tho, which the article is trying to eliminate... so we're back at the starting point :|
- chriswarbo 8y ago
  > 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!

Groxx 8y ago

>If you mean specifying the concrete types (e.g. `Integer` and `List[Integer]`, then I'd agree. Yep, that's exactly what I mean (since that's the only example in the article that seems to imply any kind of compile-time safety). re dependent types: interesting! yeah, it does seem like normal generics could be a type-dependent type in a case like this - I hadn't really thought about that before. though that also seems like a "shadow type" tho, which the article is trying to eliminate... so we're back at the starting point :|

chriswarbo 8y ago
> 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!