如何创建不返回类型的类型构造函数？

Question

我正在尝试创建一个类型构造函数，其签名不以

*

（类型）结尾（例如

k -> k

）

这是一个小例子：

{-# 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

如果我使用类型同义词（Identity1）

(a :: k) :: (a :: k)

它可以工作，但是我无法部分应用它来获得

k -> k

如果我使用新类型（Identity2），我可以部分应用它，但返回的元素必须是类型

*

（类型）。

我来自 Agda，其中类型就是值，所以也许这无法在 Haskell 中完成。

PS：我知道在这种特定情况下

type instance TF (a :: k -> k) = a

会编译，但这不是我想要实现的目标，除此之外我有一个更复杂的类型族

(a :: k) :: k -> k -> k

，我将使用它来实例化

Compose (a :: k2 -> k3) (b :: k1 -> k2) (c :: k1) = a (b c)

Answer 1

如果您可以有一个

k -> k

类型的类型构造函数，您可以将其实例化为某些 Peano

Nat -> Nat

类型的

Nat

类型，并创建一个新的

Nat

构造函数，该构造函数不是其零或后继者。所以这似乎不是一个理想的功能。