|
|
|
|
|
|
by rybosome
4446 days ago
|
|
|
As others have noted, it's less about the compiler running code and making determinations as it is using extremely robust, information-rich types. For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector. Operations that increase the size of the vector are guaranteed to return a non-empty vector. They might look something like this: (::) : a -> Vector a n -> Vector a (S n)
This says that an element cons a vector of any size results in a vector that is guaranteed to be non-empty. This means that you could safely write a function to retrieve the head of a list by restricting the type to lists that are guaranteed to be non-empty. head : Vector a (S n) -> a
Something like the following pseudo-code in a REPL(I don't actually know a thing about Idris): let nums : Vector Int n = []
head nums
...would fail to compile, since the second type param to nums is simply `n` rather than `(S n)`, as required by our `head` function. All of the things you would expect from Haskell like the power of ADTs and pattern-matching apply here, so you get even more compile time type-soundness. |
|
|
In case anyone's wondering, only the first of these (the element type) is a type parameter, since it has a constant value in all sub-expressions (ie. the cons cells all contain elements of the same type).
The second is a 'type index', which is a more general term (type parameters are a special case of type indices), since its value changes in the sub-expressions (the cons cells have different lengths).
The difference is that we don't need to pattern-match parameters on every recursive call, since they're guaranteed to be constant (although we can if we like).
I didn't know this until I asked http://cs.stackexchange.com/questions/20100/what-are-the-dif...