3
$\begingroup$

I take occurrence typing to be typing that "... allows the type system to ascribe more precise types based on whether a [check] succeeds or fails." (adapted from the Racket docs with "predicate check" replaced with "check")

Here's a TypeScript example:

function foo(x: string | number) {
    switch (typeof x) {
        case "string":
            // the type of x is `string` here:
            x.length
            break
         case "number":
            // the type of x is `number` here:
            x * 3
            break
    }
}

playground link

I take "dependent types" to mean "types that depend on terms". reference reference

The type of x (a type) depends on x (a term). So is there dependent typing in the example above? More generally, is occurrence typing a form of dependent typing?

I could see an argument that the answer is "no" if we interpret "dependency" such that it is expressed via binding. So then a "dependent type" would be a type T x where T is a type and x is a term. But then maybe even on this definition occurrence typing counts as dependent typing, if we allow T to be something fancy like a type-level x -> if x is a string then string else number.

$\endgroup$
1
  • $\begingroup$ I'm not sure what you mean by "the type of x depends on x". Do you mean the type of x depends on the value of x? If so, what makes you think that is true? $\endgroup$
    – D.W.
    Nov 28 '20 at 21:57
1
$\begingroup$

No, I would not consider this a dependent type. The type of x does not depend on the value of x.

I suppose you could say that the type of the expression x depends on the type of the variable x, but that doesn't make this dependent typing.

You link to Wikipedia, but the Wikipedia article on dependent types say "a dependent type is a type whose definition depends on a value" and says " The return type of a dependent function may depend on the value (not just type) of one of its arguments" and "A dependent pair may have a second value of which the type depends on the first value". Here the type of x does not depend on values; only on the types of the variables. Beware that these English sentences describing terms like "dependent types" or "occurrence types" are not to be taken too seriously and you need to look at the precise mathematical formalism if you want to be precise.

I would not consider the feature you describe as dependent typing. Rather, I would consider it an instance of flow-sensitive typing.

$\endgroup$
5
  • $\begingroup$ thanks for your answer. When you say I should look at the "precise mathematical formalism" - would you be able to find such a thing for "dependent type"? $\endgroup$
    – Max Heiber
    Dec 1 '20 at 8:54
  • $\begingroup$ You wrote that in the examples I gave the type of x does not depend on the value of x. It does. typeof is a runtime check. The presence of the runtime check lets TypeScript know (statically) that the static type of x is string in the first branch and number in the second. $\endgroup$
    – Max Heiber
    Dec 1 '20 at 8:57
  • 1
    $\begingroup$ @MaxHeiber, I don't know. Unfortunately I am not an expert on this. typeof(x) is a runtime check but its result depends only on the runtime type of x, not on any other aspect of the value of x -- that is what I meant by my statement. $\endgroup$
    – D.W.
    Dec 1 '20 at 9:02
  • $\begingroup$ Re "Beware that these English sentences ... are not to be taken seriously and you need to look at the precise mathematical formalism if you want to be precise" - this standard isn't met by any of the literature I've seen. The literature gives examples of depedendent types, but what unites this example seems only to be variations of that English sentence. For example cs.nott.ac.uk/~psztxa/publ/ydtm.pdf - two semi-formal definitions are given for ways types can be dependent, but dependent types themselves are only defined in English. $\endgroup$
    – Max Heiber
    Dec 6 '20 at 13:02
  • $\begingroup$ typeof(x) is effectively checking a runtime type tag - which feels like types depending on terms. It's unfortunate in this case that we call "runtime types" and "static types" both "types" - I think it's obscuring what's going on. $\endgroup$
    – Max Heiber
    Dec 6 '20 at 13:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.