DEV Community

Discussion on: Dynamic value type inference?

deciduously profile image
Ben Lovy

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.

kosich profile image
Kostia Palchyk Author • Edited on

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?

deciduously profile image
Ben Lovy • Edited on

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!