#10039 closed feature request (fixed)
Make Const (Control.Applicative) kind polymorphic in its second argument
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.1 |
Component: | Core Libraries | Version: | 7.8.4 |
Keywords: | report-impact | Cc: | hvr, ekmett, core-libraries-committee@…, RyanGlScott, duairc |
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: |
Description (last modified by )
Is there any reason why Const
isn't kind polymorphic?
newtype Const a (b :: k) = Const { getConst :: a } deriving (Generic, Generic1)
An example where I need it is for interpreting typed PHOAS, the following fails to compile complaining that The first argument of ‘PTerm’ should have kind ‘Ty -> *’, but ‘Const Char’ has kind ‘* -> *’
:
{-# 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 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.
Change History (19)
comment:1 Changed 4 years ago by
comment:2 Changed 4 years ago by
Cc: | core-libraries-committee@… added |
---|---|
Component: | libraries/base → Core Libraries |
Owner: | set to ekmett |
comment:3 Changed 4 years ago by
Another example of a kind polymorphic Const
is in the paper True Sums of Products by Edsko de Vries and Andres Löh, defined in section 2. Preliminaries:
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
andConstant
, respectively), but the definition ofK
makes use of GHC'sPolyKinds
extension and is kind polymorphic; we will need this generality.
comment:4 Changed 4 years ago by
Description: | modified (diff) |
---|
comment:5 Changed 4 years ago by
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
comment:7 Changed 4 years ago by
To my knowledge all of the others that take a phantom argument (like Proxy
, Proxy#
, etc.) which can be already are kind polymorphic.
comment:8 Changed 4 years ago by
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.
comment:9 Changed 4 years ago by
That would be great, other types like Data.Functor.Compose.Compose
and Data.Functor.Reverse.Reverse
could also be generalised (Vinyl does this with Compose):
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
, discussion), non-empty vectors:
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 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.
comment:10 Changed 4 years ago by
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.
comment:11 Changed 4 years ago by
Keywords: | report-impact added |
---|
comment:12 Changed 3 years ago by
Cc: | RyanGlScott added |
---|
comment:13 Changed 3 years ago by
Owner: | ekmett deleted |
---|
comment:14 Changed 3 years ago by
Cc: | duairc added |
---|
comment:15 Changed 3 years ago by
Differential Rev(s): | → Phab:D1630 |
---|
comment:16 Changed 3 years ago by
Status: | new → patch |
---|
comment:18 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
comment:19 Changed 3 years ago by
Milestone: | → 8.0.1 |
---|
A good question for the Core Libraries Committee