Hacker News new | past | comments | ask | show | jobs | submit login

Dependently typed languages do use the same evaluation mechanism for the type level and value level. In Java you have List<Int> and that's different than foo(bar), but in dependently typed languages Int is just a value of type Type, and List is a function that takes a Type and returns a Type. The difference is that this evaluation takes place at compile time.

For run-time checking there is the work on higher order contracts. That's a systematic way to create wrappers around functions that check the input and output values against a contract. For example, the contract A -> B applied to a function f wraps f with a check on the input and output. The A and B itself can be primitive contracts such as Int which just checks if a value is an int, or function contracts, so that you can have (Int -> Int) -> Int. The neat thing about contracts is that they can tell you whose fault it is if something goes wrong. If you wrap f with the contract (Int -> Int) -> Int, and you call f(g) with some function g, then the contract will ensure that f can only pass Int to g, and if it passes something else the contract will tell you that's f's fault. On the other hand, if g returns something that's not an Int, then the contract can tell you that's g's fault. In general for some value v wrapped with a contract C evaluated in a context E(v wrapped with C), the contract can tell you if it's v's fault if something goes wrong, or E's fault. This is very helpful if v is a module and E is code that uses the module: the contracts can tell you if the module is at fault or whether the user of the module is at fault.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: