Playing with Data.Constraint for great fun

FunWithDictionaries.hs

{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE ScopedTypeVariables    #-}

import Data.Constraint
import Data.Proxy

newtype (f ∘ g) a = O { getO :: f (g a) }

data Product (f :: k -> *) (xs :: [k]) where
   (:*:) :: f x -> Product f xs -> Product f (x ': xs)
   Nil   :: Product f '[]

uncons :: Product f (x ': xs) -> (f x, Product f xs)
uncons (x :*: xs) = (x, xs)

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where
   All c '[] = ()
   All c (x ': xs) = (c x, All c xs)

-- Map, lifted to the type level
type family Map (f :: k -> l) (xs :: [k]) :: [l] where
   Map f '[]        = '[]
   Map f (x ': xs) = f x ': Map f xs

-- Discharge a constraint with a dictionary
(~~>) :: Dict c -> (c => z) -> z
Dict ~~> z = z

-- If for all x in xs, (c x) holds, produce a list of dictionaries as evidence
dicts :: All c xs => Proxy c -> Product Proxy xs -> Product (Dict ∘ c) xs
dicts _ Nil        = Nil
dicts p (_ :*: xs) = O Dict :*: dicts p xs

-- If for all x in xs, (c (f x)) holds, produce a list of dictionaries as evidence
dictsF :: All c (Map f xs) => Proxy c -> Proxy f -> Product Proxy xs -> Product (Dict ∘ c ∘ f) xs
dictsF _ _ Nil        = Nil
dictsF p q (_ :*: xs) = O (O Dict) :*: dictsF p q xs

-- Given a list of dictionaries showing that for each x in xs, (c x) holds,
-- collapse them into a single dictionary showing that (c x) holds for all x.
collectDicts :: Product (Dict ∘ c) xs -> Dict (All c xs)
collectDicts Nil              = Dict
collectDicts (O Dict :*: ds') = collectDicts ds' ~~> Dict

-- Given a list of dictionaries showing that for each x in xs, (c (f x)) holds,
-- collapse them into a single dictionary showing that (c (f x)) holds for all x.
collectDictsF :: Product (Dict ∘ c ∘ f) xs -> Dict (All c (Map f xs))
collectDictsF Nil                  = Dict
collectDictsF (O (O Dict) :*: ds') = collectDictsF ds' ~~> Dict

-- Given a function which needs (d x) and (c (f x)) to hold for all x in xs,
-- map it over a list of xs if provided explicit dictionary evidence that these
-- constraints do in fact hold.
mapWithDicts :: forall c d f g xs. (forall x. (d x, c (f x)) => f x -> g x)
             -> Product (Dict ∘ c ∘ f) xs -> Product (Dict ∘ d) xs
             -> Product f xs -> Product g xs
mapWithDicts t ds1 ds2 xs =
   case xs of
      (x :*: xs') ->
         case uncons ds1 of
            (O (O Dict), ds1') -> case uncons ds2 of
               (O Dict,  ds2') -> t x :*: mapWithDicts t ds1' ds2' xs'
      Nil -> Nil

-- Map a function requiring certain constraints over a (Product f xs).
-- The function requires (c f), as well as (d (f x)) and (e x) for all x in xs.
mapWithConstraints :: forall c d e f g xs. (c f, All d (Map f xs), All e xs, KnownProduct xs)
                   => Proxy c -> Proxy d -> Proxy e
                   -> (forall x. (c f, d (f x), e x) => f x -> g x)
                   -> Product f xs -> Product g xs
mapWithConstraints _ _ _ f xs =
   mapWithDicts f (dictsF (Proxy :: Proxy d) (Proxy :: Proxy f) proxies) (dicts (Proxy :: Proxy e) proxies) xs
   where proxies = productProxy :: Product Proxy xs

-- Generate a Product of Proxies for any type-level list.
class                         KnownProduct (xs :: [k]) where productProxy :: Product Proxy xs
instance                      KnownProduct '[]         where productProxy = Nil
instance (KnownProduct xs) => KnownProduct (x ': xs)   where productProxy = Proxy :*: productProxy