封闭式家庭的归纳定义

Question

这是我要实现的功能越少：

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType             #-}
type family ReturnType arr where
  ReturnType (a -> b) = ReturnType b
  ReturnType a = a
type family ReplaceReturnType t r where
  ReplaceReturnType (a -> b) r = a -> ReplaceReturnType b r
  ReplaceReturnType _ r = r
class CollectArgs f where
  collectArgs :: ((forall r. ReplaceReturnType f r -> r) -> ReturnType f) -> f
instance CollectArgs f => CollectArgs (a -> f) where
  collectArgs :: ((forall r. (a -> ReplaceReturnType f r) -> r) -> ReturnType f) -> a -> f
  collectArgs f a = collectArgs (ap -> f (k -> ap (k a)))
instance (ReturnType a ~ a, ReplaceReturnType a dummy ~ dummy) => CollectArgs a where
  collectArgs :: ((forall r. ReplaceReturnType a r -> r) -> a) -> a
  collectArgs f = f id

我最终想对此做的是编写在传入参数数量中具有多态性的函数，而它们不必是类型类定义的一部分（这与printf var args样式相对应）。因此，例如：

wrapsVariadicFunction :: (CollectArgs f) => f -> Int -> f
wrapsVariadicFunction f config = collectArgs $ apply -> 
  if odd config 
    then error "odd config... are you nuts?!"
    else apply f

仅f的返回类型可能不会与wrapsVariadicFunction的坐层。

现在，在一个完美的世界中，我可以将类型类与封闭类型的家庭联系起来（可以这么说），这很容易实现，因为连接ReplaceReturnType a r ~ r将很清楚。

由于我无法说明这种连接，因此可以理解，GHC 8.2.1尚不清楚：

    * Could not deduce: ReplaceReturnType a r ~ r
      from the context: (ReturnType a ~ a,
                         ReplaceReturnType a dummy ~ dummy)
        bound by the instance declaration
      `r' is a rigid type variable bound by
        a type expected by the context:
          forall r. ReplaceReturnType a r -> r
      Expected type: ReplaceReturnType a r -> r
        Actual type: r -> r
    * In the first argument of `f', namely `id'
      In the expression: f id
      In an equation for `collectArgs': collectArgs f = f id
    * Relevant bindings include
        f :: (forall r. ReplaceReturnType a r -> r) -> a
        collectArgs :: ((forall r. ReplaceReturnType a r -> r) -> a) -> a
   |
29 |   collectArgs f = f id
   |

在实例上下文中，这里的解决方案将通过dummy普遍量化，但这是不可能的（从我在ICFP上看到的内容来看）。也很麻烦。

因此，这里的实际问题是：如何将价值级别的定义与封闭类型的家庭相关联？还是这是不可能的，因为不能再擦除类型？如果是这样，还有其他解决方法吗？

Answer 1

拥有看起来像重叠的这些类型类的标准技巧是将第二个参数添加到Typeclass中，该参数在每个实例中都不同，并且可以从另一个实例中计算出其值

这个想法蒸馏到其核心的核心如下（我们需要一些可怕的扩展名，例如UndecidableInstances，但这很好：我们正在编写总程序）：

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE UndecidableInstances   #-}
type family IsBase arr :: Bool where
  IsBase (a -> b) = 'False
  IsBase a        = 'True
class SillyId a b where
  sillyId :: IsBase a ~ b => a -> a
instance SillyId b (IsBase b) => SillyId (a -> b) 'False where
  sillyId f = x -> sillyId (f x)
instance SillyId b 'True where
  sillyId t = t

现在，在您的情况下，这更复杂了，因为您不仅希望此额外的参数进行调度，还希望其他类型级别的功能基于它减少。诀窍是...用该调度来定义这些功能！

当然，类型级别Bool将不再执行：您需要保留所有信息。因此，代替IsBase，您将拥有IsArrow：

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE UndecidableInstances   #-}
type family IsArrow arr :: Either (*, *) * where
  IsArrow (a -> b) = 'Left '(a, b)
  IsArrow a        = 'Right a
type family ReturnType arr where
  ReturnType ('Left '(a, b)) = ReturnType (IsArrow b)
  ReturnType ('Right a)      = a
type family ReplaceReturnType t r where
  ReplaceReturnType ('Left '(a, b)) r = a -> ReplaceReturnType (IsArrow b) r
  ReplaceReturnType _               r = r
class CollectArgs f (f' :: Either (*, *) *) where
  collectArgs :: IsArrow f ~ f' => ((forall r. ReplaceReturnType f' r -> r) -> ReturnType f') -> f
instance CollectArgs f (IsArrow f) => CollectArgs (a -> f) ('Left '(a, f)) where
  collectArgs :: ((forall r. (a -> ReplaceReturnType (IsArrow f) r) -> r) -> ReturnType (IsArrow f)) -> a -> f
  collectArgs g a = collectArgs (ap -> g (k -> ap (k a)))
instance CollectArgs a ('Right a) where
  collectArgs :: IsArrow a ~ 'Right a => ((forall r. ReplaceReturnType (IsArrow a) r -> r) -> a) -> a
  collectArgs f = f id

和voilà。当然，您可以为ReplaceReturnType (IsArrow a) r定义类型的同义词，以使符号更轻一些，但这就是其中的要点。