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

Question

依赖对如何输入 Sigma来自singletons使用库吗？

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

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

(您可以在 this question 中找到 replicateVec 的几种不同实现)。

我想创建一个函数 replicateVecSigma返回 Vect在依赖对中。理想情况下，它应如下所示:

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更容易吗？

你可以找到我的完整代码here .

<小时/>

为了完整起见，这里是 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

去功能化是解决缺少一流函数的通用方法(事实上，它最初是作为一种消除这些函数的编译技术而被发现的)，将它们编码为由单个一阶 Apply 函数解释的符号。

例如，您的 Foo a b 是一个对函数 \n -> a n b 进行编码的符号。

<小时/>

获得等效符号的另一种方法是遵循 (\n -> a n b) = 翻转 a b 的直觉。

请注意，像 Vec 这样的类型构造函数本身并不是可以传递给 Apply 的符号，但必须包装在“符号构造函数”中:TyCon2 Vec 是 \n ->\b -> Vec n b 的符号。

单例有一个表示flip的符号，FlipSym0(符号可以通过将其他符号作为参数来代表高阶函数)。

Foo a b = Apply (Apply FlipSym0 (TyCon2 a)) b

请注意，部分应用程序会减少为其他符号:

        = Apply (FlipSym1 (TyCon2 a)) b
        = FlipSym2 (TyCon2 a) b

<小时/>

TyFun 类型是一种为非功能化符号提供类型的方法。我看到的主要好处是类型推断；如果没有它，类型家族可能会陷入困惑的境地。

另请参阅 Richard Eisenberg 撰写的有关 Haskell 类型去功能化的博文:https://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-win/