I am trying to create a type constructor, whose signature does not end with * (Type) (e.g. k -> k)

This is a small example:

{-# LANGUAGE TypeFamilies #-}

type family TF (a :: k) :: k

-- Try 1 : type synonym

type Identity1 (a :: k) = a -- This works

type instance TF (a :: k -> k) = Identity1 -- This does not work: The type synonym ‘Identity1’ should have 1 argument, but has been given none

-- Try 2 : newtype

newtype Identity2 (a :: k) = Identity2 a  -- This does not work: Expected a type, but ‘a’ has kind ‘k’

type instance TF (a :: k -> k) = Identity2 -- This would work

If I use a type synonym (Identity1) (a :: k) :: (a :: k) it works, but then I cannot partially apply it to get k -> k

If I use a newtype (Identity2) I can partially apply it, but the returning element must be of kind * (Type).

I am coming from Agda where types are values, so maybe this cannot be done in Haskell.

PS: I known in this specific case type instance TF (a :: k -> k) = a would compile, but it is not what I want to achieve, besides that I have a more complex type family (a :: k) :: k -> k -> k which I would instance using Compose (a :: k2 -> k3) (b :: k1 -> k2) (c :: k1) = a (b c)

I am trying to create a type constructor, whose signature does not end with * (Type) (e.g. k -> k)

This is a small example:

{-# LANGUAGE TypeFamilies #-}

type family TF (a :: k) :: k

-- Try 1 : type synonym

type Identity1 (a :: k) = a -- This works

type instance TF (a :: k -> k) = Identity1 -- This does not work: The type synonym ‘Identity1’ should have 1 argument, but has been given none

-- Try 2 : newtype

newtype Identity2 (a :: k) = Identity2 a  -- This does not work: Expected a type, but ‘a’ has kind ‘k’

type instance TF (a :: k -> k) = Identity2 -- This would work

If I use a type synonym (Identity1) (a :: k) :: (a :: k) it works, but then I cannot partially apply it to get k -> k

If I use a newtype (Identity2) I can partially apply it, but the returning element must be of kind * (Type).

I am coming from Agda where types are values, so maybe this cannot be done in Haskell.

PS: I known in this specific case type instance TF (a :: k -> k) = a would compile, but it is not what I want to achieve, besides that I have a more complex type family (a :: k) :: k -> k -> k which I would instance using Compose (a :: k2 -> k3) (b :: k1 -> k2) (c :: k1) = a (b c)

• haskell
• type-families
• type-kinds

• 5 I don't think this is possible in Haskell. AFAIK, we can only inhabit a kind through data/newtype definitions when the kind "ends in *", or through data constructors and DataKinds when the kind is a freshly-named one. Type-level functions do not really exist in Haskell, and their substitutes (type synonyms, type families, ...) are not first-class and can not be used everywhere as in true dependently typed languages (e.g. Agda). – chi Commented Jan 20 at 16:24
• I don't think you're going to be able to get the answer you want with the question as it is. Because terms and types are not unified in Haskell, type-level programming is full of artificial limitations, workarounds, and dirty tricks. Solving your "small example" isn't going to solve your "more complex type family" problem. I think you'll have to explain in more detail what you're actually trying to do. – K. A. Buhr Commented Jan 25 at 20:16

1 Answer 1

If you could have a type constructor of kind k -> k you could instantiate it to kind Nat -> Nat for some Peano Nat type and create a new Nat constructor that's not its zero or successor. So this doesn't seem like a desirable feature.