[GHC] #10039: Make Const (Control.Applicative) kind polymorphic in its second argument
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: | Owner: Iceland_jack | Status: new Type: feature | Milestone: request | Version: 7.8.4 Priority: normal | Operating System: Unknown/Multiple Component: | Type of failure: None/Unknown libraries/base | Blocked By: Keywords: | Related Tickets: Architecture: | Unknown/Multiple | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Is there any reason why `Const` isn't kind polymorphic? {{{#!hs newtype Const a (b :: k) = Const { getConst :: a } deriving (Generic, Generic1) }}} An example where I need it is for [[http://wiki.ocharles.org.uk/Name%20Binding%20in%20EDSLs|interpreting typed PHOAS]], the following fails to compile complaining that `The first argument of ‘PTerm’ should have kind ‘Ty -> *’, but ‘Const Char’ has kind ‘* -> *’`: {{{#!hs {-# LANGUAGE DataKinds, KindSignatures, GADTs, RankNTypes, PolyKinds #-} import Control.Applicative data Ty = TyBool | TyArr Ty Ty data PTerm :: (Ty -> *) -> Ty -> * where Var :: v t -> PTerm v t Tru :: PTerm v 'TyBool Fals :: PTerm v 'TyBool App :: PTerm v ('TyArr t1 t2) -> PTerm v t1 -> PTerm v t2 Abs :: (v t1 -> PTerm v t2) -> PTerm v ('TyArr t1 t2) newtype Term t = Term (forall v. PTerm v t) showT :: Term t -> String showT (Term pterm) = show' 'a' pterm where show' :: Char -> PTerm (Const Char) t -> String show' _ (Var (Const c)) = [c] show' _ Tru = "True" show' _ Fals = "False" show' s (App x y) = "(" ++ show' s x ++ ") " ++ show' s y show' s (Abs f) = [s] ++ ". " ++ show' (succ s) (f (Const s)) }}} but it compiles if one defines a bespoke form of `Const` with kind `* -> Ty -> *` (or the more general suggestion at the beginning of the ticket), I implemented all the related instances from `Control.Applicative` and the compiled without a hitch. Relevant discussion: a [[http://stackoverflow.com/questions/2023052/haskell-specifying-kind-in- data-declaration|question on StackOverflow]] that predates the `PolyKinds` extension effectively wants to define `type Const' (a :: * -> *) = Const Integer a` which would be possible if it were kind polymorphic. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): A good question for the Core Libraries Committee -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * cc: core-libraries-committee@… (added) * owner: => ekmett * component: libraries/base => Core Libraries -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Iceland_jack): Another example of a kind polymorphic `Const` is in the paper [[http://www .andres-loeh.de/TrueSumsOfProducts/TrueSumsOfProducts.pdf|True Sums of Products]] by Edsko de Vries and Andres Löh, defined in section '''2. Preliminaries''': {{{#!hs newtype I (a :: *) = I { unI :: a } newtype K (a :: *) (b :: k) = K { unK :: a } }}} noting: These are similar to their definitions in the standard libraries (called `Identity` and `Constant`, respectively), but the definition of `K` makes use of GHC's `PolyKinds` extension and is ''kind polymorphic''; we will need this generality. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
Is there any reason why `Const` isn't kind polymorphic?
{{{#!hs newtype Const a (b :: k) = Const { getConst :: a } deriving (Generic, Generic1) }}}
An example where I need it is for [[http://wiki.ocharles.org.uk/Name%20Binding%20in%20EDSLs|interpreting typed PHOAS]], the following fails to compile complaining that `The first argument of ‘PTerm’ should have kind ‘Ty -> *’, but ‘Const Char’ has kind ‘* -> *’`:
{{{#!hs {-# LANGUAGE DataKinds, KindSignatures, GADTs, RankNTypes, PolyKinds #-}
import Control.Applicative
data Ty = TyBool | TyArr Ty Ty
data PTerm :: (Ty -> *) -> Ty -> * where Var :: v t -> PTerm v t Tru :: PTerm v 'TyBool Fals :: PTerm v 'TyBool App :: PTerm v ('TyArr t1 t2) -> PTerm v t1 -> PTerm v t2 Abs :: (v t1 -> PTerm v t2) -> PTerm v ('TyArr t1 t2)
newtype Term t = Term (forall v. PTerm v t)
showT :: Term t -> String showT (Term pterm) = show' 'a' pterm where show' :: Char -> PTerm (Const Char) t -> String show' _ (Var (Const c)) = [c] show' _ Tru = "True" show' _ Fals = "False" show' s (App x y) = "(" ++ show' s x ++ ") " ++ show' s y show' s (Abs f) = [s] ++ ". " ++ show' (succ s) (f (Const s)) }}}
but it compiles if one defines a bespoke form of `Const` with kind `* -> Ty -> *` (or the more general suggestion at the beginning of the ticket), I implemented all the related instances from `Control.Applicative` and the compiled without a hitch. Relevant discussion: a [[http://stackoverflow.com/questions/2023052/haskell-specifying-kind-in- data-declaration|question on StackOverflow]] that predates the `PolyKinds` extension effectively wants to define `type Const' (a :: * -> *) = Const Integer a` which would be possible if it were kind polymorphic.
New description: Is there any reason why `Const` isn't kind polymorphic? {{{#!hs newtype Const a (b :: k) = Const { getConst :: a } deriving (Generic, Generic1) }}} An example where I need it is for [[http://wiki.ocharles.org.uk/Name%20Binding%20in%20EDSLs|interpreting typed PHOAS]], the following fails to compile complaining that `The first argument of ‘PTerm’ should have kind ‘Ty -> *’, but ‘Const Char’ has kind ‘* -> *’`: {{{#!hs {-# LANGUAGE DataKinds, KindSignatures, GADTs, RankNTypes, PolyKinds #-} import Control.Applicative data Ty = TyBool | TyArr Ty Ty data PTerm :: (Ty -> *) -> Ty -> * where Var :: v t -> PTerm v t Tru :: PTerm v 'TyBool Fals :: PTerm v 'TyBool App :: PTerm v ('TyArr t1 t2) -> PTerm v t1 -> PTerm v t2 Abs :: (v t1 -> PTerm v t2) -> PTerm v ('TyArr t1 t2) newtype Term t = Term (forall v. PTerm v t) showT :: Term t -> String showT (Term pterm) = show' 'a' pterm where show' :: Char -> PTerm (Const Char) t -> String show' _ (Var (Const c)) = [c] show' _ Tru = "True" show' _ Fals = "False" show' s (App x y) = "(" ++ show' s x ++ ") " ++ show' s y show' s (Abs f) = [s] ++ ". " ++ show' (succ s) (f (Const s)) }}} but it compiles if one defines a bespoke form of `Const` with kind `* -> Ty -> *` (or the more general suggestion at the beginning of the ticket), I implemented all the related instances from `Control.Applicative` and it compiled without a hitch. Relevant discussion: a [[http://stackoverflow.com/questions/2023052/haskell-specifying-kind-in- data-declaration|question on StackOverflow]] that predates the `PolyKinds` extension effectively wants to define `type Const' (a :: * -> *) = Const Integer a` which would be possible if it were kind polymorphic. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ekmett): I, for one, would support this. We already have packages out there that have to define their own kind- polymorphic `Const`, e.g. `vinyl`. http://hackage.haskell.org/package/vinyl-0.5.1/docs/Data-Vinyl- Functor.html#t:Const -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Iceland_jack): I wonder if other data types would benefit from kind polymorphism -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ekmett): To my knowledge all of the others that take a phantom argument (like `Proxy`, `Proxy#`, etc.) which can be already are kind polymorphic. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ekmett): This may change if we decided to bring more of the "non-transformers" that sit in `transformers` into `base`, e.g. `Product` and `Sum` for functors can generalize {{{ Product :: (k -> *) -> (k -> *) -> k -> * Sum :: (k -> *) -> (k -> *) -> k -> * }}} and the generalizations are quite useful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Iceland_jack): That would be great, other types like `Data.Functor.Compose.Compose` and `Data.Functor.Reverse.Reverse` could also be generalised (Vinyl does this with [[http://hackage.haskell.org/package/vinyl-0.5.1/docs/Data-Vinyl- Functor.html#t:Compose|Compose]]): {{{#!hs newtype Compose (f :: j -> *) (g :: k -> j) (a :: k) = Compose { getCompose :: f (g a) } newtype Reverse (f :: k -> *) (a :: k) = Reverse { getReverse :: f a } }}} A more general `Compose` is definitely useful for composing dictionaries constraints (`Compose Dict Eq`, [[http://www.reddit.com/r/haskell/comments/2qwqf2/generate_list_of_dicts_from_type_level_list/|discussion]]), non-empty vectors: {{{#!hs data Exists :: (k -> *) -> * where Never :: p x -> Exists p more :: Compose (Vector Char) Suc (Suc Zero) more = Compose (Cons 'H' (Cons 'S' Nil)) type NonEmpty a = Exists (Compose (Vector a) Suc) oh :: NonEmpty Char oh = Never more }}} working with typed lists and such (I also ran into [[http://lpaste.net/edit/75980|this]]). It's not clear to me that a generalised `Reverse` would be worth it. I wonder if any of this will break code though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ekmett): Most of the Data.Functor.* suite is amenable to this treatment, yes. I've been programming with rather excessively generalized kinds on a large chunk of code for a couple of years now with surprisingly few problems. However, as we don't currently have those instances in `base` this is definitely a concern for future `base` efforts, not so much for now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: ekmett Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: report- | impact Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: report-impact Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by duairc): * cc: duairc (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: report-impact Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1630 Wiki Page: | -------------------------------------+------------------------------------- Changes (by duairc): * differential: => Phab:D1630 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: patch Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: | Keywords: report-impact Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1630 Wiki Page: | -------------------------------------+------------------------------------- Changes (by duairc): * status: new => patch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner:
Type: feature request | Status: patch
Priority: normal | Milestone:
Component: Core Libraries | Version: 7.8.4
Resolution: | Keywords: report-impact
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D1630
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#10039: Make Const (Control.Applicative) kind polymorphic in its second argument -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Core Libraries | Version: 7.8.4 Resolution: fixed | Keywords: report-impact Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1630 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10039#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC