Data Promotion Syntax

Question

I recently discovered the Data.Promotion half of singletons. It has loads of type families which allow essentially arbitrary computation at the type level. I have a couple of questions about usage:

1. What is the difference between ($), (%$), ($$), and are they related to :++$, :.$, etc? Are these actually infix operators? I was under the impression all infix type constructors had to begin with a :.

2. I'm trying to map a constructor over a list:

   {-# LANGUAGE DataKinds, TypeOperators, PolyKinds #-}
   import Data.Promotion.Prelude
   
   data Foo a b
   type MyList = '[Int, Double, Float]
   
    -- expects one more argument to `Foo`
   type FooList1 b = Map ((Flip Foo) $ b) MyList
   
   -- parse error on the second `b`
   type FooList2 b = Map (($ b) :. Foo) MyList 
   

   but I'm having trouble using a multi-parameter type constructor. Ideas?

3. I was able to replace all of the type functions I had written with equivalent functions from Data.Promotion except this one:

   type family ListToConstraint (xs :: [Constraint]) :: Constraint
   type instance ListToConstraint '[] = ()
   type instance ListToConstraint (x ': xs) = (x, ListToConstraint xs)
   

   Is there some kind of magic going on with the Constraint kind that would prevent its manipulation as nested pairs?

Answer 1

1. As has been explained in the comments, there's no longer a syntactic requirement for infix functions on the type level to start with a colon. So yes, all these are infix operators. No two infix operators are automatically related to each other, but the singletons library uses some naming conventions internally, to relate symbols used for defunctionalization (see below) to their normal counterparts.

2. There's a whole bunch of problems arising from the fact that type families cannot be partially applied, but datatypes can. That's why the singletons library uses a technique called defunctionalization: for each partially applied type function, it defines a datatype. There's then a (very large and open) type family called Apply that takes all these datatypes that represent partially applied functions and suitable arguments and performs the actual application.

   The kind of such defunctionalized representations of type functions is

   TyFun k1 k2 -> *
   

   for various reasons (btw, a good introduction to all this is in Richard Eisenberg's blog post "Defunctionalization for the win"), whereas the kind of the corresponding "normal" type function would be

   k1 -> k2
   

   Now all higher-order type functions in singletons expect defunctionalized arguments. For example, the kind of Map is

   Map :: (TyFun k k1 -> *) -> [k] -> [k1]
   

   and not

   Map :: (k -> k1) -> [k] -> [k1]
   

   Now let's look at the functions you're working with:

   Flip :: (TyFun k (TyFun k1 k2 -> *) -> *) -> k1 -> k -> k2
   

   The first argument is a defunctionalized curried function of kind k -> k1 -> k2, and it turns this into a normal type function of kind k1 -> k -> k2.

   Also:

   ($) :: (TyFun k1 k -> *) -> k1 -> k
   

   This is just a synonym for the Apply I mentioned above.

   Now let's look at your example:

   type FooList1 b = Map ((Flip Foo) $ b) MyList  -- fails
   

   There are two problems here: First, Foo is a datatype and not a defunctionalized symbol as Flip expects. Second, Flip is a type family and expects three arguments, but only one is provided. We can fix the first problem by applying TyCon2, which takes a normal datatype and turns it into a defunctionalized symbol:

   TyCon2 :: (k -> k1 -> k2) -> TyFun k (TyFun k1 k2 -> *) -> *
   

   For the second problem, we need one of the partial applications of Flip that singletons already defines for us:

   FlipSym0 :: TyFun (TyFun k1 (TyFun k2 k -> *) -> *)
                     (TyFun k2 (TyFun k1 k -> *) -> *)
               -> *
   FlipSym1 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> TyFun k2 (TyFun k1 k -> *) -> *
   
   FlipSym2 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> k2 -> TyFun k1 k -> *
   
   Flip     ::    (TyFun k (TyFun k1 k2 -> *) -> *)
               -> k1 -> k -> k2
   

   If you look closely, then FlipSymN is the representation required if Flip is partially applied to N arguments, and Flip corresponds to the imaginary FlipSym3. In the example, Flip is applied to one argument, so the corrected example becomes

   type FooList1 b = Map ((FlipSym1 (TyCon2 Foo)) $ b) MyList
   

   And this works:

   GHCi> :kind! FooList1 Char
   FooList1 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

   The second example is similar:

   type FooList2 b = Map (($ b) :. Foo) MyList
   

   Here, we have the following problems: again, Foo must be turned into a defunctionalized symbol using TyCon2; operator sections such as $ b are not available on the type level, hence the parse error. We'll have to use Flip again, but this time FlipSym2, because we apply it to the operator $ and b. Oh, but then $ is partially applied, so we need a symbol corresponding to $ with 0 arguments. This is available as $$ in singletons (for symbolic operators, the defunctionalized symbols have appended $s). And finally, :. is also partially applied: it expects three operators, but has been given only two. So we go from :. to :.$$$ (three dollars because one dollar corresponds to 0, and three dollars correspond to 2). All in all:

   type FooList2 b = Map ((FlipSym2 ($$) b) :.$$$ TyCon2 Foo) MyList
   

   And again, this works:

   GHCi> :kind! FooList2 Char
   FooList2 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

3. I may be blind, but I don't think this is contained in singletons, which is not all that much concerned with Constraints. It's a useful function, though. It's in a library I'm currently working on. It's still unfinished and mostly undocumented, though, that's why I haven't released it yet.