让 GHC 相信类型族声明没有重叠

Question

所以我想实现一个将值应用于函数的第 n 个参数的函数，我们称之为 inject:

inject :: (???) => a -> f -> ???

所以我声明了一个 class 代表所有适用的三元组 (n, a, f)。注意 n 必须大于 0 并且 a 取决于 f 和 n

class (1 <= n) => Applicable n a f | f n -> a where
  type ApplyAt n a f :: Type
  inject :: a -> f -> ApplyAt n a f

然后我们可以对n做一些归纳：

instance Applicable 1 a (a -> b) where
  type ApplyAt 1 a (a -> b) = b
  inject a f = f a

instance (Applicable (n - 1) a c) => Applicable n (a :: Type) (b -> c) where
  type ApplyAt n a (b -> c) = b -> ApplyAt (n - 1) a c
  inject a f = \x -> inject @(n - 1) a (f x)

Applicable n a (b -> c) 暗示 Applicable (n - 1) a c 暗示 n - 1 >= 1 或 n >= 2 所以这些实例声明不重叠。但是 GHC 继续抱怨：

Conflicting family instance declarations:
  ApplyAt 1 a (a -> b) = b
  ApplyAt n a (b -> c) = b -> ApplyAt (n - 1) a c

我应该怎么做才能让 GHC 相信这些类型家族声明没有重叠？

Answer 1

解决方案是使用归纳定义的自然 numbers/positive 整数来避免实例重叠。

data NPlus = One | Suc NPlus

class Applicable (n :: NPlus) a f | f n -> a where
  type ApplyAt n a f :: Type
  inject :: a -> f -> ApplyAt n a f

instance Applicable One a (a -> b) where
  type ApplyAt One a (a -> b) = b
  inject a f = f a

instance (Applicable n a c) => Applicable (Suc n) (a :: Type) (b -> c) where
  type ApplyAt (Suc n) a (b -> c) = b -> ApplyAt n a c
  inject a f = \x -> inject @n a (f x)

-- >>> inject @(Suc One) 1 (\y x -> (y + 3) * x) 2
-- 5
--

让 GHC 相信类型族声明没有重叠

Convince GHC that type family declarations are not overlapping

haskell

type-families

type-level-computation