3 ms·

Actually, this is mostly possible. Except for some issues regarding the stack size when resolving the types. (But I think there are more efficient implementati

• lifthrasiir 6y ago
  No, you are creating a literal type which is not same to the corresponding literal. This is evident when you try to use alen and blen (respectively named n and m in your code) in the function code: they are strictly type-level constructs. Also, probably I should have written my example as follows: function concat( alen: number, blen: number, a: ArrayOfLength<alen>, b: ArrayOfLength<blen>, ): ArrayOfLength<alen + blen> { return [...a, ...b]; } My original code did distinguish two sets of arguments because that's the TypeScript syntax closest to currying (and I was lazy to check its implication), but the point of dependent typing is that alen and blen are not necessarily known to the compiler. The compiler may have to deal with the following code then: let abc = concat(a, concat(b, c)); abc = concat(concat(a, b), c); ...where the first type `ArrayOfLength<alen + (blen + clen)>` should equal to the second type `ArrayOfLength<(alen + blen) + clen>` for the assignment to be valid. Since the compiler doesn't know alen, blen or clen, this means the compiler needs to somehow understand the associativity! This is hard, considering that (a+b)+c is not even generally same to a+(b+c) thanks to floating point. For this reason many dependently typed languages also act as proof assistants or verifiers. If this point is removed, so-called "const generics" will be classified as dependently typed.
  • Garlef 6y ago
    Well... would this satisfy you? (I removed the _add part for convenience. You could still argue that `_concat` is not a literal... if by literal you mean a primitive provided by the language itself. Note that i'm not claiming that this is a dependent type system. But you can emulate some features of such a type system.) https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAOyhAHsCyAmBnKZAVwFsAjCOAGigH1a4IBjNTbfKAQ2RAG0BdALwCAfFEEAoKNMKkKcVllwFkUmeoD8XHgLXrpALj10GzXgCIANtgDmwABbn+i9iuOaTjJu5kHYCFBpeADpQ+i8abhB+EQk40Eg6JgB7ZCZOYEQYF2VtPn4aACEcjijRcWNickoSghgLa2Q7R34faS0y1v1fSrkajCUOQobbByc2qA6dLu6oI3VigdcoXgBLZAAzGsKABhpQ4PWthQAlGe6tWhS0jMQQ0JginYKoE9jZueMYOI2iNOBVqkoNd0pkYI1arJqtQoIUIUtclV5CIABTGTiNPzg7BUYxkTGwxq49ScLEBbHIETEmRkMlIOHYKkSACUfiuqVBWXJjSp-npPLEAG9jAB6EVQAACwDwAFpVjZkMlGMZGMAiHBUPdgpx9qEyPwANwSAC+cTFUAA7kqANZ4CTXPDAKDodAAJnEwI5GRRrpoAGYggBGGiul68ANQAAsNAArPxmWbxQloJQ4EqoDgiNBgMkoI1mlASKs8CQMkx7PbUo7nW7aBsPSDvRG9itg1BQ0EI9GoHGE4muHg8MkmKsMqsAG6rUBQZL1xtOmVQMjJBxQRhDyzj7O53ht31QP2tZNQAAyHvZN0yF85u7Dod54ZiEmPJ3P87ugZe19uvA7K0PIixJWyDVlg1aCJ6l4om2ba3kEoZ9uax7FisUSRDw6HRMB1acIOQ5MAAKhAjpnhB87QSG1LSHBxjkTBVH6L+BQTI+DEJohSbgNAKG8GheSYa0DpOrhg7DkR4GQaCPo0MGtFesAFFQLJHw0SpHbGMyDGsSycQSOaTDqnAqwQDg2FOgZCAgAAwhkHpZPCbCIn0MIMqgCIcEilCouiBIUgx+LYH4rkaeIYhZAQ7l1NyjJFBFjkcPA-KMt5HykrAeAMeotKwhlEyskk8nhbFYiCO8HwyOaUqyvKirKuVMhajqUAHPqulCcCgbumRhnWd6e4JkhXFQDxe7+oJVZOugTCdQ2nUoruA5KXei37n6i2Hgm7VTZ1daza682Botn7wSt-rrTQ5g5rQpY8LQU4QCQeBOMyQA https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAO...
    • lifthrasiir 6y ago
      Uh, no? _concat is a type-level function and you can't generalize it to receive runtime arguments in any way. I do acknowledge the value of type-level evaluation, but there is a very deep gap between type-level evaluation and dependent typing.