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:
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 :
.
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?
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?
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.
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]
I may be blind, but I don't think this is contained in singletons, which is not all that much concerned with Constraint
s. 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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With