有人可以提供一个“weaken”函数会做什么的例子吗？

Question

在Thinking With Types练习11.2-i中，练习11.2-i将编写具有以下类型签名的函数。

weaken :: OpenSum f ts -> OpenSum f (x ': ts)

data OpenSum (f :: k -> Type) (ts :: [k]) where
  UnsafeOpenSum :: Int -> f t -> OpenSum f ts 

我认为练习之前的段落应该提供足够的上下文来了解这个函数的功能，但我不清楚。

在实践中，能够扩大开放总和的可能性也很有用。一个新功能，weak，将斧头类型固定在可能性列表的前面。

如果我有一些使用此函数的示例，这将对我完成此练习大有帮助。

Answer 1

UnsafeOpenSum :: Int -> f t -> OpenSum f ts列表中ts与其他类型变量完全无关，因此该构造函数可以生成OpenSum f tsany类型的值ts。

因此，我们得到

weaken :: OpenSum f ts -> OpenSum f (x ': ts)
weaken (UnsafeOpenSum i ft) = UnsafeOpenSum newI ft
   where newI = ...  -- To do

请注意，这两个术语UnsafeOpenSum i ft看起来相同（零件除外i），但类型不同。

weaken (UnsafeOpenSum i ft) = UnsafeOpenSum newI ft
       \- :: OpenSum f ts     |
                              \- :: OpenSum f (x :' ts)

此外，我们需要一个新的索引newI，我们可以根据 来计算它i。

由于访问构造函数允许人们选择ts类型中的任何列表，因此命名构造函数是Unsafe....为了提醒用户应该仅使用它来实现安全原语（例如weaken）。之后，用户应该使用安全原语而不访问较低级别的构造函数。