Lambda the Ultimate

https://github.com/JuliaLang/julia/issues/6113

sorry if this has already been posted; i don't read here much and ltu was mentioned in the link above (but i can't find anything).

i want to ask some questions about my limited, practical, non-theoretical understanding of dependent types:

it seems to me that in julia i can define a datatype (something like a struct in c), that has an associated parametric type that contains information about the data. so, for example, i could put the length of an array in there. and then, as long as any code that constructs or modifies an instance of that datatype follows the contract implicit in the associated parametric type, the code will work correctly and i can dispatch on array length.

now, it seems to me that this differs from how i expected dependent types to work, in that there is no inspection of the actual data value on dispatch. when i dispatch on the array length i am using information in the parametric type associated with my datatype that i trust is correct. but there is, at the moment of dispatch on that type, no inspection. length(array) is not called.

so the correctness of my code depends on the correctness of functions that construct and modify the datatype, rather than on functions that inspect it.

so my questions are:

1 - do other dependent type systems inspect the data?

2 - is this just an implementation detail, or is it connected with what was argued about in the link?

3 - please can someone explain the link like i am five? if the above is not connected with the argument, then i don't get it... in particular, julia often (usually?) compiles code specific to particular types. it doesn't do type unification (HM), afaik, but it does propagate types from annotations, and all concrete types are final (leaf), so the compiled code is "static" in some sense.

thanks,
andrew

[edit: i don't know in detail how julia works, but my impression is that although it's called a "jit" it's basically a static compiler that is triggered only when dispatch on a new combination of function and types is encountered. wherever possible it extrapolates type information to compile static code with fixed types. this is why it is fast.]