Hacker News Reader

Comment by amitport | Hacker News Reader

"a dependent function may depend on the value (not just type) of one of its arguments" from wikipedia https://en.wikipedia.org/wiki/Dependent_type

The value does not exist during compilation. AFAIKT dependent type are used mostly during executable proof checkers to verify claims on the value-dependent types. So maybe using the term runtime is a bit to specific, but you do not have values (except literals) during typescript execution phase.

View on HN

Well, I can't be bothered to edit wikipedia, but it's a confusing claim. Dependent typing does not require runtime information, results can be produced at compile time. The dependent type depends on a value, but the interesting property of the value is independently tracked in the type system, it's not retrieved from runtime information.

The gist of how it works is so:

    createEmptyIntList() => List<size=0, content=int> {...}
    push(List<size=a, content=b>) => List<size=a+1, content=b> {...}
    firstElement(List<size=a, content=b> | a > 0) => b {...}

In this example, you don't need to know runtime values, you need to know that you can safely get the first element. For that, you just need to know that something has been pushed at least once in the list.

Since push returns a type that is different from createEmptyList, your typesystem has this information.

> The value does not exist during compilation.

    type Z = []["length"]
    type One = [0]["length"]
    type Two = [0,0]["length"]

The "value" in this case is symbolic, sort of like defining an array with variable length arr[x] and having the compiler verify that arr[x+5] is always out of bounds before knowing the actual value of x. If the type system is not powerful to prove correctness of some expression, you will need to insert a runtime check that lets the compiler to trust the value at compile time.

You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F<x>).

Reply on news.ycombinator.com