问题标签 [derivingvia]

最好的代码是不存在的代码，在这方面，Haskell 对派生实现有很好的支持（使用deriving via.

据我所知，OCaml 中的相同需要一些手动管道

这些推导在 OCaml 中的状态如何？

到目前为止，有没有更好的方法来自动提供相应的证明树？

deriving做一些类似的更强大的扩展会很难吗？

我正在使用 ReaderT 为这种类型编写 Monad 实例并通过

我试过这样做

但出现错误：

我究竟做错了什么？

我想学习使用 Deriving Via 来获取更多类型。目前，我经常遇到的一个问题是泛型表示不同时，但如果转换为类型表示更深入到嵌套类型，则它们将是相等的。

简单的例子：

不起作用，因为Rec0 () :+: Rec0 ()不强制使用U1 :+: U1，即使也:kind! Rep ()给出了 U1。

更复杂的例子

是同构的，Free [] a并且由于类似的原因它不会强制。我如何在这些类型之间进行强制转换？我也知道如何使用 DerivingVia 在具有相等 Rep1 的类型之间进行强制转换，如果这有帮助的话。

以下断言是否正确：

1. 唯一真正的同构，用户可以通过编程方式访问，由 Haskell 类型系统验证，并且 Haskell 编译器是/可以知道的，是：

   • Haskell 数据类型的一组值
   • 其构造函数所需的类型值的集合

2. 即使是通用编程也不能产生“真正的”同构，其组合在运行时会产生一个身份（因此staged-sop -在Ocaml中也是如此）

3. Haskell 本身是唯一产生同构的Coercible，但那些同构仅限于恒等同构

“真正的同构，用户可以通过编程方式访问，由 Haskell 类型系统验证，并且 Haskell 编译器是/可以知道的”我的意思是一对函数u : a -> b，并且v : b -> aHaskell知道（通过被告知或以其他方式）u.v=id并且v.u=id. 就像它知道（在编译时）如何重写一些代码来进行“折叠融合”，这类似于立即识别并应用它。

给定以下数据类型

我可以像这样为 Applicative 等编写实例（在这里省略 Functor，因为我们可以使用DeriveFunctor）：

由于Both与 同构(a,b)，我想知道是否可以使用DerivingVia来派生实例：

这会导致错误消息，例如：

我将其解释为“编译器不知道如何Both变成(,)”。我如何告诉编译器使用明显的方式来做到这一点？

我已经看到了这个问题和答案，但我希望有一个需要更少样板的解决方案。

我希望能够写出类似的东西：

是否可以通过一揽子实施？我做到了

而且我不知道如何写这个，除了手工编写每个实例：一个实例为真，一个实例为假，等等。我不想全部手写，也不想使用模板haskell 为我做这件事。我可以只有一个实例来做吗？

或者也许存在其他一些方法？我的用例是能够编写：

至于我在世界上看到的这样做的图书馆，它们似乎都有一些小的设置，我相信这些设置都是手工实现的。