Geometry Bugs and Geometry Types (www.cs.cornell.edu)
from armchair_progamer@programming.dev to programming_languages@programming.dev on 10 Aug 2024 21:19
https://programming.dev/post/17970911

Key excerpt:

At OOPSLA 2020, Prof. Dietrich Geisler published a paper about geometry bugs and a type system that can catch them. The idea hasn’t exactly taken over the world, and I wish it would. The paper’s core insight is that, to do a good job with this kind of type system, you need your types to encode three pieces of information:

• the reference frame (like model, world, or view space)
• the coordinate scheme (like Cartesian, homogeneous, or polar coordinates)
• the geometric object (like positions and directions)

In Dietrich’s language, these types are spelled scheme<frame>.object. Dietrich implemented these types in a language called Gator with help from Irene Yoon, Aditi Kabra, Horace He, and Yinnon Sanders. With a few helper functions, you can get Gator to help you catch all the geometric pitfalls we saw in this post.

#programming_languages