Currying Product Types

Question

Using type families, we can define the function fold over a type and the underlying algebra for that type represented as an n-tuple of functions and constant values. This permits the definition of a generalized foldr function, defined in the Foldable type class:

import Data.Set (Set)
import Data.Map (Map)
import qualified Data.Set as S
import qualified Data.Map as M

class Foldable m where
  type Algebra m b :: *
  fold :: Algebra m b -> m -> b

instance (Ord a) => Foldable (Set a) where
  type Algebra (Set a) b = (b, a -> b -> b)
  fold = uncurry $ flip S.fold

instance (Ord k) => Foldable (Map k a) where
  type Algebra (Map k a) b = (b, k -> a -> b -> b)
  fold = uncurry $ flip M.foldWithKey

Similarly, constraint kinds permit the definition of a generalized map function. The map function differs from fmap by considering each value field of an algebraic data type:

class Mappable m where
  type Contains m     :: *
  type Mapped   m r b :: Constraint
  map :: (Mapped m r b) => (Contains m -> b) -> m -> r

instance (Ord a) => Mappable (Set a) where
  type Contains (Set a)     = a
  type Mapped   (Set a) r b = (Ord b, r ~ Set b)
  map = S.map

instance (Ord k) => Mappable (Map k a) where
  type Contains (Map k a)     = (k, a)
  type Mapped   (Map k a) r b = (Ord k, r ~ Map k b)
  map = M.mapWithKey . curry

From the user's perspective, neither function is particularly friendly. In particular, neither technique permits the definition of curried functions. This means that the user cannot easily apply either fold or the mapped function partially. What I would like is a type-level function that curries tuples of functions and values, in order to generate curried versions of the above. Thus, I would like to write something approximating the following type-function:

Curry :: Product -> Type -> Type
Curry ()       m = m
Curry (a × as) m = a -> (Curry as m b)

If so, we could generate a curried fold function from the underlying algebra. For instance:

  fold :: Curry (Algebra [a] b) ([a] -> b)
≡ fold :: Curry (b, a -> b -> b) ([a] -> b)
≡ fold :: b -> (Curry (a -> b -> b)) ([a] -> b)
≡ fold :: b -> (a -> b -> b -> (Curry () ([a] -> b))
≡ fold :: b -> ((a -> b -> b) -> ([a] -> b))

  map :: (Mapped (Map k a) r b) => (Curry (Contains (Map k a)) b) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (Curry (k, a) b) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (k -> (Curry (a) b) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (k -> (a -> Curry () b)) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (k -> (a -> b)) -> Map k a -> r

I know that Haskell doesn't have type functions, and the proper representation of the n-tuple would probably be something like a type-level length-indexed list of types. Is this possible?

EDIT: For completeness, my current attempt at a solution is attached below. I am using empty data types to represent products of types, and type families to represent the function Curry, above. This solution appears to work for the map function, but not the fold function. I believe, but am not certain, that Curry is not being reduced properly when type checking.

data Unit
data Times a b

type family Curry a m :: *
type instance Curry Unit        m = m
type instance Curry (Times a l) m = a -> Curry l m

class Foldable m where
  type Algebra m b :: *
  fold :: Curry (Algebra m b) (m -> b)

instance (Ord a) => Foldable (Set a) where
  type Algebra (Set a) b = Times (a -> b -> b) (Times b Unit)
  fold = S.fold

instance (Ord k) => Foldable (Map k a) where
  type Algebra (Map k a) b = Times (k -> a -> b -> b) (Times b Unit)
  fold = M.foldWithKey

 class Mappable m where
   type Contains m     :: *
   type Mapped   m r b :: Constraint
   map :: (Mapped m r b) => Curry (Contains m) b -> m -> r

 instance (Ord a) => Mappable (Set a) where
   type Contains (Set a)     = Times a Unit
   type Mapped   (Set a) r b = (Ord b, r ~ Set b)
   map = S.map

 instance (Ord k) => Mappable (Map k a) where
   type Contains (Map k a)     = Times k (Times a Unit)
   type Mapped   (Map k a) r b = (Ord k, r ~ Map k b)
   map = M.mapWithKey

Answer 1

A type-level list is exactly what you need! You got very close, but you need the full power of both DataKinds and ScopedTypeVariables for this to work properly:

{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances, TypeFamilies, TypeOperators, ScopedTypeVariables #-}
import GHC.Exts (Constraint)
import Data.Set (Set)
import Data.Map (Map)
import qualified Data.Set as S
import qualified Data.Map as M

-- | A "multifunction" from a list of inhabitable types to an inhabitable type (curried from the start).  
type family (->>) (l :: [*]) (y :: *) :: *
type instance '[] ->> y = y
type instance (x ': xs) ->> y = x -> (xs ->> y)

class Foldable (m :: *) where
  type Algebra m (b :: *) :: [*]
  fold :: forall (b :: *). Algebra m b ->> (m -> b)

instance (Ord a) => Foldable (Set a) where
  type Algebra (Set a) b = '[(a -> b -> b), b]
  fold = S.fold :: forall (b :: *). (a -> b -> b) -> b -> Set a -> b

instance (Ord k) => Foldable (Map k a) where
  type Algebra (Map k a) b = '[(k -> a -> b -> b), b]
  fold = M.foldWithKey :: forall (b :: *). (k -> a -> b -> b) -> b -> Map k a -> b

class Mappable m where
  type Contains m :: [*]
  type Mapped m (b :: *) (r :: *) :: Constraint
  map :: forall (b :: *) (r :: *). Mapped m b r => (Contains m ->> b) -> m -> r

instance (Ord a) => Mappable (Set a) where
  type Contains (Set a) = '[a]
  type Mapped (Set a) b r = (Ord b, r ~ Set b)
  map = S.map :: forall (b :: *). (Ord b) => (a -> b) -> Set a -> Set b

instance (Ord k) => Mappable (Map k a) where
  type Contains (Map k a) = '[k, a]
  type Mapped (Map k a) b r = r ~ Map k b
  map = M.mapWithKey :: forall (b :: *). (k -> a -> b) -> Map k a -> Map k b

Answer 2

Ok, I think my other answer isn't actually really an answer to your question. Sorry for that.

In your final code, compare the types of fold and map:

fold :: Curry (Algebra m b) (m -> b)
map  :: (Mapped m r b) => Curry (Contains m) b -> m -> r

There's a substantial difference here. The type of fold is just a type family application, whereas the type of map contains the final m -> r, mentioning the class parameter m. So in the case of map, it's easy for GHC to learn at which type you want to instance the class from the context.

Not so in the case of fold, unfortunately, because type families need not be injective, and therefore aren't easy to invert. So by seeing a particular type you use fold at, it's impossible for GHC to infer what m is.

The standard solution to this problem is to use a proxy argument that fixes the type of m, by defining

data Proxy m = P

and then giving fold this type instead:

fold :: Proxy m -> Curry (Algebra m b) (m -> b)

You have to adapt the instances to take and discard the proxy argument. Then you can use:

fold (P :: Proxy (Set Int)) (+) 0 (S.fromList [1..10])

or similar to call the fold function on sets.

To see more clearly why this situation is difficult for GHC to solve, consider this toy example instead:

class C a where
  type F a :: *
  f :: F a

instance C Bool where
  type F Bool = Char -> Char
  f = id

instance C () where
  type F () = Char -> Char
  f = toUpper

Now, if you call f 'x', there's no meaningful way for GHC to detect which instance you meant. The proxy would help here as well.

Answer 3

Ok, if I understand you correctly, you can create inconvenient folds, but want to have convenient curried folds.

Below is an explanation how to achieve this as a separate step. Yes, it can also be done all at once, I've done something similar before. However, I think the separate phase makes it clearer what's going on.

We need the following language extensions:

{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleInstances #-}

I'm using the following product and unit types:

data U = U
data a :*: b = a :*: b

infixr 8 :*:

As an example, let's assume we have an inconvenient version of a fold on lists:

type ListAlgType a r = (U -> r)
                   :*: (a :*: r :*: U -> r)
                   :*: U

inconvenientFold :: ListAlgType a r -> [a] -> r
inconvenientFold   (nil :*: cons :*: U) []       = nil U
inconvenientFold a@(nil :*: cons :*: U) (x : xs) = cons (x :*: inconvenientFold a xs :*: U)

We have a nested product type, and we want to curry both levels. I'm defining two type classes for this, one for each layer. (It might be doable with one more general function, I haven't tried in this case.)

class CurryInner a where
  type CurryI a k :: *
  curryI   :: (a -> b) -> CurryI a b
  uncurryI :: CurryI a b -> a -> b

class CurryOuter a where
  type CurryO a k :: *
  curryO   :: (a -> b) -> CurryO a b
  uncurryO :: CurryO a b -> (a -> b) -- not really required here

Each type class implements the isomorphism between the curried and uncurried types. The type classes look identical, but CurryOuter will call CurryInner for each component of the outer nested tuple.

The instances are relatively straightforward:

instance CurryInner U where
  type CurryI U k = k
  curryI f   = f U
  uncurryI x = \ U -> x

instance CurryInner ts => CurryInner (t :*: ts) where
  type CurryI (t :*: ts) k = t -> CurryI ts k
  curryI f   = \ t -> curryI (\ ts -> f (t :*: ts))
  uncurryI f = \ (t :*: ts) -> uncurryI (f t) ts

instance CurryOuter U where
  type CurryO U k = k
  curryO f   = f U
  uncurryO x = \ U -> x

instance (CurryInner a, CurryOuter ts) => CurryOuter ((a -> b) :*: ts) where
  type CurryO ((a -> b) :*: ts) k = CurryI a b -> CurryO ts k
  curryO f   = \ t -> curryO (\ ts -> f (uncurryI t :*: ts))
  uncurryO f = \ (t :*: ts) -> uncurryO (f (curryI t)) ts

That's it. Note that

*Main> :kind! CurryO (ListAlgType A R) ([A] -> R)
CurryO (ListAlgType A R) ([A] -> R) :: *
= R -> (A -> R -> R) -> [A] -> R

(for suitably defined placeholder types A and R). We can use it as follows:

*Main> curryO inconvenientFold 0 (+) [1..10]
55

Edit: I now see you're actually only asking about currying the outer layer. You then only need one class, but can use the same idea. I used this example because I had written something for a sum-of-product based generic programming library which needed two levels of currying before, and thought at first you are in the same setting.