5 ms·
Another thing to consider is the type system of Idris where the compiler may recognise at compile time that the value can only be of a certain subset of a union
by fhars 7y ago
Another thing to consider is the type system of Idris where the compiler may recognise at compile time that the value can only be of a certain subset of a union and, more importantly, can use the type of a function to infer much of the correct implementation, like, all the cases that must be handled and sometimes even how to handle them.
- _bxg1 7y agoLots of type systems support type inference. It seemed (I could have misinterpreted) like the OP was suggesting that in a perfect world all types would be inferred. That's the idea I was disagreeing with.
- fhars 7y agoNormal type inference deduces the type from the code, Idris can infer the implementation from the type if the type is specific enough. In a way, this is Church in action: the type is a theorem, and the compiler is a proof assistant that helps to automatically find a proof (a correct program having that type). So Idris is an argument supporting your position: if it works (it is still part of a research program), the types are the primary expression, and the code is secondary.