Re:Generalizing 'jq' and Traversal Systems using optics and ...
by AnthonBerg on Thursday October 08, 2020 @02:37AM
(#24716477)
To continue the thought: This dependent type is expressible, trivially decidable, and has no additional side effect burden:
"This function's type depends on its function name. If its function name is "sqrt", then {check some simple rules about square roots, like if x is 0 then output is 0, if x > 1 then output < x, etc.}"
This one too:
"This function's type depends on its function name. If its function name is "sqrt", then check that it calls and returns a formally verified square root function applicable to its input type that is known to be decidable and appropriate to the floating point math definitions we're operating in right now"
"This function's type depends on its function name. If its function name is "sqrt", then {check some simple rules about square roots, like if x is 0 then output is 0, if x > 1 then output < x, etc.}"
This one too:
"This function's type depends on its function name. If its function name is "sqrt", then check that it calls and returns a formally verified square root function applicable to its input type that is known to be decidable and appropriate to the floating point math definitions we're operating in right now"