UPD: Ben Lovy (@deciduously) has linked to dependent types, which seems to be what I'm clumsy describing here. See his comment under the post for more details! Thank you, Ben!
Here, I'm asking for guidance and advice on further reading regarding a subject I'm going to describe next:
Consider this example in typescript:
if (false) {
log('Unreachable code');
}
The log part will never be executed, no matter what. And a modern type system has ways to detect that dead code and will probably raise an error at the build time.
Now let's see this snippet:
const answer = 42;
if (answer - 42 > 0) {
log('Unreachable code');
}
The log part is still unreachable, yet we won't see any error or warning.
The compiler will eat that, since the validation is static, and the minus operation done on 42 and 42 is statically defined to return a type Number.
And not 0, that it truly does.
I'll skip > comparison fn for brevity.
One more case
Imagine we have a function head, that accepts an array of items, and return the first element:
const head = arr => arr[0]
So the type of the function is detected as:
head :: any[] -> any
While in reality, it's more like:
head :: Array of length 0 as a =>
a -> undefined
head :: Array of 1+ length as a
, First element of a as b
=> a -> b
Forgive me this free-form type notation
So the type validation would forbid me accidentally doing:
const a = head([true, 1, 'hi']);
return a / 8; // <-- Error, dividing a Boolean
To the point
Are there type systems with "dynamic type analysis" / "dynamic subset inference" that would handle such cases and properly report the type of answer - 42 to be 0?
Since I work in webdev, I'm primarily looking for implementations in this field. Yet, as well I would be glad to read more general information/achievements in other fields.
How I imagine that
For such systems to exist, I guess, they should run all the code that doesn't create side-effects and build a graph of sets of possible values subtypes.
Well, a function that divides one integer by another, has an infinity of possible values, so the calculation should be lazy somehow. Also, the system should handle loops/recursions that never stabilize.
As to side-effect-full functions where we can't infer subtypes, developers could manually define their types (as we already do now with foreign code):
Say, for an HTTP request function
function getACoinNominal(url) {
return http(url).then(
// ...
);
}
we could declare:
getACoinNominal
:: Subset of String that starts with `/`, `//` or `https://` as URL
, Subset of number of [1, 2, 5, 10, 25, 50] value as Nominal
=> URL -> Promise<Nominal>
So that we can use getACoinNominal function only with strings that start with / // or https://, and it will return us a Promise with 1, 2, 5, 10, 25, or 50. Nothing other.
And in the cases when the exact value subset can't be calculated properly, or it takes more than a reasonable time to do so, we can always fall-back to the basic type inference.
Conclusion
I think such active analysis in the build phase will be useful not only for dead code detection but even more so for:
- smarter errors reporting
- better type guidance
- code reduce by letting us handle exact cases we should cover
As you may have found already, I don't know type systems theory (nor much of other theories, to be honest) . So, I'm asking to share some of your wisdom on:
- if such systems exist (I suspect they exist for a long time, at least in runtime engines)
- what can I read to learn more on the subject
- if it cannot exist
- share your thoughts if we need such a system
Thanks!
Appendix with use case speculations
if (code >= 400) {
return;
}
// ... some lines of code / function calls here...
if (value == 502) { // <- Error: [ 502 ] is not a subset of [ -Infinity..400 ]
// ...
// name :: \w* => name -> void
function capitalize(name){
// ... fn logic
}
// ... some lines of code / function calls here...
const value = ' Henry ';
capitalize(value); // <- Error: [' Henry '] is not a subset of ['\w*']
Original tweet:
Top comments (3)
I'm not completely positive I've correctly parsed your question, but it sounds to me like you're describing dependent types. Is that more or less correct? I don't know of any webdev technologies that can do this, it's a pretty niche feature confined to fancy academic languages like Idris, F*, and ATS. All very cool, but not exactly what you'd use for practical work today.
Hi, Ben!
From what I understand, it looks like what I was searching for!
And it surely supplies me with reading materials for months (well, years rather) 🙂
Thank you very much! 🎄
P.S.: Will it be useful to have it in our day-to-day development? What do you think?
Awesome! My only experience with it is from messing around with Idris, here's the relevant section in the docs - the "holes" described in the section preceding are another really cool idea. Idris is just pretty cool in general, and worth your time even if you never deploy any code
I do think it's a useful idea, but the Wiki article notes it does complicate type checking. It can slow the process, and lead to more complicated situations, including those which may be undecidable - potentially a step backwards in terms of practical benefit if you hit that case.
In general, though, I agree with you, I think moving that check to the type level is a good idea. If I append to an array, it actually, conceptually, is part of the "type" of the return value that the length of my array is greater than the original length (by exactly one). Seems useful to be able to specify that in the definition, much like it's useful to define any types at all.
I'd be curious to see if you come up with anything cool with this feature, or work out a way to approximate it with TS!