There's currently this line in Data.Singletons.Promote:
|
-- Until we get visible kind applications, this is the best we can do. |
|
promoteExp (DAppTypeE exp _) = do |
|
qReportWarning "Visible type applications are ignored by `singletons`." |
|
promoteExp exp |
Darn, if only we had visible kind applications! But hey, we're getting just that in GHC 8.8! Surely this means that we can rip out this antiquated code and treat visible type applications as a first-class citizen in singletons...
...but not so fast. It turns out that having visible kind applications isn't enough—we also need to figure out how to use it properly. Here's a function to help illustrate some of the challenges that VTA presents:
constBA :: forall b a. a -> b -> a
constBA x _ = x
constBA is exactly the same as the familiar const function, except I've deliberately swapped the conventional order that the type variables are quantified in. One interesting observation, right off the bat, is that when constBA is promoted to a type family:
type family ConstBA (x :: a) (y :: b) :: a where ...
The kind of ConstBA is now forall a b. a -> b -> a, not forall b a. a -> b -> a! What's worse, there is no reliable way of swapping the order that a and b are quantified in until we get top-level kind signatures. Blast.
But that's far from the only sticky thing about this situation. Let's suppose you want to use constBA, like in the following function:
blah :: forall b a. [a] -> [b -> a]
blah x = map (constBA @b) x
How should this promote? This is what currently happens in today's singletons, which simply drops VTAs:
type family Blah (x :: [a]) :: [b ~> a] where
Blah x = Apply (Apply MapSym0 ConstBASym0) x
Notice that singletons always uses defunctionalization symbols when promoting function application, so if we want to promote constBA @b, this suggests that the output should be something like ConstBASym0 @b. But that presents its own set of challenges, because this is the code that gets generated for ConstBASym0:
data ConstBASym0 :: forall a b. a ~> b ~> a
This happens because during defunctionalization, we take the type a ~> b ~> a and quantify over it by simply gathering the free variables in left-to-right order. Unfortunately, this means that we get forall a b. <...> instead of forall b a. <...>. Double blast.
One could envision tweaking defunctionalization to remember the original order of type variables so that we generate data ConstBASym0 :: forall b a. a ~> b ~> a instead. That would fix blah, but we're not out of the clear yet. There's one more defunctionalization symbol to consider: ConstBASym1, which arises from this generated code:
data ConstSym1 (x :: a) :: forall b. b ~> a
This is even gnarlier than ConstSym0. The kind of ConstSym1 is forall a. a -> forall b. b ~> a, and this time, it's not simple to rearrange the foralls so that b is quantified before a due to the syntax used. One way forward is to declare ConstSym1 like so:
data ConstSym1 :: forall b a. a -> (b ~> a)
This works, although this trick currently won't work for anything that involves visible dependent quantification. (We could carve out a special case when defunctionalizing things without visible dependent quantification, although that would be a bit messy.)
By sheer accident, constBA is singled correctly... at least, some of the time. That is to say, this is generated for sConstBA:
sConstBA :: forall b_1 a_2 (x :: a_2) (y :: b_1). Sing x -> Sing y -> Sing (Apply (Apply ConstBASym0 x) y :: a_2)
This works only because b_1's unique happens to come before a_2's unique, so b_1 comes before a_2 when they're both put into a Set. (If compiled with -dunique-increment=-1, however, then you'd get the opposite order!)
That's not to say that singling VTAs is already a solved problem. Consider what happens when you single blah today:
sBlah :: forall b a (x :: [a]). Sing x -> Sing (Apply BlahSym0 x :: [b ~> a])
sBlah (sX :: Sing x) = (applySing ((applySing ((singFun2 @MapSym0) sMap)) ((singFun2 @ConstBASym0) sConstBA))) sX
Once again, we single function application by leveraging defunctionalization symbols. Therefore, in order to single blah correctly, we'd need to change singFun2 @ConstBASym0 to singFun2 @(ConstBASym0 @b), and moreover, we'd need to ensure that ConstBASym0 :: forall b a. a ~> b ~> a.
There's currently this line in
Data.Singletons.Promote:singletons/src/Data/Singletons/Promote.hs
Lines 762 to 765 in fb5e005
Darn, if only we had visible kind applications! But hey, we're getting just that in GHC 8.8! Surely this means that we can rip out this antiquated code and treat visible type applications as a first-class citizen in
singletons......but not so fast. It turns out that having visible kind applications isn't enough—we also need to figure out how to use it properly. Here's a function to help illustrate some of the challenges that VTA presents:
constBAis exactly the same as the familiarconstfunction, except I've deliberately swapped the conventional order that the type variables are quantified in. One interesting observation, right off the bat, is that whenconstBAis promoted to a type family:The kind of
ConstBAis nowforall a b. a -> b -> a, notforall b a. a -> b -> a! What's worse, there is no reliable way of swapping the order thataandbare quantified in until we get top-level kind signatures. Blast.But that's far from the only sticky thing about this situation. Let's suppose you want to use
constBA, like in the following function:How should this promote? This is what currently happens in today's
singletons, which simply drops VTAs:Notice that
singletonsalways uses defunctionalization symbols when promoting function application, so if we want to promoteconstBA @b, this suggests that the output should be something likeConstBASym0 @b. But that presents its own set of challenges, because this is the code that gets generated forConstBASym0:This happens because during defunctionalization, we take the type
a ~> b ~> aand quantify over it by simply gathering the free variables in left-to-right order. Unfortunately, this means that we getforall a b. <...>instead offorall b a. <...>. Double blast.One could envision tweaking defunctionalization to remember the original order of type variables so that we generate
data ConstBASym0 :: forall b a. a ~> b ~> ainstead. That would fixblah, but we're not out of the clear yet. There's one more defunctionalization symbol to consider:ConstBASym1, which arises from this generated code:This is even gnarlier than
ConstSym0. The kind ofConstSym1isforall a. a -> forall b. b ~> a, and this time, it's not simple to rearrange theforalls so thatbis quantified beforeadue to the syntax used. One way forward is to declareConstSym1like so:This works, although this trick currently won't work for anything that involves visible dependent quantification. (We could carve out a special case when defunctionalizing things without visible dependent quantification, although that would be a bit messy.)
By sheer accident,
constBAis singled correctly... at least, some of the time. That is to say, this is generated forsConstBA:This works only because
b_1's unique happens to come beforea_2's unique, sob_1comes beforea_2when they're both put into aSet. (If compiled with-dunique-increment=-1, however, then you'd get the opposite order!)That's not to say that singling VTAs is already a solved problem. Consider what happens when you single
blahtoday:Once again, we single function application by leveraging defunctionalization symbols. Therefore, in order to single
blahcorrectly, we'd need to changesingFun2 @ConstBASym0tosingFun2 @(ConstBASym0 @b), and moreover, we'd need to ensure thatConstBASym0 :: forall b a. a ~> b ~> a.