Look, I love Rust, but what one can expect of its type inference is unpredictable and poorly documented. It gets confused often, and frequently cannot explain to the user why it failed to guess the type ascription. And manual ascriptions within subexpressions (i.e. not just at bindings) are still an "unstable" feature.
Peano numbers work (sorta) in Haskell because Hindley-Milner is so damn predictable, and they work in Coq because you can bust out the Ltac stick and administer a beatdown when necessary.
People should not be trying to do type-level programming in a language whose awesome new type system has run so far ahead of its type inference.
2 comments
[ 2.7 ms ] story [ 17.4 ms ] threadLook, I love Rust, but what one can expect of its type inference is unpredictable and poorly documented. It gets confused often, and frequently cannot explain to the user why it failed to guess the type ascription. And manual ascriptions within subexpressions (i.e. not just at bindings) are still an "unstable" feature.
Peano numbers work (sorta) in Haskell because Hindley-Milner is so damn predictable, and they work in Coq because you can bust out the Ltac stick and administer a beatdown when necessary.
People should not be trying to do type-level programming in a language whose awesome new type system has run so far ahead of its type inference.