我们可以获得任意类型生成类型的恒等、常量和固定点数据类型构造函数吗？

Question

下面是一些类型构造函数：

type T0 = Type

type I0 :: T0 -> T0
data I0 x = I0 { getI0 :: x }

type K0 :: T0 -> (T0 -> T0)
data K0 x y = K0 { getK0 :: x }

type Mu0 :: (T0 -> T0) -> T0
data Mu0 f = Mu0 { unMu0 :: f (Mu0 f) }

这里还有一些类型构造函数：

type T1 = Type -> Type

type I1 :: T1 -> T1
data I1 f x = I1 { getI1 :: f x }

type K1 :: T1 -> (T1 -> T1)
data K1 f g x = K1 { getK1 :: f x }

type Mu1 :: (T1 -> T1) -> T1
data Mu1 ff x = Mu1 { unMu1 :: ff (Mu1 ff) x }

我们可以将这些类型构造函数组织成一个数据族：

class Context (k :: Type)
  where
  data I :: k -> k
  data K :: k -> (k -> k)
  data Mu :: (k -> k) -> k

instance Context Type
  where
  data I x = I0 { getI0 :: x }
  data K x y = K0 { getK0 :: x }
  data Mu f = Mu0 { getMu0 :: f (Mu0 f) }

instance Context (Type -> Type)
  where
  data I f x = I1 { getI1 :: f x }
  data K f g x = K1 { getK1 :: f x }
  data Mu ff x = Mu1 { unMu1 :: ff (Mu1 ff) x }

instance Context (Type -> Type -> Type)
  ...

instance Context ((Type -> Type) -> Type)
  ...

这些定义是临时多态性的一个例子，因为我必须为Type我能想到的每一种产生类型，在个案的基础上费力地实例化这个类。是否可以以参数化的多态方式定义这些数据类型构造函数，以便我们拥有以下类型的数据类型构造函数：

type I :: forall k. k -> k
type K :: forall k. k -> (k -> k)
type Mu :: forall k. (k -> k) -> k

我可以在Type没有进一步仪式的情况下在任何生产种类上实例化（例如，为所述种类实例化一个类）？

Answer 1

CPS 编码怎么样？

A -> B到(A -> Type) -> (B -> Type)

所以在善意的层面上我们想要

 I : (a -> Type) -> (a -> Type)
 K : a -> b -> (a -> Type) -> Type
 Fix : ((a -> Type) -> (a -> Type)) ->  (a -> Type) -> Type

我很容易只是

 newtype I x k = I (k x)

K 稍难

 newtype K a b k = K (k a)

我认为修复是

  newtype Fix f k = Fix (k (f (Fix f))

但我不太确定。