User type instance propagation to Refined

[yaitskov]

Hi.

I tried to use hello world and realized that Refined wraps a user type and hides all instances of user type. It is especially painful for numbers.

My first thought was to add an universal instance to library

instance (Num v, Predicate p v) => Num (Refined p v) where 
    (+) rx ry = case refine $ unrefine rx + unrefine ry of 
                          Right x -> x; 
                          Left e -> error (show e) 

I am not sure, because it is gonna be orphan instance isn't it? Maybe this could be extracted into a TH function to generate particular instances on request. I am interested from theoretical side than practical. What would be the best solution?

[chessai]

Hmmm I thought I replied to this. Apologies.

Why not just use the Either monad?

liftRefine :: forall p0 p1 a b. (Predicate p0 a, Predicate p1 b) => (a -> b) -> Refined p0 a -> Either RefineException (Refined p1 b)
liftRefine f r = refine (f (unrefine r))

liftRefine2 :: forall p0 p1 p2 a b c. (Predicate p0 a, Predicate p1 b, Predicate p2 c) => (a -> b -> c) -> Refined p0 a -> Refined p1 b -> Either RefineException (Refined p2 c)
liftRefine2 f rx ry = refine (f (unrefine rx) (unrefine ry))

plus, times, minus :: forall p0 p1 p2 x. (Predicate p0 x, Predicate p1 x, Predicate p2 x, Num x) => Refined p0 x -> Refined p1 x -> Either RefineException (Refined p2 x)
plus = liftRefine2 (+)
times = liftRefine2 (*)
minus = liftRefine2 (-)

randomComputation :: (Num x, Predicate p x) => Refined p x -> Either RefineException x
randomComputation r = do
  x0 <- plus r r
  x1 <- times r r
  minus x1 x0

[nikita-volkov]

We cannot add instances of Num, for the same reason as why we cannot add instances of Functor: the result of the operation may not satisfy the predicate, so it needs to be validated.

The way you're supposed to act in these situations is simply unrefine the values you want to operate on, apply your operations and refine the result. This approach scales to any number of inputs.

[chessai]

Closing since this issue is not actionable