> you can do that in a function preamble (constructor), too. Well, yeah, but that's a runtime failure. Obviously that's heaps better than just failing at some

> you can do that in a function preamble (constructor), too. Well, yeah, but that's a runtime failure. Obviously that's heaps better than just failing at some arbitrary later time, but if might be better still to force the program writer to consider up front what should happen if construction were to fail. In the particular case of preconditions for constructing data I would say that constructor validation is usually sufficient for my purposes, at least. I routinely use it in Haskell (abstract newtypes) and it seems to work fine, especially when you couple it with general validation (REST services). EDIT: I should mention: What I personally find very attractive about fully dependently typed languages is the fact that you, the programmer, get to choose exactly how much you want to prove. Want to work with a JSONValue which can be any old JSON? Sure, you can do that! Want to work with a JSONValue which must contain (at least) keys 'foo' and 'bar' which map to data of type 'Foo' and 'Bar' at all times? Sure you can do that too! (JSON may not be the best example, but I hope you get the meaning.) Of course type inference suffers a bit, error messages probably too. However, I don't see that as a huge problem. YMMV.