为所有高阶类型声明一个类型

Question

我有一种感觉，我在问不可能的事，但它就是这样。

我想将类型构造函数与一个完全应用的版本相关联，该版本将类型级别的参数与自然数相关联。这是一个具有所需用途的示例 ghci 会话：

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

为了减少上面的噪音，基本上我得到了类似的东西

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

事实证明，我可以与以下类型家族足够接近。他们实际上使用了一个额外的参数，指定参数的总数，但这没关系。

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

U 类型是另一个代理，它似乎是获得我想要的行为所必需的。如果我有一个完全应用的U，即U (a :: *)，我可以用UnU 解开它。

上面的缺点是，由于Proxy i :: *，MkNumbered只能处理带有*变量的构造函数。编号

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

出来了，A (Proxy 1) (Proxy 2) 在Proxy 1 参数中不起作用。我应该能够通过引入一些特定的编号代理来增强MkNumbered：

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

这应该让我有如下行为：

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

这很有帮助，只是这三个 NPxy 定义可能涵盖了大多数高阶类型的情况。但我想知道是否有办法增强这一点，以便我可以覆盖所有k -> j -> ... -> * 案例？

---

顺便说一句，我不希望处理像这样的类型

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

我需要这样的非法定义：

data NPxyBool (n :: Nat) :: Bool

无论如何，所有Bool 类型似乎都已被采用。更进一步，我很高兴得知有一种方法可以创建一些数据

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

我称之为UndefinedN，因为它看起来像一个底部。

---

编辑：预期用途

我打算使用的关键是查询代理参数的类型。

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

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

但是，我还要求如果代理索引是除Proxy n 之外的其他特定类型，则只返回该类型。

GetN (Either Int Char) Maybe ~ Maybe

但是，Proxy n 的任何类型族解决方案都会使在 lhs 上使用 Proxy n 为 GetN 编写族实例是非法的。我愿意接受基于类型的解决方案，我们可以：

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

但我也需要自己解析具体值会导致冲突的实例定义，我也无法解决。

剩下的只是为了提供信息，但是有了上面的内容，我应该能够从我的代理参数类型中派生子数据。比如填写我对A的定义，如上：

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

unA 处的子数据，编号参数如下：

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

我想派生一个类型族（或其他方法），该类型族基于超数据的示例创建具体的子数据。

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

最终，这将导致一般地导出遍历签名。给定一个源和目标上下文，例如A f a 和A g b，在一个通用表示中，我将在K1 节点上拥有像UnANums 这样的类型，我可以从中派生一个源和目标来遍历。

Answer 1

这个怎么样：

{-# 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 采用两个 (->) 类参数，但 Proxy 0 和 Proxy 1 仍然有效。

Answer 2

我通过类型和数据系列相结合的方式找到了解决方案。从数据定义开始：

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

我声明了一个类型类HasNProxyK，kinds 将是它的实例。关联数据NProxyK 需要Nat 和一些适当类型的变量j。此数据系列的返回类型将是其他类型，k。

然后，我为Type（又名*）创建一个基本案例，并为所有最终导致HasNProxyK 的类别的所有更高种类创建一个归纳案例。

在 GHCI 会话中检查：

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

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

我们看到这个代理几乎准备好了。返回的 lhs 表明该类型有一个 kind k，但是 rhs 上的第一个 kind 参数（我相信它对应于 class 参数）有适当的 kind。

我们可以在调用站点为 k 指定适当的种类，而我只是创建了一个类型族以确保 NProxyK 种类与类种类匹配。

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

现在，Nat 可以使用类似以下系列的东西来恢复：

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