Generics : run-time ADT for types with instances

Question

Is it possible with Haskell / GHC, to extract an algebraic data type representing all types with Eq and Ord instances ? This would probably need Generics, Typeable, etc.

What I would like is something like :

data Data_Eq_Ord = Data_String String 
                 | Data_Int Int
                 | Data_Bool Bool
                 | ...
deriving (Eq, Ord)

For all types known to have instances for Eq and Ord. If it makes the solution easier, we can limit our scope to Ord instances, since Eq is implied by Ord. But is would be interesting to know if constraints intersection is possible.

This data type would be useful because it gives the possibility to use it where Eq and Ord constraints are required, and pattern-match at runtime to refine on types.

I would need this to implement a generic Map Key Value, where Key would be this type, in a Document Indexing library, where the keys and their type is known at run-time. This library is here. For the moment I worked around the issue by defining a data DocIndexKey, and a FieldKey class, but this is not fully satisfactory since it requires boilerplate and can't cover all legit candidates.

Any good alternative approach to this situation is welcome. For some reasons, I prefer to avoid Template Haskell.

My first thought is whether you can use Data.Typeable and/or Data.Dynamic for this... — MathematicalOrchid
Generics and Typeable are definitely not going to get you there. Typeclasses are by design open, i.e. it's always possible to add more instances later on. So Data_Eq_Ord could never be guaranteed to be complete. Maybe it's possible with TH do get all the instances that are currently in scope, but I'm not sure about even that. — I'd say your best bet is probably to use TypeReps as keys into a conceptually infinite, lazy MemoTrie structure or something. — leftaroundabout
When compilation is terminated, no more instances can be added, so at some point the compiler knows what instances of Ord are defined over the whole program. That said, there is a challenge in the modules compilation sequence indeed. — Paul R

HTNW HTNW · Accepted Answer · 2020-05-29T04:10:00

Well, it's not an ADT, but this definitely works:

data Satisfying c = forall a. c a => Satisfy a
class (l a, r a) => And l r a where
instance (l a, r a) => And l r a where

ex :: [Satisfying (Typeable `And` Show `And` Ord)]
ex = [ Satisfy (7 :: Int)
     , Satisfy "Hello"
     , Satisfy (5 :: Int)
     , Satisfy [10..20 :: Int]
     , Satisfy ['a'..'z']
     , Satisfy ((), 'a')]

-- An example of use, with "complicated" logic
data With f c = forall a. c a => With (f a)
--                 vvvvvvvvvvvvvvvvvvvvvvvvvv QuantifiedConstraints chokes on this, which is probably a bug...
partitionTypes :: (forall a. c a => TypeRep a) -> [Satisfying c] -> [[] `With` c]
partitionTypes rep = foldr go []
   where go (Satisfy x) [] = [With [x]]
         go x'@(Satisfy (x :: a)) (xs'@(With (xs :: [b])) : xss) =
             case testEquality rep rep :: Maybe (a :~: b) of
                 Just Refl -> With (x : xs) : xss
                 Nothing -> xs' : go x' xss

main :: IO ()
main = traverse_ (\(With xs) -> print (sort xs)) $ partitionTypes typeRep ex

Exhaustivity is much harder. Perhaps with a plugin, you could get GHC to do it, but why bother? I don't believe GHC actually tries to keep track of what types it has seen. In particular, you'd have to scan all modules in the project and its dependencies, even those that haven't been loaded by the module containing the type definition. You'd have to implement it from the ground-up. And, as this answer shows, I very much doubt you would actually be able to use such exhaustivity for anything that you can't already do by just taking the open universe as it is.

Generics : run-time ADT for types with instances

1 Answers