4 ms·

> Stuff [...] all combine to give you a certain amount of dependent types in Typescript but also a very rich way of doing type level computations [...]. I thin

> Stuff [...] all combine to give you a certain amount of dependent types in Typescript but also a very rich way of doing type level computations [...]. I think this is a wrong use of the term "dependent types". For example, you can't write this in TypeScript (yet): function concat<alen: number, blen: number>( a: ArrayOfLength<alen>, b: ArrayOfLength<blen>, ): ArrayOfLength<alen + blen> { return [...a, ...b]; } Sure, you can have a type-level object that corresponds to the numbers and use the type-level expression to compute the equivalent of alen + blen, but they are not dependent types. You have just shifted values to the type level. The type-level expression is awesome---but not because they are dependent types. TypeScript is also not a typical type system you can compare with others. Most famously it is intentionally unsound [1], meaning that it can mostly but not entirely prevent a certain class of runtime errors, because it can't guarantee the behavior of external JS code anyway. Most static type systems are or at least try to be sound because that's what users expect them to be: preventing a wrong code beforehand. Dependent type systems are complex because they also want to be sound. TypeScript has an entirely different goal for a reason and you can't compare it with other type systems not sharing that goal. [1] https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness https://www.typescriptlang.org/docs/handbook/type-compatibil...

Garlef 6y ago
Actually, this is mostly possible. Except for some issues regarding the stack size when resolving the types. (But I think there are more efficient implementations using more copy and paste, making this actually work) playground link: https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAOyhAHsCyAmBnKZAVwFsAjCOAGigBUBeAQ2RBoH024IBjNTbfFGYgA2gF164gHxR6AKCiLCpCnD5ZcBZAqW6A-EJbiduxQC4TUDl24iARABtsAc2AALO2PUCtl-Vc4ePyUzWAQUGloaEQA6OOseGmExKTk00EgrbgB7ZG5GYEQYb01DUTEaACESwWFpWUtickoaghh7J2RXDzFgxQM63tMQxpUWjA1BSo6Xd08+qAGjIeGoC11qiZ8oEQBLZAAzFsqABho4mP2jtQAlFeGDNhy8gsRYuJgqk4qoG9TVtaWGBpOQZaBsRg4HAoVrKZrUKAkWFNVQyeS6AD0GKgAAFgHgALS7ZzIbJcKAEglQACi6G4EDweF2ADdoHhgIxuABrKA4CBgdyWLFQAAUAEkoO59jz3JRoLsCIxEWToBADgddtxdthgFBdiQwE4SDqCrtclAyERdRKDmTnNldbtgDEAJSWJ65fKFeBIZBSGg+xAkKRSGZdOa9dLgaBYdmyLKe14iACMNAATD8U+mUqDo5KGcA0-GPS9ClmoBnoqmKykw915lHMsgTvHAydUmDCMnW+Fkx288gi-Qwkg06lc5kNazi5DoQBmdPjuTPOPPL3xxBRQjIsYIpFbUooyhSEWWRgIZOhQPISL+s8INNX8IkW9UIXYgCyCttcGARGQBQQA4rCSm4CpQAcjC7A4BA4EQMbZFA7KcjyTIAF4QDElguk+SAQlCESIv6dBov8qzCnihLEqSXALO8MTnnA1YXIxGYgiuuroOg8ZrgUIrlpWOwLlAAAsNAAKxiC6QA https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAO...
- 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...
dwohnitmok 6y ago
> I think this is a wrong use of the term "dependent types". The operative term here is "a certain amount." `typeof` in Typescript is definitely a dependent type operator (it takes a runtime value and extracts its type which can then be used as a type signature for other types). You don't have full-spectrum dependent types a la Idris, but you do have some amount of dependent typing. See for example type MyResult<T extends boolean> = T extends true ? { tag: 'a' } : { tag: 'b' } function outputTypeDependsOnInputValue( value: boolean ): MyResult<typeof value> { if (value) { // replacing 'a' with 'b' is a type error const result: MyResult<typeof value> = { tag: 'a' }; return result; } else { // replacing 'b' with 'a' is a type error const result: MyResult<typeof value> = { tag: 'b' }; return result; } } Now there's a good deal of limitations and hackiness here in how you call this function (in particular you need some weird overloadedness to preserve the types at call sites), but it is really some measure of dependent types! I'll include a full example at the end of this post. > Dependent type systems are complex because they also want to be sound. Dependent Haskell, if it lands, will not be sound (TypeInType). Idris 2.0 currently also is explicitly not sound. In the case of Idris that's mostly a matter of prioritization, but it's enough to demonstrate that soundness is, perhaps surprisingly, not a huge priority for even all full-spectrum dependently typed languages. Full TS example: type MyResult<T extends boolean> = T extends true ? { tag: 'a' } : { tag: 'b' } function outputTypeDependsOnInputValue<T extends boolean>( value: boolean ): MyResult<T> function outputTypeDependsOnInputValue( value: boolean ): MyResult<typeof value> { if (value) { const result: MyResult<typeof value> = { tag: 'a' }; return result; } else { const result: MyResult<typeof value> = { tag: 'b' }; return result; } } function worksWithA(a: 'a'): void {} function worksWithB(b: 'b'): void {} function useOurFunction(value: boolean): void { if (value) { const result = outputTypeDependsOnInputValue<typeof value>(value); worksWithA(result.tag); // worksWithB(result.tag) is a type error } else { const result = outputTypeDependsOnInputValue<typeof value>(value); worksWithB(result.tag); // worksWithA(result.tag) is a type error } }
- lifthrasiir 6y ago

Garlef 6y ago

Actually, this is mostly possible. Except for some issues regarding the stack size when resolving the types. (But I think there are more efficient implementations using more copy and paste, making this actually work) playground link: https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAOyhAHsCyAmBnKZAVwFsAjCOAGigBUBeAQ2RBoH024IBjNTbfFGYgA2gF164gHxR6AKCiLCpCnD5ZcBZAqW6A-EJbiduxQC4TUDl24iARABtsAc2AALO2PUCtl-Vc4ePyUzWAQUGloaEQA6OOseGmExKTk00EgrbgB7ZG5GYEQYb01DUTEaACESwWFpWUtickoaghh7J2RXDzFgxQM63tMQxpUWjA1BSo6Xd08+qAGjIeGoC11qiZ8oEQBLZAAzFsqABho4mP2jtQAlFeGDNhy8gsRYuJgqk4qoG9TVtaWGBpOQZaBsRg4HAoVrKZrUKAkWFNVQyeS6AD0GKgAAFgHgALS7ZzIbJcKAEglQACi6G4EDweF2ADdoHhgIxuABrKA4CBgdyWLFQAAUAEkoO59jz3JRoLsCIxEWToBADgddtxdthgFBdiQwE4SDqCrtclAyERdRKDmTnNldbtgDEAJSWJ65fKFeBIZBSGg+xAkKRSGZdOa9dLgaBYdmyLKe14iACMNAATD8U+mUqDo5KGcA0-GPS9ClmoBnoqmKykw915lHMsgTvHAydUmDCMnW+Fkx288gi-Qwkg06lc5kNazi5DoQBmdPjuTPOPPL3xxBRQjIsYIpFbUooyhSEWWRgIZOhQPISL+s8INNX8IkW9UIXYgCyCttcGARGQBQQA4rCSm4CpQAcjC7A4BA4EQMbZFA7KcjyTIAF4QDElguk+SAQlCESIv6dBov8qzCnihLEqSXALO8MTnnA1YXIxGYgiuuroOg8ZrgUIrlpWOwLlAAAsNAAKxiC6QA https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAO...

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

dwohnitmok 6y ago

> I think this is a wrong use of the term "dependent types". The operative term here is "a certain amount." `typeof` in Typescript is definitely a dependent type operator (it takes a runtime value and extracts its type which can then be used as a type signature for other types). You don't have full-spectrum dependent types a la Idris, but you do have some amount of dependent typing. See for example type MyResult<T extends boolean> = T extends true ? { tag: 'a' } : { tag: 'b' } function outputTypeDependsOnInputValue( value: boolean ): MyResult<typeof value> { if (value) { // replacing 'a' with 'b' is a type error const result: MyResult<typeof value> = { tag: 'a' }; return result; } else { // replacing 'b' with 'a' is a type error const result: MyResult<typeof value> = { tag: 'b' }; return result; } } Now there's a good deal of limitations and hackiness here in how you call this function (in particular you need some weird overloadedness to preserve the types at call sites), but it is really some measure of dependent types! I'll include a full example at the end of this post. > Dependent type systems are complex because they also want to be sound. Dependent Haskell, if it lands, will not be sound (TypeInType). Idris 2.0 currently also is explicitly not sound. In the case of Idris that's mostly a matter of prioritization, but it's enough to demonstrate that soundness is, perhaps surprisingly, not a huge priority for even all full-spectrum dependently typed languages. Full TS example: type MyResult<T extends boolean> = T extends true ? { tag: 'a' } : { tag: 'b' } function outputTypeDependsOnInputValue<T extends boolean>( value: boolean ): MyResult<T> function outputTypeDependsOnInputValue( value: boolean ): MyResult<typeof value> { if (value) { const result: MyResult<typeof value> = { tag: 'a' }; return result; } else { const result: MyResult<typeof value> = { tag: 'b' }; return result; } } function worksWithA(a: 'a'): void {} function worksWithB(b: 'b'): void {} function useOurFunction(value: boolean): void { if (value) { const result = outputTypeDependsOnInputValue<typeof value>(value); worksWithA(result.tag); // worksWithB(result.tag) is a type error } else { const result = outputTypeDependsOnInputValue<typeof value>(value); worksWithB(result.tag); // worksWithA(result.tag) is a type error } }

lifthrasiir 6y ago