Can we obtain the identity, constant, and fixpoint datatype constructors for arbitrary type-producing kinds?

user_1726343 0
Viewed 147

Here are some type constructors:

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

Here are some more type constructors:

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 }

We can organize these type constructors into a data family:

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

These definitions are an example of ad-hoc polymorphism, in that I must laboriously instantiate the class on a case by case basis for each Type-producing kind I can think of. Is it possible to define these datatype constructors in a parametrically polymorphic way, so that we have datatype constructors of kind:

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

which I can instantiate at any Type producing kind without further ceremony (e.g. instantiating a class for said kind)?

haskell
1 Answers

How about a CPS sort of encoding?

A -> B to (A -> Type) -> (B -> Type)

So at kind level we want

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

I is easy being just

 newtype I x k = I (k x)

K is slightly harder

 newtype K a b k = K (k a)

I think fix is

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

But I'm not quite sure.

user_9906660
Related