Ensuring that a haskell type A contains a member of type B

Question

Let us look at the following code:

transformBi (++"asdasd") [1,2,3,4]

Clearly, this code does nothing, but it still compiles fine. I would like to create a new version of transformBi that will not compile if the compiler can prove by the types that it is a no-op. Ideally, this would be done by a typeclass called Contains, so that the type of the new transformBi will be

transformBi :: (Biplate from to, Contains from to) => (to -> to) -> from -> from

How do we implement Contains?

I am looking for a Contains that can be automatically derived, not for something I have to write for every algebraic data type.

Answer 1

If there is a Generic instance for a type, then we can search the type of its generic representation for a certain field. We would like to be able to traverse recursive and mutually recursive types, so we need to:

1. Ensure we don't loop endlessly on recursive types. We need to keep record of the visited types, and stop when we encounter one.

2. Make the type family call lazy enough so that GHC actually stops computing when we want it to. Closed type families are only lazy on top-down equation matching (i. e. the computation stops at the first matching equation), so we use a helper for recursion.

Here it is:

{-# LANGUAGE
    TypeOperators,
    TypeFamilies,
    DataKinds,
    ConstraintKinds,
    UndecidableInstances,
    DeriveGeneric,
    DeriveDataTypeable
    #-}

import Data.Generics.Uniplate.Data 
import GHC.Generics
import Data.Type.Bool
import Data.Type.Equality
import Data.Data

type family Elem (x :: *) (xs :: [*]) :: Bool where
    Elem x '[]       = False
    Elem x (y ': xs) = (x == y) || Elem x xs

type family LazyRec hasVisited vis t x where
    LazyRec True  vis x y = False
    LazyRec False vis x x = True
    LazyRec False vis t x = Contains (t ': vis) (Rep t ()) x

type family Contains (visited :: [*]) (t :: *) (x :: *) :: Bool where
    Contains vis (K1 i c p)    x = LazyRec (Elem c vis) vis c x 
    Contains vis ((:+:) f g p) x = Contains vis (f p) x || Contains vis (g p) x
    Contains vis ((:*:) f g p) x = Contains vis (f p) x || Contains vis (g p) x
    Contains vis ((:.:) f g p) x = Contains vis (f (g p)) x
    Contains vis (M1 i t f p)  x = Contains vis (f p) x
    Contains vis t             x = False

Now we can define a shorthand for a Biplate that works only when from possibly contains a to field:

type family Biplate' from to where
    Biplate' from to = (Contains '[from] (Rep from ()) to ~ True, Biplate from to)

And behold:

transformBi' :: Biplate' from to => (to -> to) -> from -> from
transformBi'= transformBi

-- this one typechecks, but it's a no-op.
foo :: [Int]
foo = transformBi (++"foo") ([0..10] :: [Int])

-- type error 
foo' :: [Int]
foo' = transformBi' (++"foo") ([0..10] :: [Int])

-- works as intended
foo'' :: [Int]
foo'' = transformBi' (+(10::Int)) ([0..10] :: [Int])

-- works for recursive/mutually recursive types too
data Foo = Foo Int Bar deriving (Show, Generic, Typeable, Data)
data Bar = Nil | Cons () Foo deriving (Show, Generic, Typeable, Data)

foo''' :: Bar
foo''' = transformBi' (+(10::Int)) (Cons () (Foo 0 Nil))

Some notes:

• This only works for Data.Generic.Uniplate.Data. In the case of Uniplate.Direct we could implement custom biplate-s that may or may not visit certain fields, so we can't reason anymore about what's no-op and what's not, which is another reason why this doesn't work there.

• We rely on the consistency of GHC and uniplate internals, i. e. we suppose that uniplate visits a to field iff Rep contains a corresponding field. This is a reasonable assumption, but might be broken by bugs beyond our control. Also, we have to change the definition of Contains whenever the Generic representation API changes. On the other hand, we don't pay any runtime penalty for Generic, since we only inspect Rep at compile time.