5 ms·

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

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.

shalabhc 9y ago
I wish this was adopted more broadly, e.g. by Rust and other newer languages.
- oconnor663 9y ago
  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?"
  - AnimalMuppet 9y ago
    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).
  - willtim 9y ago
    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.
  - zbobet2012 9y ago
    Look at Idris to see how this kind of thing works. https://jeremywsherman.com/blog/2015/10/10/idris-metaprogramming-hello-world/ https://jeremywsherman.com/blog/2015/10/10/idris-metaprogram...
  - ziotom78 9y ago
    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.
    - willtim 9y ago
      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.
- Others 9y ago
  If I'm understanding what you want correctly, Rust kinda will get that once the `!` type is stable/used in type inference correctly.
gertef 9y ago
> 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.
- ORioN63 9y ago
  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.
- willtim 9y ago
  Yes I don't use deferred type errors much. But the parent poster wanted the option to avoid worrying about type correct programs.

shalabhc 9y ago

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

oconnor663 9y ago
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?"
- AnimalMuppet 9y ago
  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).
- willtim 9y ago
  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.
- zbobet2012 9y ago
  Look at Idris to see how this kind of thing works. https://jeremywsherman.com/blog/2015/10/10/idris-metaprogramming-hello-world/ https://jeremywsherman.com/blog/2015/10/10/idris-metaprogram...
- ziotom78 9y ago
  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.
  - willtim 9y ago
    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.
Others 9y ago
If I'm understanding what you want correctly, Rust kinda will get that once the `!` type is stable/used in type inference correctly.

gertef 9y ago

> 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.

ORioN63 9y ago
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.
willtim 9y ago
Yes I don't use deferred type errors much. But the parent poster wanted the option to avoid worrying about type correct programs.