Declare a type to for all higher order kind

Question

I have a feeling I'm asking the impossible, but here it goes.

I want to associate type constructors with a fully applied version that number's the parameters at the type level with natural numbers. Here's an example ghci session with its desired use:

ghci> :kind! MKNumbered Maybe
MKNumbered Maybe :: *
= Maybe (Proxy Nat 1)
ghci> :kind! MKNumbered Either
MKNumbered Either :: *
= Either (Proxy Nat 1) (Proxy Nat 2)

To cut down on the noise of the above a little bit, essentially I get something like

Maybe  >----> Maybe 1
Either >----> Either 1 2 

It turns out, I can get close enough with the following type families. They actually use an extra parameter, specifying the total number of arguments, but that's ok.

type MkNumbered f n = UnU (MkNumbered_ (U f) 1 n)
type family MkNumbered_ (f :: k) (i::Nat) (n::Nat) :: j where
  MkNumbered_ (U f) i i = U (f (Proxy i))
  MkNumbered_ (U f) i n = MkNumbered_ (U (f (Proxy i))) (i+1) n

data U (a::k)
type family UnU f :: * where
  UnU (U f) = f

The U type is another proxy which seems necessary to get behavior I wanted. If I have a fully applied U, i.e. U (a :: *) I can unwrap it with UnU.

The shortcoming of the above is that, since Proxy i :: *, MkNumbered can only handle constructors with * variables. Numbering

data A (f :: * -> *) a = ...

is out, A (Proxy 1) (Proxy 2) won't work in the Proxy 1 argument. I should be able to enhance MkNumbered, by introducing a number of specific numbering proxies:

data NPxy1 (n :: Nat)
data NPxy2 (n :: Nat) (a :: i)
data NPxy3 (n :: Nat) (a :: i) (b :: j)
...

This should leave me with behavior like:

ghci> :kind! MKNumbered A
MKNumbered A :: *
= A (NPxy2 Nat 1) (NPxy1 Nat 2)

That helps a lot, just those three NPxy definitions probably cover most of the higher ordered kind cases. But I was wondering if there was a way to enhance this so that I could cover all k -> j -> ... -> * cases?

---

Incidentally, I don't seriously hope to handle types like

data B (b::Bool) = ...   

I would need something like this illegal definition:

data NPxyBool (n :: Nat) :: Bool

In any case, all the Bool types seem to be taken already. Going further, I'd be thrilled to learn that there was a way to create some data

data UndefinedN (n :: Nat) :: forall k . k

which I called UndefinedN since it seems like a bottom at the kind level.

---

Edit: Intended Use

The crux of my intended use is to query a type for the proxied parameter.

type family GetN s (a :: k) :: k 

GetN (Either Int Char) (Proxy 1) ~ Int

However, I also require that if the Proxy index is some other specific type besides Proxy n, then that type is just returned.

GetN (Either Int Char) Maybe ~ Maybe

However, any type family solution for Proxy n makes writing family instances for GetN with Proxy n on the lhs illegal. I'm open to type class based solutions, where we can have:

instance (Proxy n ~ pxy, GetNat s n ~ a) => GetN s pxy a where... 

but my requirement to also resolve concrete values to themselves causes conflicting instance definitions that I'm also having trouble to resolve.

The rest of this is just for information sake, but having the above I should be able to derive sub-data from my proxy parameter types. For example, filling in my definition of A, above:

data A f a = A { unA :: f (Maybe a) }

the sub-data at unA, as numbered parameters looks like:

type UnANums = (Proxy 1) (Maybe (Proxy 2))

I would like to derive a type family (or some other method) that creates a concrete sub-data based on an example of the super-data.

type family GetNs s (ns :: k) :: k
GetNs (A [] Int) UnANums ~ [Maybe Int]
GetNs (A (Either String) Char) UnANums ~ Either String (Maybe Char)

Ultimately, this is leading to deriving traversal signatures generically. Given a source and target contexts, for instance A f a and A g b, in a Generic representation I will have at the K1 nodes types like UnANums, from which I can derive a source and target to traverse to.

Answer 1

How about this:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module SO56047176 where
import GHC.TypeLits
import Data.Functor.Compose -- for example

type family Proxy (n :: Nat) :: k

type Maybe_ = Maybe (Proxy 0)
type Either__ = Either (Proxy 0) (Proxy 1)
type Compose___ = Compose (Proxy 0) (Proxy 1) (Proxy 2)

Data.Functor.Compose takes two (->)-kinded parameters, but Proxy 0 and Proxy 1 still work.

Answer 2

I found a solution by way of type and data families combined. Starting with the data definition:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}

import GHC.TypeLits hiding ( (*) )
import Data.Kind

class HasNProxyK j where
  data NProxyK (n :: Nat) (a::j) :: k
instance HasNProxyK Type where
  data NProxyK n a = NProxyK0
instance HasNProxyK k => HasNProxyK (j -> k) where
  data NProxyK n f = NProxyKSuc -- or NProxyKS (ProxyK n (f a))

I declare a type class HasNProxyK for which kinds will be instances. The associated data, NProxyK expects a Nat and some variable of the appropriate kind, j. The return type of this data family will be some other kind, k.

I then create a base case for Type, (aka *), and an inductive case for all higher kinds that eventually lead to a kind with HasNProxyK.

Checking this out in a GHCI session:

> :kind! NProxyK 3 Int
NProxyK 3 Int :: k
= NProxyK * k 3 Int

> :kind! NProxyK 3 (,,,,)
NProxyK 3 (,,,,) :: k
= NProxyK (* -> * -> * -> * -> * -> *) k 3 (,,,,)

We see that this proxy is almost ready. The lhs of the return shows that the type has a kind k, but the first kind parameter on the rhs (which I believe corresponds to the class parameter) has the appropriate kind.

We could specify at the call site the appropriate kind for k, instead I just made a type family to ensure the NProxyK kind matches the class kind.

type family ToNProxyK (n :: Nat) (a :: k) :: k where
  ToNProxyK n (a :: Type) = NProxyK n a
  ToNProxyK n (a :: j -> k) = NProxyK n a

>:kind! ToNProxyK 1 (,,,,)
ToNProxyK 1 (,,,,) :: * -> * -> * -> * -> * -> *
= NProxyK
  (* -> * -> * -> * -> * -> *) (* -> * -> * -> * -> * -> *) 1 (,,,,)

Now, the Nat can be recovered using something like the following family:

type family LookupN (x :: k) :: Maybe Nat where
  LookupN (NProxyK n a) = Just n
  LookupN x             = Nothing

>:kind! (LookupN (ToNProxyK 3 Maybe))
(LookupN (ToNProxyK 3 Maybe)) :: Maybe Nat
= 'Just Nat 3
>:kind! (LookupN Maybe)
(LookupN Maybe) :: Maybe Nat
= 'Nothing Nat