3 ms·
Is ! verified or enforced; i.e. does the compiler check to make sure that the functions does terminate in some way (besides returning) ?
by winter_blue 10y ago
Is ! verified or enforced; i.e. does the compiler check to make sure that the functions does terminate in some way (besides returning) ?
- jonesetc 10y agoLooks like it [0]. The author had to use inline assembly, so compiler couldn't enforce it and failed to compile. They had to add an annotation to say that the code after the assembly was unreachable. [0] http://os.phil-opp.com/better-exception-messages.html#intrinsics-unreachable http://os.phil-opp.com/better-exception-messages.html#intrin...
- Gankro 10y agoIt's the exact same analysis as ensuring all paths of a function do return the right type -- you just make sure all paths call a divergent function (typically unconditional panic) or enter a loop {} that never breaks/returns. This is of course a conservative analysis so e.g. "while true { }" is assumed to terminate and is rejected. Failing to perform this verification correctly would trivially lead to memory unsafety as calling code is allowed to assume such a function returns any and all requested types.
- pcwalton 10y agoIt'd be type and memory unsafe if it weren't verified, so yes, it is.
- Peaker 10y agoIt seems to be equivalent to Haskell's Void type. The Void type is simply the type of no values. If you cannot create a value of this type, yet you "return" it, then it is proof that you never return.
- munificent 10y agoAlso "Nothing" in Scala and "never" in TypeScript. The bottom type[1] goes by a lot of names. Interesting, I think Haskell does sort of have a value for it, undefined. It's just that if you look at that value too hard, it throws. :) [1]: https://en.wikipedia.org/wiki/Bottom_type https://en.wikipedia.org/wiki/Bottom_type