Opened 4 years ago

Closed 3 years ago

Last modified 3 years ago

#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 Iceland_jack)

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 simonpj

A good question for the Core Libraries Committee

comment:2 Changed 4 years ago by simonpj

Cc: core-libraries-committee@… added
Component: libraries/baseCore Libraries
Owner: set to ekmett

comment:3 Changed 4 years ago by Iceland_jack

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 and Constant, respectively), but the definition of K makes use of GHC's PolyKinds extension and is kind polymorphic; we will need this generality.

comment:4 Changed 4 years ago by Iceland_jack

Description: modified (diff)

comment:5 Changed 4 years ago 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

comment:6 Changed 4 years ago by Iceland_jack

I wonder if other data types would benefit from kind polymorphism

comment:7 Changed 4 years ago 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.

comment:8 Changed 4 years ago 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.

comment:9 Changed 4 years ago 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 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 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.

comment:11 Changed 4 years ago by hvr

Keywords: report-impact added

comment:12 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:13 Changed 3 years ago by thomie

Owner: ekmett deleted

comment:14 Changed 3 years ago by duairc

Cc: duairc added

comment:15 Changed 3 years ago by duairc

Differential Rev(s): Phab:D1630

comment:16 Changed 3 years ago by duairc

Status: newpatch

comment:17 Changed 3 years ago by Ben Gamari <ben@…>

In edcf17b/ghc:

Move Const to own module in Data.Functor.Const and enable PolyKinds

`Const` from `Control.Applicative` can trivially be made
kind-polymorphic in its second argument. There has been a Trac issue
about this for nearly a year now. It doesn't look like anybody objects
to it, so I figured I might as well make a patch.

Trac Issues: #10039, #10865, #11135

Differential Revision: https://phabricator.haskell.org/D1630

Reviewers: ekmett, hvr, bgamari

Subscribers: RyanGlScott, thomie

comment:18 Changed 3 years ago by bgamari

Resolution: fixed
Status: patchclosed

comment:19 Changed 3 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.