If you have a haskell style type system you can do such a thing and have the type system prevent you from calling things multiple times, eg:
data P1 a
data P2 a
data PointNotEqual where
| T :: P1 a -> P2 a -> PointNotEqual
getP1 :: P1 a -> Point
getP2 :: P2 a -> Point
checkNE :: Point -> Point -> Maybe PointNotEqual
(+) :: P1 a -> P2 a -> Point
Here when you are given a PointNotEqual, you don’t know what the type variable is, only that it’s the same between the two points. So you (ie the compiler) cannot prove that a P1 or P2 from a different call to PointNotEqual has the same type variable, so you can’t add them.
But these types also mean you need to do the check before every addition which defeats the point of the whole constant time thing, so the typechecking is still limited. And I guess you can’t do it in Go either.
But these types also mean you need to do the check before every addition which defeats the point of the whole constant time thing, so the typechecking is still limited. And I guess you can’t do it in Go either.