search

cucapra / gator

Geometry types
https://capra.cs.cornell.edu/research/gator/
26 stars 11 forks source link

Require Canonical Transformations To Be Unique Under Subsumption #50

Open Checkmate50 opened 5 years ago

Checkmate50 commented 5 years ago

Canonical transformations are assumed to be unique -- there is exactly one canonical map between two coordinate systems. While this is not in fact always true (read: homogeneous coordinates), it is both best practice and most sensical to treat them as such. The only reason we currently do not do this is to allow the norm to homogeneous coordinates hack, something that was found to be done incorrectly from a type perspective.

Practically this means that invocations of in should fail if there are multiple ways to reach label B from label A in a single step (including subsumption). Note that this does not require checking if multiple paths exist over the course of several steps, as we assume that the programmer has checked that each of these paths are equivalent (see https://github.com/cucapra/linguine/wiki/Tutorial:-Casting-and-In-Expressions for details).

Checkmate50 commented 4 years ago

We should add tests to check this