Make Const (Control.Applicative) kind polymorphic in its second argument
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.
Edited by Icelandjack