时间戳

首页 > 解决方案 > 为所有高阶类型声明一个类型

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

问题描述

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

我想将类型构造函数与一个完全应用的版本相关联，该版本的数字是类型级别的参数与自然数。这是一个具有所需用途的示例 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.

上面的缺点是，since 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 索引是除 之外的其他特定类型Proxy n，则只返回该类型。

GetN (Either Int Char) Maybe ~ Maybe

但是，任何类型的族解决方案都使得在 lhs 上为withProxy n编写族实例是非法的。我愿意输入基于类的解决方案，我们可以在其中拥有：GetNProxy n

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，从中我可以派生要遍历的源和目标。

标签： haskelltype-familieshigher-kinded-types

解决方案

这个怎么样：

{-# 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接受两个(->)-kinded 参数，但Proxy 0仍然Proxy 1有效。

推荐阅读