-
Notifications
You must be signed in to change notification settings - Fork 37
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Promote GADTs #150
Comments
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: Consider a simpler example: singletonizing kind-polymorphic
Right now (with minor modifications I introduced to preserve the kind annotation) this results in the following splice:
This almost works. The error GHC gives me is this:
Indeed, we apply
I started to ponder when it's fine to omit However, if we have 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
The only simple and consistent solution I see is to get rid of
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)? |
Yes, then we could figure out when to apply
|
For a length-indexed vector:
For higher-order kinds I don't know what to do. If we have
where |
Really, the problem here is that we don't do type inference. The
|
To help me understand better what changes would be needed here, can you help me hand-write the singled version of the @int-index suggests in #150 (comment) that the 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:
This makes sense: we're trying to claim that {-# 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:
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:
However, changing the type signature of
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
but we'll also need this:
|
Oh, I see, you're dealing with a different problem now. Sorry, the comment above talks about poly-kinded |
@RyanGlScott Your handwritten
And indeed, this works for your definition of
If you add the same constraint, |
One could think that it would be fine to remove the application of
and yeah, it compiles. However, consider a use of
if you singletonize
and |
@int-index, thanks for the advice! The 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
Also, to flesh out my polykinded
I tested my ideas in the following, and it compiles (did not import
|
Ooh, that looks really nice. Is the idea that the algorithm for coming up
And that for each data type, you'd also stub out an instance of the form:
And would you need a kind-polymorphic BTW, this design helped me find another GHC bug: Trac #13790. Isn't |
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 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
Any ideas what this means? |
This just needs more types.
worked for me. My whole file is below:
|
@goldfirere, thanks! I've updated the gist accordingly. This technique even works for poly-kinded things such as @int-index's 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 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 |
Note that the I'm note sure what your last comment refers to. |
How would you write a |
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 |
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 |
I haven't read the discussion
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 |
One thing that I realized recently is that, AFAICT, the only thing blocking |
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 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. :) |
This patch introduces an `Options` data type and an `mtl`-like `OptionsMonad` class for monads that carry `Options`. At present, the only things one can do with `Options` are: * Toggle the generation of `SingKind` instances. Suppressing `SingKind` instances provides an effective workaround for #150. * Hook into the TH machinery's naming conventions for promoted and singled names. This fixes #204. The vast majority of this patch simply adds plumbing by using `OptionsMonad` in places that need it. See the `D.S.TH.Options` module for where most of the new code is housed, as well as the `T150` and `T204` test cases for examples of how to use it.
#427 implements the workaround described in #150 (comment). |
This patch introduces an `Options` data type and an `mtl`-like `OptionsMonad` class for monads that carry `Options`. At present, the only things one can do with `Options` are: * Toggle the generation of `SingKind` instances. Suppressing `SingKind` instances provides an effective workaround for #150. * Hook into the TH machinery's naming conventions for promoted and singled names. This fixes #204. The vast majority of this patch simply adds plumbing by using `OptionsMonad` in places that need it. See the `D.S.TH.Options` module for where most of the new code is housed, as well as the `T150` and `T204` test cases for examples of how to use it.
This patch introduces an `Options` data type and an `mtl`-like `OptionsMonad` class for monads that carry `Options`. At present, the only things one can do with `Options` are: * Toggle the generation of `SingKind` instances. Suppressing `SingKind` instances provides an effective workaround for #150. * Hook into the TH machinery's naming conventions for promoted and singled names. This fixes #204. The vast majority of this patch simply adds plumbing by using `OptionsMonad` in places that need it. See the `D.S.TH.Options` module for where most of the new code is housed, as well as the `T150` and `T204` test cases for examples of how to use it.
This patch introduces an `Options` data type and an `mtl`-like `OptionsMonad` class for monads that carry `Options`. At present, the only things one can do with `Options` are: * Toggle the generation of `SingKind` instances. Suppressing `SingKind` instances provides an effective workaround for #150. * Hook into the TH machinery's naming conventions for promoted and singled names. This fixes #204. The vast majority of this patch simply adds plumbing by using `OptionsMonad` in places that need it. See the `D.S.TH.Options` module for where most of the new code is housed, as well as the `T150` and `T204` test cases for examples of how to use it.
This patch introduces an `Options` data type and an `mtl`-like `OptionsMonad` class for monads that carry `Options`. At present, the only things one can do with `Options` are: * Toggle the generation of `SingKind` instances. Suppressing `SingKind` instances provides an effective workaround for #150. * Hook into the TH machinery's naming conventions for promoted and singled names. This fixes #204. The vast majority of this patch simply adds plumbing by using `OptionsMonad` in places that need it. See the `D.S.TH.Options` module for where most of the new code is housed, as well as the `T150` and `T204` test cases for examples of how to use it.
* Bump major version to 2.7 * Introduce Options and OptionsMonad This patch introduces an `Options` data type and an `mtl`-like `OptionsMonad` class for monads that carry `Options`. At present, the only things one can do with `Options` are: * Toggle the generation of `SingKind` instances. Suppressing `SingKind` instances provides an effective workaround for #150. * Hook into the TH machinery's naming conventions for promoted and singled names. This fixes #204. The vast majority of this patch simply adds plumbing by using `OptionsMonad` in places that need it. See the `D.S.TH.Options` module for where most of the new code is housed, as well as the `T150` and `T204` test cases for examples of how to use it.
#448 poses an interesting challenge: how should {-# 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:
Can you think of a way to make these instances typecheck? |
For
At least, it type checks. Something tells me something is wrong here. But, really, this is just #82 I think. |
Interesting. Are you suggesting that in order for this to work, {-# 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 instance (SingKindX f, SingKindX g, SingKindX a) => SingKind (PProduct f g a) where
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 {-# 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 {-# 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:
This is reaffirming my belief that |
A little experimentation revealed that a problem is the overlap between |
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 |
I wanted to say 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 |
Ah, now I see. I guess this is yet another thing that |
Given inductively defined naturals
data N = Z | S N
we can define finite sets as follows:If I wrap the above definition in
singletons [d| |]
I get these errors:Instead I'd expect these definitions to be generated:
The text was updated successfully, but these errors were encountered: