如何使用单例库中的依赖对类型Sigma？

Question

如何使用来自单例库的依赖对类型Sigma？

假设存在以下类型索引列表和复制函数:

data Vect :: Nat -> Type -> Type where
  VNil :: Vect 0 a
  VCons :: a -> Vect n a -> Vect (n + 1) a

replicateVec :: forall n a. Sing n -> a -> Vect n a

(你可以replicateVec在这个问题中找到几个不同的实现).

我想创建replicateVecSigma一个Vect在依赖对中返回a 的函数.理想情况下,它将如下所示:

replicateVecSigma :: Natural -> Sigma Nat (\n -> Vect n String)

怎么Sigma用来写这个功能？如何写出函数的类型？

---

实际上,我能够实现replicateVecSigma如下,但它似乎不是很干净:

data Foo a b (m :: TyFun Nat Type)

type instance Apply (Foo a b) (n :: Nat) = a n b

replicateVecSigma :: Natural -> Sigma Nat (Foo Vect String)
replicateVecSigma i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec snat "hello"

似乎不幸的是我必须声明这种Foo类型和Apply实例才能使用Sigma.singletons图书馆是否提供了Sigma更轻松的工作方式？

你可以在这里找到我的完整代码.

---

为了完整起见,这里有以下定义Sigma:

data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t

这是~>:

type a ~> b = TyFun a b -> *

data TyFun :: * -> * -> *

instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2)

type instance Demote (k1 ~> k2) = Demote k1 -> Demote k2

class SingKind k where
  type family Demote k :: * = r | r -> k
  fromSing :: forall (a :: k). Sing a -> Demote k
  toSing :: Demote k -> SomeSing k

这是@@:

type a @@ b = Apply a b

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

singletons为...定义了一堆实例Apply.

怎么做TyFun和Apply工作？

---

以下是上述三个问题:

1. 我怎么Sigma用来写一个像这样的函数replicateVecSigma :: Natural -> Sigma Nat (\n -> Vect n String)？
2. 我可以replicateVecSigma使用Foo上面的类型编写,但似乎有太多额外的工作.有没有更简单的方法？
3. 怎么做TyFun和Apply工作？

Answer 1

在这个特定的例子中，我们想要计算类型级别的 lambda

\n -> Vect n String

不幸的是，我们没有类型级别的 lambda。最多，我们可以定义类型族，就像OP所做的那样。然而，我们可以用 pointfree 风格重写 lambda：

\n -> flip Vect String n    -- pseudocode
flip Vect String

singletons我们可以使用类型级类型函数将这个想法转化为实际类型Flip。在这里，我们想要部分应用Flip两个参数（在饱和调用中需要三个参数），因此我们使用“去功能化”FlipSym2变体。

这编译：

replicateVecSigma :: Natural -> Sigma Nat (FlipSym2 (TyCon Vect) String)
replicateVecSigma i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec snat "hello"

如果我们n从一开始就将参数放在最后一个位置，我们就可以避免Flip.

data Vect2 :: Type -> Nat -> Type where
  VNil2 :: Vect2 a 0
  VCons2 :: a -> Vect2 a n -> Vect2 a (n + 1)

replicateVec2 :: forall n a. Sing n -> a -> Vect2 a n
replicateVec2 = undefined

replicateVecSigma2 :: Natural -> Sigma Nat (TyCon (Vect2 String))
replicateVecSigma2 i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec2 snat "hello"

（TyCon Vect2 @@ String这里也适用，在去功能化级别使用显式应用程序@@，而不是实际的类型应用程序。）

非常粗略地说，您可以将去功能化变体视为FlipSym0, FlipSym1, FlipSym2基本标签（不是函数！），没有内在含义，除了以下事实：Apply您可以假装它们是函数来使用它们这一事实。通过这种方式，我们可以像处理函数一样处理非函数（“标签”）。这是必需的，因为在 Haskell 中，我们没有类型级别的函数，因此我们必须使用这些“假装”版本。

这种方法很通用，但它确实需要程序员做比预期更多的工作。

我不知道有任何 Template Haskell 实用程序可以自动将类型级 lambda 转换为 pointfree 形式，然后将其去功能化。那将非常有用。