3 ms·
> 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 ty
by 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 agoThere are numerous other well-known terms other than "dependent typing" that describe those features better, namely flow(-sensitive) typing. I believe the implementation of those type systems is considerably different from one of dependent type systems. I do have heard calling const generics as a "dependent fragment", which is fitting given that it might be the largest feasible fragment of dependent types without actually implementing the full-featured type system. I however object to any mention of dependent typing to describe something less capable than const generics since it's pretty misleading IMO. You are absolutely correct that soundness is not the highest priority for dependently typed languages, as it had been true for other languages as well. Still I think most languages with a complex type system (subjective) do try to minimize the number of unsound corners as circumstances permit. I'm not an Idris user by myself but for example, the recent Idris 2 0.3.0 announcement [1] clearly considers unsoundness as something undesirable. As a result I have a general expectation for the type safety of those languages; I don't have that for TypeScript however (and I don't view that as a problem, just a difference). [1] https://www.idris-lang.org/idris-2-version-030-released.html https://www.idris-lang.org/idris-2-version-030-released.html "Removed multiplicity subtyping, as this is unsound and unfortunately causes more problems than it solves."
- dwohnitmok 6y agoI mean we're talking about definitions here so ultimately there isn't a definitive answer, but I think your definition of dependent types excludes a lot of things that are commonly referred to as "some dependent typing" or "lightweight dependent types" (this includes things like GADTs and singletons, Liquid Haskell, etc.). It's important to note that what is going on in that TS example isn't just flow typing (otherwise something like Kotlin would count as a dependently typed language). The `typeof` operator is playing a crucial role here. That's what makes this really a case of a type depending on a runtime value. If it was really just flow typing, then you could still replicate it in something like Scala by just introducing additional layers of types and folding over them (this is also why I would agree flow typing by itself is not dependent types). But that's insufficient to replicate the full TS example. Idris doesn't want to make its soundness situation any worse than it already it is because the community does eventually want it to be completely sound. But like I said, that's not at the top of its priority list. EDIT: Removed "Flow-sensitive typing isn't really all that different from dependent pattern matching (the main difference is on the other side of the coin, where you need some way of generating those dependent patterns and of cascading the flow "down" so to speak, so indeed by itself flow-sensitive typing isn't dependent typing). " as the first line because it didn't seem all that relevant in retrospect.