haskell - 如何帮助 GHC 推断 `Arrows (Domains func) (CoDomain func) ~ func`

Question

考虑在代码库Arrows中定义的,Domains和CoDomain类型族。agda

对程序员来说很明显，它认为Arrows (Domains func) (CoDomain func) ~ func. 但我无法curries (Proxy :: Proxy (Domains func)) (Proxy :: Proxy (CoDomain func)) undefined :: func通过 GHC 的类型检查器。那是因为 GHC 不够聪明，无法推断 和 的组合Domains是单CoDomain射的。有没有办法教 GHC 呢？我想有些情况会在IsBase谓词上分裂。

Answer 1

你改成Currying被索引会更好func吗？

class Currying func where
  curries :: (Products (Domains func) -> CoDomain func) -> func
  uncurries :: func -> Products (Domains func) -> CoDomain func

instance Currying b => Currying (a -> b) where
  curries f a = curries (f . (,) a)
  uncurries f (a, as) = uncurries (f a) as

instance {-# OVERLAPPABLE #-} (IsBase b ~ 'True) => Currying b where
  curries f = f ()
  uncurries b _ = b

---

我们也可以用这种方式断言公理，尽管我什至不确定这个公理是否安全：

arrowAxiom :: forall func. func :~: Arrows (Domains func) (CoDomain func)
arrowAxiom = unsafeCoerce Refl

可以通过公理上的模式匹配将相等性置于范围内。