Promote GADTs
int-index opened this issue · 38 comments
Given inductively defined naturals data N = Z | S N
we can define finite sets as follows:
data Fin :: N -> Type where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
If I wrap the above definition in singletons [d| |]
I get these errors:
R.hs:23:1: error:
• Expected kind ‘N’, but ‘a0’ has kind ‘*’
• In the first argument of ‘Fin’, namely ‘a_ap1v’
In the first argument of ‘SingKind’, namely ‘Fin a_ap1v’
In the instance declaration for ‘SingKind (Fin a_ap1v)’
R.hs:23:1: error:
• Expected kind ‘Fin a0’, but ‘'FS n1’ has kind ‘Fin ('S n0)’
• In the definition of data constructor ‘SFS’
In the data instance declaration for ‘Sing’
Instead I'd expect these definitions to be generated:
data instance Sing (fn :: Fin n) where
SFZ :: Sing FZ
SFS :: Sing fn -> Sing (FS fn)
instance SingKind (Fin n) where
type DemoteRep (Fin n) = Fin n
toSing = \case
FZ -> SomeSing SFZ
FS fn -> case toSing fn of
SomeSing sfn -> SomeSing (SFS sfn)
fromSing = \case
SFZ -> FZ
SFS sfn -> FS (fromSing sfn)
This would be nice, I agree. I think it's possible, too. If you describe your use cases (and what you have to write by hand to work around), that would motivate me. Thanks!
I've tackled this issue and there's a blocker: Demote
. Parameters to GADTs are often of kinds other than *
, or even kind-polymorphic, so that's what we've got to solve first.
Consider a simpler example: singletonizing kind-polymorphic Proxy
. Say I write this:
$(singletons [d|
data Prox (a :: k) = P
|])
Right now (with minor modifications I introduced to preserve the kind annotation) this results in the following splice:
data Prox_a2mSb (a_a2mSe :: k_a2mSd) = P_a2mSc
type PSym0 = P_a2mSc
data instance Sing (z_a2mSg :: Prox_a2mSb (a_a2mSe :: k_a2mSd))
= z_a2mSg ~ P_a2mSc => SP
type SProx = (Sing :: Prox_a2mSb (a_a2mSe :: k_a2mSd) -> Type)
instance SingKind (a_a2mSe :: k_a2mSd) =>
SingKind (Prox_a2mSb (a_a2mSe :: k_a2mSd)) where
type Demote (Prox_a2mSb (a_a2mSe :: k_a2mSd)) = Prox_a2mSb (Demote (a_a2mSe :: k_a2mSd))
fromSing SP = P_a2mSc
toSing P_a2mSc = SomeSing SP
instance SingI P_a2mSc where
sing = SP
This almost works. The error GHC gives me is this:
poly.hs:8:3: error:
• Expected a type, but ‘a0’ has kind ‘k0’
• In the first argument of ‘SingKind’, namely
‘(a_a2mTX :: k_a2mTW)’
In the instance declaration for
‘SingKind (Prox (a_a2mTX :: k_a2mTW))’
Indeed, we apply SingKind
and Demote
to the parameter of Prox
, but this parameter is kind-polymorphic, whereas SingKind
and Demote
expect something of kind *
. If I was to write this code by hand, I'd simply remove those:
data Prox (a :: k) = P
type PSym0 = 'P
data instance Sing (z :: Prox (a :: k)) =
z ~ 'P => SP
type SProx = (Sing :: Prox (a :: k) -> Type)
instance SingKind (Prox (a :: k)) where
fromSing SP = P
toSing P = SomeSing SP
instance SingI 'P where
sing = SP
I started to ponder when it's fine to omit SingKind
and Demote
but haven't come to a conclusion. At first glance this is possible when type parameter is phantom.
However, if we have Prox Integer
, its singletonization will be SProx (p :: Prox Integer)
instead of SProx (p :: Prox Nat)
. I can't grasp all of the consequences of this choice when it comes to nominal equality. Will it prevent singletonization of code that uses Proxy
to specify a type parameter (instead of TypeApplications
?).
And if the type variable is not phantom but nominal, this means a type family could've been applied to it, so depending on our choice to apply Demote
or not, this type family could give different results:
type family F (a :: k) :: * where
F Nat = Void
F Integer = ()
data T (a :: k) = C (F a)
The only simple and consistent solution I see is to get rid of Demote
entirely and make singletonization more parametric. That is, fromSing :: Sing (a :: k) -> k
and toSing :: k -> SomeSing k
shall not apply any transformations to the kind k
. This would require the following steps:
- make
Type
inhabited at term-level byTypeRep
to supportTypeableT
as singletons. - make
Nat
andSymbol
inhabited at term-level byNatural
andString
respectively to support singletons for type-lits. - implement ghc-proposals/ghc-proposals#52 to support singletons for functions
All of this seems far off, but worthwhile.
Thanks for looking into this, @int-index.
Here's another question for you: if you restrict yourself to GADTs which have monomorphic kinds, does the problem become easier? That is, would it be possible to single/promote a GADT like:
data Foo (a :: Type) where
MkFoo :: Foo Bool
Without some of the pain points you described in #150 (comment)?
if you restrict yourself to GADTs which have monomorphic kinds, does the problem become easier?
Yes, then we could figure out when to apply Demote
and when not to. We could apply Demote
to all parts of the type that have kind *
:
type Demote (Foo a) = Foo (Demote a) -- because `a` has kind `*`
type Demote (Fin n) = Fin n -- because `n` has kind `Nat`
For a length-indexed vector:
type Demote (Vec n a) = Vec n (Demote a)
For higher-order kinds I don't know what to do. If we have Foo :: (* -> X) -> *
, we might want to do something like this:
type Demote (Foo f) = Foo (f . Demote)
where .
denotes function composition on type level. But this would be a partial application of Demote
— not possible.
Really, the problem here is that we don't do type inference. The SingKind
constraints are necessary for every type used as a data constructor argument. I've cheated by just making constraints for all type parameters, but this isn't really right. So perhaps an improvement is to do just that: walk through all the constructors to get all the SingKind
constraints.
Demote
can be fixed by making it kind-polymorphic. This would have to remove it from the SingKind
class, but that's OK. I actually think all of this shouldn't be too bad. But I've spent out my time budget on singletons
for now...
To help me understand better what changes would be needed here, can you help me hand-write the singled version of the Foo
datatype in #150 (comment)?
@int-index suggests in #150 (comment) that the Demote
instance we'd need for Foo
is type Demote (Foo a) = Foo (Demote a)
. That's great, because that's what singletons
already tries out of the box:
singletons
[d| data Foo_a3Eb (a_a3Ed :: Type)
where MkFoo_a3Ec :: Foo_a3Eb Bool |]
======>
data Foo_a6nX (a_a6nZ :: Type) where MkFoo_a6nY :: Foo_a6nX Bool
type MkFooSym0 = MkFoo_a6nY
data instance Sing (z_a6o1 :: Foo_a6nX a_a6nZ)
= z_a6o1 ~ MkFoo_a6nY => SMkFoo
type SFoo = (Sing :: Foo_a6nX a_a6nZ -> Type)
instance SingKind a_a6nZ => SingKind (Foo_a6nX a_a6nZ) where
type Demote (Foo_a6nX a_a6nZ) = Foo_a6nX (Demote a_a6nZ)
fromSing SMkFoo = MkFoo_a6nY
toSing MkFoo_a6nY = SomeSing SMkFoo
instance SingI MkFoo_a6nY where
sing = SMkFoo
But obviously it couldn't be that easy. Here's the error that the above splice gives you:
• Expected kind ‘Foo a0’, but ‘'MkFoo’ has kind ‘Foo Bool’
• In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
This makes sense: we're trying to claim that z_a6o1 ~ MkFoo_a6nY
, but those two things have different kinds. We should be able to patch this up with heterogeneous equality:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
import Data.Singletons.Prelude
import Data.Type.Equality
data Foo (a :: Type) where MkFoo :: Foo Bool
type MkFooSym0 = MkFoo
data instance Sing (z :: Foo a)
= (z ~~ MkFoo) => SMkFoo
type SFoo = (Sing :: Foo a -> Type)
instance SingKind a => SingKind (Foo a) where
type Demote (Foo a) = Foo (Demote a)
fromSing SMkFoo = MkFoo
toSing MkFoo = SomeSing SMkFoo
instance SingI MkFoo where
sing = SMkFoo
But this leads to another error:
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:19:18: error:
• Could not deduce: a ~ Bool
from the context: Demote a ~ Bool
bound by a pattern with constructor: MkFoo :: Foo Bool,
in an equation for ‘toSing’
at Foo.hs:19:10-14
‘a’ is a rigid type variable bound by
the instance declaration at Foo.hs:16:10-39
Expected type: SomeSing (Foo a)
Actual type: SomeSing (Foo Bool)
• In the expression: SomeSing SMkFoo
In an equation for ‘toSing’: toSing MkFoo = SomeSing SMkFoo
In the instance declaration for ‘SingKind (Foo a)’
• Relevant bindings include
toSing :: Demote (Foo a) -> SomeSing (Foo a) (bound at Foo.hs:19:3)
|
19 | toSing MkFoo = SomeSing SMkFoo
| ^^^^^^^^^^^^^^^
At this point, I'm stuck. Any suggestions?
@RyanGlScott Check out my changeset here: int-index@e39178b
With it in place, I managed to compile this code:
{-# OPTIONS -ddump-splices #-}
{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeFamilies, GADTs, InstanceSigs, UndecidableInstances #-}
module Singletons.PolyKindsApp where
import Data.Singletons.TH hiding (Proxy(..))
$(singletons [d|
data Proxy (a :: k) = Proxy
pId :: Proxy (a :: k) -> Proxy (a :: k)
pId p = p
|])
However, changing the type signature of pId
to pId :: Proxy (t :: k) -> Proxy (t :: k)
(yep, just a renaming of a
to t
) exposes a GHC bug:
poly.hs:9:3: error:
• GHC internal error: ‘t_a2mVi’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [a2mVh :-> Type variable ‘k_a2mVh’ = k_a2mVh]
• In the first argument of ‘Proxy’, namely ‘(t_a2mVi :: k_a2mVh)’
In the kind ‘Proxy (t_a2mVi :: k_a2mVh)’
In the type signature:
sPId :: forall (t_a2mVv :: Proxy (t_a2mVi :: k_a2mVh)).
Sing t_a2mVv
-> Sing (Apply PIdSym0 t_a2mVv :: Proxy (t_a2mVi :: k_a2mVh))
This is a TemplateHaskell issue: inserting the generated splice by hand works! If you could help me identify what causes the trouble, I suppose the promotion of GADTs is a matter of generating more Demote
instances. By "more" I mean that now for each kind we have something like this:
type instance Demote (Nat :: Type) = Integer
but we'll also need this:
type instance Demote (n :: Nat) = n
Oh, I see, you're dealing with a different problem now. Sorry, the comment above talks about poly-kinded Demote
(what @goldfirere suggested).
@RyanGlScott Your handwritten Sing
instance for Foo
looks correct to me. My first instinct would be to add a ~ Demote a
to the instance context of SingKind
to satisfy the compiler:
instance (a ~ Demote a, SingKind a) => SingKind (Foo a) where
And indeed, this works for your definition of Foo
. However, consider singletonization of a GADT like this:
data Quux (a :: Type) where
MkFoo :: Quux Integer
MkBar :: Quux Nat
If you add the same constraint, MkBar
won't be accessible. Maybe Demote
is a blocker after all :(
One could think that it would be fine to remove the application of Demote
to the parameter of Quux
altogether:
{-# OPTIONS -ddump-splices #-}
{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeFamilies, GADTs, InstanceSigs, UndecidableInstances #-}
module Singletons.Foo where
import Data.Kind
import Data.Singletons.TypeLits
import Data.Singletons.Prelude
import Data.Singletons.TH
data Quux (a :: Type) where
MkFoo :: Quux Integer
MkBar :: Quux Nat
data instance Sing (z :: Quux a) where
SMkFoo :: Sing (MkFoo :: Quux Integer)
SMkBar :: Sing (MkBar :: Quux Nat)
type SQuux = (Sing :: Quux a -> Type)
type instance Demote (Quux a) = Quux a
instance (SingKind a) => SingKind (Quux a) where
fromSing = \case
SMkFoo -> MkFoo
SMkBar -> MkBar
toSing = \case
MkFoo -> SomeSing (SMkFoo :: Sing (MkFoo :: Quux Integer))
MkBar -> SomeSing (SMkBar :: Sing (MkBar :: Quux Nat))
instance SingI MkFoo where
sing = SMkFoo
instance SingI MkBar where
sing = SMkBar
and yeah, it compiles. However, consider a use of Foo
like this:
data QSigma (a :: Type) where
QSigma :: Quux a -> a -> QSigma a
if you singletonize QSigma
, you get this definition:
data instance Sing (z :: QSigma a) where
SQSigma :: Sing (t :: Quux a) -> Sing (p :: a) -> Sing (z :: QSigma a)
and SomeSing (QSigma a)
is not isomorphic to QSigma a
! Notice that Sing (p :: a)
is inhabited for a ~ Nat
, whereas Nat
itself isn't. QSigma MkBar
can have only bottom as its second field, but SQSigma SMkBar
can have any integer (e.g. sing :: Sing 42
).
@int-index, thanks for the advice! The Demote a ~ a
trick is interesting, I'll have to give that more thought.
Also, great job at finding the bug in #150 (comment). I've reported this as GHC Trac #13782.
It looks like we need an inverse of Demote
:
type family Promote k :: Type
class (Promote (Demote k) ~ k) => SingKind (k :: Type) where ...
Also, to flesh out my polykinded Demote
idea:
type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a
type instance Promote Type = Type
instance SingKind Type where
type Demote Type = Type
fromSing = error "fromSing Type"
toSing = error "toSing Type"
I tested my ideas in the following, and it compiles (did not import Data.Singletons
):
data family Sing (a :: k)
class SingI (a :: k) where
sing :: Sing a
data SomeSing (k :: Type) where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote k :: Type
class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data instance Sing (b :: Bool) where
SFalse :: Sing False
STrue :: Sing True
instance SingI True where
sing = STrue
instance SingI False where
sing = SFalse
type instance Promote Bool = Bool
instance SingKind Bool where
type Demote Bool = Bool
fromSing STrue = True
fromSing SFalse = False
toSing True = SomeSing STrue
toSing False = SomeSing SFalse
type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a
type instance Promote Type = Type
instance SingKind Type where
type Demote Type = Type
fromSing = error "fromSing Type"
toSing = error "toSing Type"
data Foo (a :: Type) where MkFoo :: Foo Bool
type MkFooSym0 = MkFoo
data instance Sing (z :: Foo a)
= (z ~~ MkFoo) => SMkFoo
type SFoo = (Sing :: Foo a -> Type)
type instance Promote (Foo a) = Foo (Promote a)
instance SingKind a => SingKind (Foo a) where
type Demote (Foo a) = Foo (Demote a)
fromSing SMkFoo = MkFoo
toSing MkFoo = SomeSing SMkFoo
instance SingI MkFoo where
sing = SMkFoo
Ooh, that looks really nice. Is the idea that the algorithm for coming up Demote
instances would now become:
type Demote (T a1 ... an) = T (DemoteX a1) ... (DemoteX an)
And that for each data type, you'd also stub out an instance of the form:
type instance DemoteX (t :: T a1 ... an) = t
And would you need a kind-polymorphic PromoteX
type family as well, with similarly stubbed out instances?
BTW, this design helped me find another GHC bug: Trac #13790. Isn't singletons
great? :)
DemoteX
and PromoteX
(yes, we'll need that too, I suppose) should be fully recursive everywhere. This means not using the "stubbed out" instances Ryan has proposed, but instead to recur on all arguments of data constructors.
I think.
Interesting! Using this approach, I was able to create singletons for every GADT discussed in this thread (see this gist).
...well, almost. I cheated when I got to Fin
and Vec
, since the type parameters of kind N
gave me trouble. Here's the code I have for Fin
, for instance:
data Fin :: N -> Type where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
data instance Sing (z :: Fin n) where
SFZ :: Sing FZ
SFS :: Sing fn -> Sing (FS fn)
type instance Demote (Fin n) = Fin n -- Fin (DemoteX n)
type instance Promote (Fin n) = Fin n -- Fin (PromoteX n)
instance SingKind (Fin n) where
fromSing SFZ = FZ
fromSing (SFS sfn) = FS (fromSing sfn)
toSing FZ = SomeSing SFZ
toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')
$(return [])
type instance DemoteX FZ = FZ
type instance DemoteX (FS n) = FS (DemoteX n)
type instance PromoteX FZ = FZ
type instance PromoteX (FS n) = FS (PromoteX n)
instance SingI FZ where
sing = SFZ
instance SingI fn => SingI (FS fn) where
sing = SFS sing
Notice that the definitions that the algorithm would have came up with for Demote
and Promote
are commented out, because if you use them, you get some perplexing errors:
GADTSingletons.hs:324:10: error:
• Couldn't match type ‘PromoteX (DemoteX n)’ with ‘n’
arising from the superclasses of an instance declaration
• In the instance declaration for ‘SingKind (Fin n)’
|
324 | instance SingKind (Fin n) where
| ^^^^^^^^^^^^^^^^
GADTSingletons.hs:328:15: error:
• Could not deduce: n ~ 'S n0
from the context: DemoteX n ~ 'S n2
bound by a pattern with constructor:
FZ :: forall (n :: N). Fin ('S n),
in an equation for ‘toSing’
at GADTSingletons.hs:328:10-11
‘n’ is a rigid type variable bound by
the instance declaration at GADTSingletons.hs:324:10-25
Expected type: SomeSing (Fin n)
Actual type: SomeSing (Fin ('S n0))
• In the expression: SomeSing SFZ
In an equation for ‘toSing’: toSing FZ = SomeSing SFZ
In the instance declaration for ‘SingKind (Fin n)’
• Relevant bindings include
toSing :: Demote (Fin n) -> SomeSing (Fin n)
(bound at GADTSingletons.hs:328:3)
|
328 | toSing FZ = SomeSing SFZ
| ^^^^^^^^^^^^
GADTSingletons.hs:329:33: error:
• Could not deduce: DemoteX n1 ~ n2
from the context: DemoteX n ~ 'S n2
bound by a pattern with constructor:
FS :: forall (n :: N). Fin n -> Fin ('S n),
in an equation for ‘toSing’
at GADTSingletons.hs:329:11-15
Expected type: Demote (Fin n1)
Actual type: Fin n2
The type variable ‘n1’ is ambiguous
• In the first argument of ‘withSomeSing’, namely ‘fn’
In the expression: withSomeSing fn (\ fn' -> SomeSing $ SFS fn')
In an equation for ‘toSing’:
toSing (FS fn) = withSomeSing fn (\ fn' -> SomeSing $ SFS fn')
• Relevant bindings include
fn :: Fin n2 (bound at GADTSingletons.hs:329:14)
|
329 | toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')
| ^^
GADTSingletons.hs:329:45: error:
• Could not deduce: n ~ 'S n1
from the context: DemoteX n ~ 'S n2
bound by a pattern with constructor:
FS :: forall (n :: N). Fin n -> Fin ('S n),
in an equation for ‘toSing’
at GADTSingletons.hs:329:11-15
‘n’ is a rigid type variable bound by
the instance declaration at GADTSingletons.hs:324:10-25
Expected type: SomeSing (Fin n)
Actual type: SomeSing (Fin ('S n1))
• In the expression: SomeSing $ SFS fn'
In the second argument of ‘withSomeSing’, namely
‘(\ fn' -> SomeSing $ SFS fn')’
In the expression: withSomeSing fn (\ fn' -> SomeSing $ SFS fn')
• Relevant bindings include
fn' :: Sing a (bound at GADTSingletons.hs:329:38)
toSing :: Demote (Fin n) -> SomeSing (Fin n)
(bound at GADTSingletons.hs:328:3)
|
329 | toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')
| ^^^^^^^^^^^^^^^^^^
Any ideas what this means?
This just needs more types.
type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a) -- hetero is important; otherwise, GHC can't be sure that the kinds respect the Promote/Demote property
instance SingKindX n => SingKind (Fin n) where ...
worked for me.
My whole file is below:
data N = Z | S N
data instance Sing (a :: N) where
SZ :: Sing Z
SS :: Sing n -> Sing (S n)
data family Sing (a :: k)
class SingI (a :: k) where
sing :: Sing a
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing x k
= case toSing x of
SomeSing sx -> k sx
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
type instance PromoteX (k :: Type) = Promote k
type instance DemoteX (k :: Type) = Demote k
type instance Demote Type = Type
type instance Promote Type = Type
class SingKindX k => SingKind k where
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
type instance Promote N = N
type instance Demote N = N
type instance PromoteX Z = Z
type instance PromoteX (S n) = S (PromoteX n)
type instance DemoteX Z = Z
type instance DemoteX (S n) = S (DemoteX n)
instance SingKind N where
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = withSomeSing n $ \sn -> SomeSing (SS sn)
data Fin :: N -> Type where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
data instance Sing (z :: Fin n) where
SFZ :: Sing FZ
SFS :: Sing fn -> Sing (FS fn)
type instance Promote (Fin n) = Fin (PromoteX n)
type instance Demote (Fin n) = Fin (DemoteX n)
type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a)
instance SingKindX n => SingKind (Fin n) where
fromSing SFZ = FZ
fromSing (SFS sfn) = FS (fromSing sfn)
toSing FZ = SomeSing SFZ
toSing (FS fn) = withSomeSing fn (\fn' -> SomeSing $ SFS fn')
$(return [])
type instance DemoteX FZ = FZ
type instance DemoteX (FS n) = FS (DemoteX n)
type instance PromoteX FZ = FZ
type instance PromoteX (FS n) = FS (PromoteX n)
instance SingI FZ where
sing = SFZ
instance SingI fn => SingI (FS fn) where
sing = SFS sing
@goldfirere, thanks! I've updated the gist accordingly. This technique even works for poly-kinded things such as @int-index's Prox
in #150 (comment).
This. Is. Awesome.
The only thing I couldn't figure out how to do was function kinds like @int-index alluded to in #150 (comment). I figure that we'll probably need Demote
and Promote
instances like this:
type instance Demote (k1 ~> k2) = Demote k1 -> Demote k2
type instance Promote (k1 -> k2) = Promote k1 ~> Promote k2
I then tried coming up with suitable DemoteX
and PromoteX
instances for SLambda
, but I quickly got stuck...
Note that the Demote
instance above is already here.
I'm note sure what your last comment refers to.
I'm note sure what your last comment refers to.
How would you write a DemoteX
instance for something of kind Demote k1 ~> Demote k2
?
Ah -- now I understand. You wouldn't. :)
Maybe once #82 is done a way forward will present itself. But perhaps not.
Even without promoting/demoting SLambda
, this is still quite useful, no?
Even without promoting/demoting
SLambda
, this is still quite useful, no?
Certainly! I was just wondering if it was possible to cleanly singletonize arrow-kinded things like in #150 (comment) (I have a use case for this involving GHC.Generics
, which has a lot of datatypes with parameters of kind * -> *
), but as you say, it would probably require fixing #82 to accomplish that.
I haven't read the discussion
I've tackled this issue and there's a blocker:
Demote
. Parameters to GADTs are often of kinds other than*
, or even kind-polymorphic, so that's what we've got to solve first.
We have https://ghc.haskell.org/trac/ghc/ticket/12369 now, edit I don't think this is relevant, nvm
Ah, blast. The poly-kinded example in #150 (comment) no longer works in GHC 8.4 due to Trac #14441.
EDIT: And now it's fixed in GHC 8.6! Never mind.
If you want to try out the design in #150 (comment) more, I have a singleton-gadts
package (not yet released on Hackage) with Template Haskell functionality to quickly generate the boilerplatey parts. (I wouldn't advocate merging this into singletons
proper yet due to the unsightly workarounds one has to employ to avoid Trac #12088.)
One thing that I realized recently is that, AFAICT, the only thing blocking singletons
from being able to handle GADTs at the moment is SingKind
. Perhaps we don't have to let this SingKind
issue block us from being able to other useful things with GADTs. I'm envisioning some sort of option (in the style of #204) that makes singletons
/genSingletons
/etc. generate all of the code it normally does except for SingKind
instances.
Unless there's a crying need, I would personally hold off. Things seem to be getting closer and closer to fixing GHC's dreaded #12088, so perhaps the extra work needed to suppress the instances will be wasted.
Even if we possessed the ability to define and use SingKind
as described in this issue, I'm still skeptical that singletons
' TH machinery will generate the desired instances 100% of the time. As one data point in support of this claim, someone filed an issue because the generated instance put a SingKind
constraint on a phantom type, which is questionable. (There are other various corner cases that I could cite, although I'll leave it at that for now.)
At the end of the day, I think it would be nice to give power users the ability to tweak this. It would certainly save me from having to write a lot of code, at least, and #348 suggests that others would save as well.
OK. Don't let me stand in your way. :)
#427 implements the workaround described in #150 (comment).
#448 poses an interesting challenge: how should SingKind
handle Data.Functor.Product
? I started out with a simple attempt at defining Promote
/Demote
instances for it:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where
import Data.Functor.Product
import Data.Kind
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type instance Promote Type = Type
type instance Demote Type = Type
type instance Promote (a -> b) = PromoteX a ~> PromoteX b
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
type instance PromoteX (k :: Type) = Promote k
type instance DemoteX (k :: Type) = Demote k
$(pure [])
type instance Promote (Product f g a) = Product (PromoteX f) (PromoteX g) (PromoteX a)
type instance Demote (Product f g a) = Demote (DemoteX f) (DemoteX g) (DemoteX a)
However, that doesn't work:
$ /opt/ghc/8.10.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o, Foo.dyn_o )
Foo.hs:32:76: error:
• Expected kind ‘TyFun (Promote k0) *’,
but ‘PromoteX a’ has kind ‘Promote k0’
• In the third argument of ‘Product’, namely ‘(PromoteX a)’
In the type ‘Product (PromoteX f) (PromoteX g) (PromoteX a)’
In the type instance declaration for ‘Promote’
|
32 | type instance Promote (Product f g a) = Product (PromoteX f) (PromoteX g) (PromoteX a)
| ^^^^^^^^^^
Foo.hs:33:41: error:
• Expected kind ‘* -> Demote k0 -> *’,
but ‘Demote (DemoteX f)’ has kind ‘*’
• In the type ‘Demote (DemoteX f) (DemoteX g) (DemoteX a)’
In the type instance declaration for ‘Demote’
|
33 | type instance Demote (Product f g a) = Demote (DemoteX f) (DemoteX g) (DemoteX a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Can you think of a way to make these instances typecheck?
For Promote
, this works:
type instance Promote (Product f g a) = Product (PromoteX f) (PromoteX g) @@ (PromoteX a)
At least, it type checks. Something tells me something is wrong here. But, really, this is just #82 I think.
But, really, this is just #82 I think.
Interesting. Are you suggesting that in order for this to work, Product
needs to be able to switch between (~>)
and (->)
depending on whether it's promoted or not? Following that idea, I was able to write instances of Promote
and Demote
successfully:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where
import Data.Kind
import Data.Type.Equality
type Sing :: k -> Type
type family Sing
type SomeSing :: Type -> Type
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
type Promote :: Type -> Type
type family Promote k
type PromoteX :: k -> Promote k
type family PromoteX a
type Demote :: Type -> Type
type family Demote k
type DemoteX :: k -> Demote k
type family DemoteX a
type SingKindX :: k -> Constraint
type SingKindX a = PromoteX (DemoteX a) ~~ a
type SingKind :: Type -> Constraint
class SingKindX k => SingKind k where
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
withSomeSing :: forall k r
. SingKind k
=> Demote k
-> (forall (a :: k). Sing a -> r)
-> r
withSomeSing x f =
case toSing x of
SomeSing x' -> f x'
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type (@@) :: (a ~> b) -> a -> b
type f @@ x = Apply f x
infixl 9 @@
type instance Promote Type = Type
type instance Demote Type = Type
type instance Promote (a -> b) = PromoteX a ~> PromoteX b
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
type instance PromoteX (k :: Type) = Promote k
type instance DemoteX (k :: Type) = Demote k
data TyCon1 :: (a -> b) -> (a ~> b)
type instance Apply (TyCon1 f) x = f x
data TyCon2 :: (a -> b -> c) -> (a ~> b ~> c)
type instance Apply (TyCon2 f) x = TyCon1 (f x)
type TyConApp :: (a -> b) -> a -> b
type family TyConApp f where
TyConApp f = f
type TyConAppSym0 :: (a -> b) ~> a ~> b
data TyConAppSym0 f
type instance Apply TyConAppSym0 f = TyConAppSym1 f
type TyConAppSym1 :: (a -> b) -> a ~> b
data TyConAppSym1 f x
type instance Apply (TyConAppSym1 f) x = TyConApp f x
type (~>@#@$) :: Type ~> Type ~> Type
data (~>@#@$) a
type instance Apply (~>@#@$) a = (~>@#@$$) a
type (~>@#@$$) :: Type -> Type ~> Type
data (~>@#@$$) a b
type instance Apply ((~>@#@$$) a) b = a ~> b
type ApplySym0 :: (a ~> b) ~> a ~> b
data ApplySym0 f
type instance Apply ApplySym0 f = ApplySym1 f
type ApplySym1 :: (a ~> b) -> a ~> b
data ApplySym1 f x
type instance Apply (ApplySym1 f) x = Apply f x
type Product' :: forall k.
forall (arr :: Type ~> Type ~> Type)
(app :: arr @@ k @@ Type ~> k ~> Type)
-> arr @@ k @@ Type -> arr @@ k @@ Type -> k -> Type
data Product' arr app f g a = Pair (app @@ f @@ a) (app @@ g @@ a)
type Product = Product' (TyCon2 (->)) TyConAppSym0
type PProduct = Product' (~>@#@$) ApplySym0
type SProduct :: PProduct f g a -> Type
data SProduct p where
SPair :: Sing fa -> Sing ga -> SProduct (Pair fa ga)
type instance Sing = SProduct
$(pure [])
type instance Promote (Product f g a) = PProduct (PromoteX f) (PromoteX g) (PromoteX a)
type instance Demote (PProduct f g a) = Product (DemoteX f) (DemoteX g) (DemoteX a)
However, I get stuck when trying to define the SingKind
instance:
instance (SingKindX f, SingKindX g, SingKindX a) => SingKind (PProduct f g a) where
fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
$ /opt/ghc/8.10.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o, Foo.dyn_o )
Foo.hs:125:36: error:
• Could not deduce: Demote (Apply f a) ~ DemoteX f (DemoteX a)
from the context: (SingKindX f, SingKindX g, SingKindX a)
bound by the instance declaration at Foo.hs:124:10-77
or from: a1 ~ 'Pair fa ga
bound by a pattern with constructor:
SPair :: forall k (f :: k ~> *) (a :: k) (g :: k ~> *)
(fa :: Apply f a) (ga :: Apply g a).
Sing fa -> Sing ga -> SProduct ('Pair fa ga),
in an equation for ‘fromSing’
at Foo.hs:125:13-25
Expected type: (TyConAppSym0 @@ DemoteX f) @@ DemoteX a
Actual type: Demote (Apply f a)
• In the first argument of ‘Pair’, namely ‘(fromSing sfa)’
In the expression: Pair (fromSing sfa) (fromSing sga)
In an equation for ‘fromSing’:
fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
• Relevant bindings include
sga :: Sing ga (bound at Foo.hs:125:23)
sfa :: Sing fa (bound at Foo.hs:125:19)
fromSing :: Sing a1 -> Demote (PProduct f g a)
(bound at Foo.hs:125:3)
|
125 | fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
| ^^^^^^^^^^^^
Foo.hs:125:51: error:
• Could not deduce: Demote (Apply g a) ~ DemoteX g (DemoteX a)
from the context: (SingKindX f, SingKindX g, SingKindX a)
bound by the instance declaration at Foo.hs:124:10-77
or from: a1 ~ 'Pair fa ga
bound by a pattern with constructor:
SPair :: forall k (f :: k ~> *) (a :: k) (g :: k ~> *)
(fa :: Apply f a) (ga :: Apply g a).
Sing fa -> Sing ga -> SProduct ('Pair fa ga),
in an equation for ‘fromSing’
at Foo.hs:125:13-25
Expected type: (TyConAppSym0 @@ DemoteX g) @@ DemoteX a
Actual type: Demote (Apply g a)
• In the second argument of ‘Pair’, namely ‘(fromSing sga)’
In the expression: Pair (fromSing sfa) (fromSing sga)
In an equation for ‘fromSing’:
fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
• Relevant bindings include
sga :: Sing ga (bound at Foo.hs:125:23)
sfa :: Sing fa (bound at Foo.hs:125:19)
fromSing :: Sing a1 -> Demote (PProduct f g a)
(bound at Foo.hs:125:3)
|
125 | fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
| ^^^^^^^^^^^^
Any ideas?
Please disregard #150 (comment). It is based on the false premise that we need separate Product
(term-level) and PProduct
(type-level) types. In reality, we don't need to vary the arrows, but rather whether the fields are demoted or not. Here is a version of Product
that can be given a SingKind
instance:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where
import Data.Kind
import Data.Type.Equality
type family Sing :: k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a)
class SingKindX k => SingKind k where
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing x k
= case toSing x of
SomeSing sx -> k sx
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type instance Demote Type = Type
type instance Promote Type = Type
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
type instance Promote (a -> b) = PromoteX a ~> PromoteX b
type instance DemoteX (k :: Type) = Demote k
type instance PromoteX (k :: Type) = Promote k
data Product f g a = Pair (f a) (g a)
data DemotedProduct f g a = DemotedPair (Demote (f a)) (Demote (g a))
data SProduct :: forall f g a. Product f g a -> Type where
SPair :: Sing fa -> Sing ga -> SProduct (Pair fa ga)
type instance Sing = SProduct
type instance Demote (Product f g a) = DemotedProduct f g a
type instance Promote (DemotedProduct f g a) = Product f g a
instance (SingKind (f a), SingKind (g a)) => SingKind (Product f g a) where
fromSing (SPair sfa sga) = DemotedPair (fromSing sfa) (fromSing sga)
toSing (DemotedPair fa ga) =
withSomeSing fa $ \sfa ->
withSomeSing ga $ \sga ->
SomeSing (SPair sfa sga)
Or, if you don't want Product
and DemotedProduct
to be separate data types, you can do this:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where
import Data.Kind
import Data.Type.Equality
import Unsafe.Coerce
type family Sing :: k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
data DemoteSym0 :: Type ~> Type
type instance Apply DemoteSym0 x = Demote x
type SingKindX a = PromoteX (DemoteX a) ~~ a
class SingKindX k => SingKind k where
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing x k
= case toSing x of
SomeSing sx -> k sx
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type f @@ x = Apply f x
type instance Demote Type = Type
type instance Promote Type = Type
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
type instance Promote (a -> b) = PromoteX a ~> PromoteX b
type instance DemoteX (k :: Type) = Demote k
type instance PromoteX (k :: Type) = Promote k
type family Id (x :: a) :: a where
Id x = x
data IdSym0 :: a ~> a
type instance Apply IdSym0 x = Id x
data Product' (p :: Type ~> Type) f g a = Pair (p @@ f a) (p @@ g a)
type Product = Product' IdSym0
type DemotedProduct = Product' DemoteSym0
data SProduct :: forall f g a. Product f g a -> Type where
SPair :: Sing fa -> Sing ga -> SProduct (Pair fa ga)
type instance Sing = SProduct
type instance Demote (Product f g a) = DemotedProduct f g a
type instance Promote (DemotedProduct f g a) = Product f g a
instance (SingKind (f a), SingKind (g a)) => SingKind (Product f g a) where
fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
toSing (Pair fa ga) = withSomeSing fa $ \sfa ->
withSomeSing ga $ \sga ->
SomeSing (SPair sfa sga)
Neither version is quite satisfying for two reasons:
- You can't define
PromoteX
orDemoteX
instances forPair
. I'm starting to believe that this is a fundamental limitation ofPromoteX
andDemoteX
, since you can't define instances of them for(n :: Nat)
,(s :: Symbol)
, or(f :: a ~> b)
either. - Neither version is able to simply use
Product
fromData.Functor.Product
everywhere. In the former version, you have to define a separateDemotedProduct
data type alongsideData.Functor.Product.Product
in order to make theSingKind
instance work, and in the latter version, you don't useData.Functor.Product.Product
at all. This means that this version ofSingKind
wouldn't be a solution for #448.
This is reaffirming my belief that SingKind
is fundamentally limited in what in can express. This version of SingKind
can define instances for more things than the current version, yes, but it's far from perfect.
A little experimentation revealed that a problem is the overlap between TyFun a b -> Type
(that is, a ~> b
) and a -> b
. Maybe if there were an encoding of a ~> b
that was apart from a -> b
, we would be in better shape. But I'm not feeling particularly creative around that at the moment...
A little experimentation revealed that a problem is the overlap between
TyFun a b -> Type
(that is,a ~> b
) anda -> b
.
That sounds like an interesting experiment, although it's unclear to me what steps led to to that conclusion. Do you mind providing some more details on what you tried? I have also wondered if a different encoding of a ~> b
would be worthwhile (since you cannot partially apply (~>)
currently), and this seems to add another argument in favor of that.
I wanted to say Demote (a -> b) = Demote a -> Demote b
. But that overlapped. So I wrote
type family DemoteArrow a b where
DemoteArrow (TyFun a b) Type = Demote a -> Demote b
DemoteArrow a b = Demote a -> Demote b
type instance Demote (a -> b) = DemoteArrow a b
but then Demote (k0 -> Type)
is stuck. :(
Ah, now I see. I guess this is yet another thing that UnsaturatedTypeFamilies
would make easier, since (~>)
would become a distinct entity from (->)
.