Hacker News Reader

Comment by willtim | Hacker News Reader

There's no reason why static type errors can't be deferred until runtime, GHC Haskell can do this. Personally I find types invaluable when prototyping. I often fill in the implementations after I work out the types.

View on HN

I wish this was adopted more broadly, e.g. by Rust and other newer languages.

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?"

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.

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.

If I'm understanding what you want correctly, Rust kinda will get that once the `!` type is stable/used in type inference correctly.

> I often fill in the implementations after I work out the types.

OK, but that's the opposite of deffering type errors until runtime.

Using "undefined"/bottom as the implemenation of a function is how we wrote Haskell before GHC added support for deferring type-errors.

Oops. I still use undefined everywhere, while my code isn't complete.

Also, typed holes. Typed holes are awesome for building implementations based on types.

Yes I don't use deferred type errors much. But the parent poster wanted the option to avoid worrying about type correct programs.

Reply on news.ycombinator.com