为所有更高阶的类型声明一个类型 [英] Declare a type to for all higher order kind

问题描述

我有一种感觉，我在问不可能的事，但事情就到此为止.

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

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

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

U类型是似乎需要获得我想要的行为的另一个代理.如果我已完全使用U，即U (a :: *)，则可以使用UnU对其进行解包.

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.

上述缺点是，由于Proxy i :: *，MkNumbered仅能处理具有*变量的构造函数.编号

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

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

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

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)

这很有帮助，只有这三个NPxy定义可能涵盖了大多数高阶同类案例.但是我想知道是否有一种方法可以增强此功能，以便涵盖所有k -> j -> ... -> *案例?

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

无论如何，所有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

之所以称为UndefinedN，是因为它在种类方面似乎是一个底线.

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

预期用途

我打算使用的问题的关键是要查询代理参数的类型.

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

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

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

但是，对于Proxy n的任何类型族解决方案都使在lhs上用Proxy n编写GetN的族实例成为非法.我愿意输入基于类的解决方案，我们可以在其中提供:

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.

其余的这些只是出于信息的考虑，但是有了上面的内容，我应该能够从我的代理参数类型派生子数据.例如，在上面填写我的A定义:

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

unA处的子数据，其编号参数如下所示:

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)

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

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.

推荐答案

我通过结合类型和数据族找到了一个解决方案.从数据定义开始:

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

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

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.

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

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.

在GHCI会话中进行检查:

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

我们看到此代理几乎已准备就绪.返回的lhs表明该类型具有种类k，但是rhs上的第一个kind参数(我认为它对应于class参数)具有适当的种类.

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.

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

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

现在，可以使用以下家族来恢复Nat:

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

这篇关于为所有更高阶的类型声明一个类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！