|
|
|
|
|
|
by star-castle
2939 days ago
|
|
|
c.f. https://github.com/deech/LeftPad/blob/master/left-pad.org , in particular "At the type level we have:" and "At the level of sorts and refinements:" Or take this silly code: https://stackoverflow.com/questions/50658528/how-do-you-repl... At the type level, nothing changes between the first program and the second. At the level of sorts and refinements, ATS2 is given more information in the second program so it's able to turn the two noted error conditions into compile time errors, when in first program they could only be runtime errors. I haven't heard anything bad about Hongwei Xi. Who are these ill-regarded researchers? |
|
|