haskell - 我们能否获得任意类型生成类型的标识、常量和定点数据类型构造函数？

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

但我不太确定。