How to map existentials with multiple constraints in Haskell?

user_342882 0
Viewed 79

I figured out how to process a list of heterogeneous types constrained by a single class:

data Ex c = forall a. (c a) => Ex a

forEx :: [Ex c] -> (forall a. c a => a -> b) -> [b] 
forEx [] _ = [] 
forEx (Ex a:r) f = f a : forEx r f

> forEx @Show [Ex 3, Ex (), Ex True] show
["3","()","True"]

Looks great, but in real life instead of show function would more complicated one relying on more than 1 constraint. Going further by analogy doesn't work:

Attempt 1:

forEx @(Show, Eq) [Ex 3, Ex (), Ex True] show

<interactive>:85:8: error:
    • Expected kind ‘* -> Constraint’, but ‘(Show, Eq)’ has kind ‘*’

Attempt 2:

type ShowEq c = (Show c, Eq c)
> forEx @ShowEq [Ex 3, Ex (), Ex True] show

<interactive>:87:1: error:
    • The type synonym ‘ShowEq’ should have 1 argument, but has been given none

Attempt 3 works, but defining dummy class and instance for one time use is to clumsy:

class (Show a, Eq a) => ShowEq1 a 
instance (Show a, Eq a) => ShowEq1 a
forEx @ShowEq1 [Ex (3::Int), Ex (), Ex True] show

["3","()","True"]
haskell
2 Answers

With enough language features, it's possible to make a constraint that combines constraints:

{-# LANGUAGE RankNTypes, ConstraintKinds, GADTs, TypeApplications, MultiParamTypeClasses, FlexibleInstances, UndecidableSuperClasses #-}

data Ex c = forall a. (c a) => Ex a

forEx :: [Ex c] -> (forall a. c a => a -> b) -> [b] 
forEx [] _ = [] 
forEx (Ex a:r) f = f a : forEx r f

class (c a, d a) => (Combined c d) a
instance (c a, d a) => (Combined c d) a

shown :: [String]
shown = forEx @(Combined Show Eq) [Ex 3, Ex (), Ex True] show
user_59231390

I would do it this way:

{-# LANGUAGE DataKinds, GADTs, RankNTypes, StandaloneKindSignatures, TypeFamilies, TypeOperators #-}

import Data.Kind

type All :: [Type -> Constraint] -> Type -> Constraint
type family All cs t
  where All '[] _ = ()
        All (c ': cs) t = (c t, All cs t)

data Ex cs
  where Ex :: All cs t => t -> Ex cs

forEx :: [Ex cs] -> (forall a. All cs a => a -> b) -> [b]
forEx [] _ = []
forEx (Ex x : xs) f = f x : forEx xs f

Now Ex is parameterised not on a single class but a list of classes1. And we have the All type family for taking a list of classes and applying them all to the same type, combining them into a single Constraint.

This means (unlike the class-to-combine-two-other-classes approach) it now supports any number of constraints you need.

You can call it like this2:

λ forEx @[Show, Eq] [Ex 3, Ex (), Ex True] show
["3","()","True"]
it :: [String]

1 Technically not a list of classes, but rather a list of things that need one more type argument to produce a Constraint. Single-param classes would be the most common thing you'd use this on, though.

2 Of course Eq is not a very useful constraint to have in there, because you can't actually use it without another value of the same unknown type, and you've thrown away all the information about whether any given type is the same type.

user_4501280
Related