Hacker News new | ask | show | jobs
by shalabhc 3234 days ago
I wish this was adopted more broadly, e.g. by Rust and other newer languages.
2 comments

What would the semantics of that be? Something like "this function contains a type error, so if you call it your code will just panic?"
Look at Idris to see how this kind of thing works.

https://jeremywsherman.com/blog/2015/10/10/idris-metaprogram...

If I understand well, Ada packages provide the necessary architecture for this kind of stuff. A package is like a Python "module", but it is typically split in two files: a specification, just containing the declaration of all the types and functions exported by the package, and a body, which actually implements the functions working on those types. When writing a program which uses that package, if you only compile it without linking, the compiler will complain about wrong types even if no function has been implemented yet.

A poor man's version of the above schema can be achieved in C/C++ as well. Just declare your functions in a header file and include it in your program, then compile without linking.

This is not the same thing as deferred type errors though. The programs are still type correct, it's just that some of the implementations are missing / producing errors.
At it's simplest, I could see it being a compiler flag. No annotations needed. Default would be strict compile-time typing. But with a flag, you could turn type errors into warnings (and runtime panics), or even into not-even-warnings, just silence (and runtime panics).
Haskell can defer them by producing thunks (values) containing runtime exceptions. But unlike a dynamic-only language, you still get to know about the errors at compile time, by way of a set of warnings.
If I'm understanding what you want correctly, Rust kinda will get that once the `!` type is stable/used in type inference correctly.