[GHC] #13179: Levity-polymorphic data types
#13179: Levity-polymorphic data types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Core | Version: 8.0.1 Libraries | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #12708 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I don't know if this belongs as a part of [https://github.com/ghc- proposals/ghc-proposals/pull/30 levity-polymorphic type classes] (#12708) but many data types can be made levity-polymorphic, some have just been added to base: {{{#!hs -- Sum Array# Array# :: Type -> Type data Product :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where Pair :: f a -> g a -> (Product f g) a -- Sum Array# Array# :: Type -> Type data Sum :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where InL :: f a -> (Sum f g) a InR :: g a -> (Sum f g) a -- Compose Array# [] :: Type -> Type data Compose :: forall rep. (b -> TYPE rep) -> (a -> b) -> (a -> Type) where Compose :: f (g a) -> (Compose f g) a }}} Can you think of other examples? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13179 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13179: Levity-polymorphic data types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12708 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -7,2 +7,1 @@ - - -- Sum Array# Array# :: Type -> Type + -- Product Array# Array# :: Type -> Type New description: I don't know if this belongs as a part of [https://github.com/ghc- proposals/ghc-proposals/pull/30 levity-polymorphic type classes] (#12708) but many data types can be made levity-polymorphic, some have just been added to base: {{{#!hs -- Product Array# Array# :: Type -> Type data Product :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where Pair :: f a -> g a -> (Product f g) a -- Sum Array# Array# :: Type -> Type data Sum :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where InL :: f a -> (Sum f g) a InR :: g a -> (Sum f g) a -- Compose Array# [] :: Type -> Type data Compose :: forall rep. (b -> TYPE rep) -> (a -> b) -> (a -> Type) where Compose :: f (g a) -> (Compose f g) a }}} Can you think of other examples? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13179#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13179: Levity-polymorphic data types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12708 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm afraid your definitions may not be what you think they are. In particular, the way you've written your GADT constructors forces `TYPE rep ~ Type`, so in effect they're not much different from `Product`, `Sum`, and `Compose` and they exist today in `base`. If you tried to write truly levity polymorphic definitions for, say, `Product`, it'll actually be rejected! {{{#!hs data Product :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where Pair :: forall rep k (f :: k -> TYPE rep) (g :: k -> TYPE rep) (a :: k). f a -> g a -> (Product f g) a }}} {{{ <interactive>:9:85: error: • A levity-polymorphic type is not allowed here: Type: f a Kind: TYPE rep • In the definition of data constructor ‘Pair’ In the data type declaration for ‘Product’ <interactive>:9:85: error: • A levity-polymorphic type is not allowed here: Type: g a Kind: TYPE rep • In the definition of data constructor ‘Pair’ In the data type declaration for ‘Product’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13179#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13179: Levity-polymorphic data types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12708 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:2 RyanGlScott]:
I'm afraid your definitions may not be what you think they are.
Yes. GHC will do levity polymorphism only upon request, and there is no request in your data constructor types.
If you tried to write truly levity polymorphic definitions for, say, `Product`, it'll actually be rejected!
As well they should be. When creating data constructors, we need to know representations of their fields. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13179#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13179: Levity-polymorphic data types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12708 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:2 RyanGlScott]:
I'm afraid your definitions may not be what you think they are.
Fiddlesticks, I was worried something like this was happening. Replying to [comment:3 goldfire]:
As well they should be. When creating data constructors, we need to know representations of their fields.
, could something like this work (possibly with UnliftedDataTypes) {{{#!hs Product :: forall rep₁ rep₂. (k -> TYPE rep₁) -> (k -> TYPE rep₂) -> (k -> TYPE (rep₁ <> rep₂)) }}} for some handwavey `Max` {{{#!hs Sum :: forall rep₁ rep₂. (k -> TYPE rep₁) -> (k -> TYPE rep₂) -> (k -> TYPE (Max rep₁ rep₂)) }}} More importantly, are there any '''actual''' cases in base/core amenable to levity polymorphism? If not I'll close the ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13179#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13179: Levity-polymorphic data types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12708 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I'd need more info about your `Product` and `Sum` (constructors, usage sites) to know if they are feasible. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13179#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC