Earlier quoted context omitted.
In dependent types, types depend on values. Here, the type depends on the value that is the function name :) As far as I know, this is literally actually possible in Idris, right now. 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, uncounta…
Reading your other comment, I'll concede that it's not impossible to encode these things into the type system. I don't think it will scale beyond toy examples (at least until AGI is a thing). There are plenty of function names that represent highly specific business processes (and jargon) and I don't see how any type system will have enough context for that. Less bugs does sound good, but after a minute thought there…
(But yes: It's a good place to hook the AGI up!)