The types of the arguments to the function can have value constraints on it, and those constraints can be determined from a value that exists there: the name of the function.
In any case, the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it.
Wrote a bit more earlier: https://news.ycombinator.com/item?id=24716477
> the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it.
Unbounded infinity has infinite, uncountable bugs. A defined, bounded, well-constructed, proven type system has fewer bugs. Dependent types are not an axis of explosion, but rather a way to express useful bounds on multiple axes.
Less bugs does sound good, but after a minute thought there still seem to be uncountably infinite bugs even in the presence of dependent types. Just a few less than without. :)
(But yes: It's a good place to hook the AGI up!)
First, I don't know that dependent types have huge decidability issues that are an inherent obstacle in general; Idris for one has a very practical and elegant model of computation – things like totality checking, linearity rules and elimination of "scaffolding" types do a lot for us.
Dependent types do allow telling the compiler about more dimensions to consider – in a way that allows for a computational explosion at compile time – but those were always an available to consider as part of the computation; Dependent types dont add that complexity, rather they allow us to address it in the type system. I see it such that we're in a stronger position to manage and navigate that complexity by allowing us to express it to the compiler in a succinct and clear way near the core context of desired action. Dependent types allow us to do less by allowing us to do more.
And integrating purely functional mechanisms with side effects is a fun and interesting avenue of research, and I don't know that adding dependent types makes that more difficult; I'd think it makes it easier?
"This function's type depends on its function name. If its function name is "sqrt", then {check some simple rules about square roots, like if x is 0 then output is 0, if x > 1 then output < x, etc.}"
This one too:
"This function's type depends on its function name. If its function name is "sqrt", then check that it calls and returns a formally verified square root function applicable to its input type that is known to be decidable and appropriate to the floating point math definitions we're operating in right now"