Hacker News Reader

Comment by skulk | Hacker News Reader

Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.

View on HN

Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point?

What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing

> What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code

This doesn't even exist in TypeScript. If I change

    function foo(a: any) { return baz(a); }

    function foo(a: number) { return baz(a); }

whoever calls foo has to still prove (or assert) that the argument is a number.

Is that what you're after, asserting a dependent type? For example being able to change:

    function divByTwo(a: number): number { return a/2; }

    function divByTwo(a: even_number): number { return a/2; }

You want every place divByTwo is called to also automatically supply a proof that the argument is even?

i don't even need it to go beyond the insides of a function. something like a proof of an invariant that's only relevant inside the function's body would be fine. e.g. in Rust, almost every place where you see something like ".unwrap()" with "// unwrap safety:" comment, this comment could be an assertion easily proven from the few lines above

Not sure if it's what you're asking for, but in lean, you can put `sorry` to skip a proof. It's `believe_me` in Idris2, and I think the Agda version is `trustMe`.

You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).

Reply on news.ycombinator.com