Search code examples
haskellconstraint-kinds

Constraint kinds: Pass multiple constraints


When I have a data type like the following in haskell:

data A ctx = A (forall a. ctx a => a -> a)

Then I can put functions that work on values of types of a given class into this datatype:

> A (+3) :: A Num
A (+3) :: A Num :: A Num

But is it also possible to put functions which have multiple constraints into this datatype? I tried this:

> :t ((+ 3) . succ)
((+ 3) . succ) :: (Enum c, Num c) => c -> c
> :t A ((+ 3) . succ) :: A (Enum,Num)
  Expecting one more argument to `Enum'
  In an expression type signature: A (Enum, Num)
  In the expression: A ((+ 3) . succ) :: A (Enum, Num)

So this doesn't work. How is it possible to do what I want, or is it impossible? I know one solution would be to use a "dummy" data type and a type family, but I don't want to do that if there is another way because of the it's complexity. Also, I this example I could have just used (+1) instead of succ, but there are more complex cases where such a transformation to just one class is not possible.


Solution

  • I've found one way to generalize the idea of joining multiple classes into one. Although it's quite awkward to use, it works.

    {-# LANGUAGE ConstraintKinds       #-}
    {-# LANGUAGE EmptyDataDecls        #-}
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE GADTs                 #-}
    {-# LANGUAGE KindSignatures        #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE OverlappingInstances  #-}
    {-# LANGUAGE RankNTypes            #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TypeOperators         #-}
    {-# LANGUAGE UndecidableInstances  #-}
    module Test where
    
    import GHC.Exts
    
    data (:>+<:) ctx1 ctx2 a where
      C'C :: (ctx1 a, ctx2 a) => (ctx1 :>+<: ctx2) a
    
    data (:++:) (ctx1 :: * -> Constraint) (ctx2 :: * -> Constraint) = C
    
    class Ctx2 c1 c2 a where
      useCtx :: c1 :++: c2 -> a -> ((c1 :>+<: c2) a -> b) -> b
    
    instance (c1 a, c2 a) => Ctx2 c1 c2 a where
      useCtx _ a f = f C'C
    
    fC :: (Ctx2 Num Enum a) => a -> a
    fC a = useCtx (C :: Num :++: Enum) a $ \C'C  -> 3 + succ a
    
    data A ctx = A 
      { call :: forall a. ctx a => a -> a
      }
    
    main = print $ call (A fC :: A (Ctx2 Num Enum)) 3
    

    It should be possible to use constraint aliases to define Ctx3, Ctx4, ...