Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is this use of UndecidableInstances okay? Alternatives?

I would like to do some magic in a library, allowing a product type to be destructured polymorphically. This is a more or less working mockup illustrating what I'd like to do:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} 
newtype Wrapped a = Wrapped { unwrap :: a } 

-- our example structure
ex :: (Int, (Int, Int))
ex = (1,(2,3))

class WrapDecomp x y | y -> x where
    decomp :: x -> y

instance (WrapDecomp x x', WrapDecomp y y')=> WrapDecomp (x,y) (x',y') where
    decomp (x,y) = (decomp x, decomp y)

instance WrapDecomp x (Wrapped x) where
    decomp = Wrapped


example = let w = decomp ex
              (w0, w1) = decomp ex
              (w0', (w1', w2')) = decomp ex :: (Wrapped Int, (Wrapped Int, Wrapped Int))
           in print $ ( unwrap w, unwrap w0, unwrap $ snd w1, unwrap $ fst w1 )
         -- Also works:
         -- in print $ ( unwrap w, unwrap w0, unwrap w1 )

My actual application is a library, and will have two properties that make the warts I noticed in the above acceptable:

  1. the Wrapped type constructor is not exported

  2. the user will always be calling unwrap on all Wrapped data in a binding (because of boring details of my application), so there shouldn't be ambiguity in practice

The consensus seems to be that UndecidableInstances isn't really bad, but I'd like to be sure the above is kosher before I proceed.


Update w/ solution

I puzzled with this for a bit, but I was able to solve my problem with TypeFamilies as follows:

{-# LANGUAGE TypeFamilies #-}
class Out a where
    type In a :: *
    decomp :: In a -> a

instance Out (Wrapped a) where
    type In (Wrapped a) = a
    decomp = Wrapped

instance (Out a, Out b)=> Out (a,b) where
    type In (a,b) = (In a,In b)
    decomp (x,y) = (decomp x, decomp y)
like image 787
jberryman Avatar asked Aug 04 '12 19:08

jberryman


1 Answers

The use of UndecidableInstances alone is kosher in general, what UndecidableInstances does is allow the type checker to try to resolve instances when it can't prove in advance that it will finish. If it does, the code is no less safe than if termination could have been proved in advance.

However, with your instances, you can create a situation where the type checker would loop with an expression that causes a constraint WrapDecomp x (x,y), for example

foo x = [fst $ decomp x, x]

The use of fst requires decomp x to have type (a,b) for some types a and b, thus an instance WrapDecomp t (a,b) where t is the type of x. Being in the same list requires that x have tape a too, so an

instance WrapDecomp a (a,b)

The only instance with a pair for the second parameter is

instance (Wrapdecomp x x', WrapDecomp y y') => WrapDecomp (x,y) (x',y')

hence a = (x,y) for some types x and y and the constraint of foo becomes

WrapDecomp (x,y) ((x,y),b)

The pairs instance says there is such an instance if there are instances

WrapDecomp y b

and

WrapDecomp x (x,y)

which is the exact form of instance we started with.

like image 126
Daniel Fischer Avatar answered Sep 20 '22 13:09

Daniel Fischer