3

这是旧栗子的变种。我写它期望它不起作用，但它确实起作用了。还是很狡猾？（在 GHC 8.6.5 时。）

{-# LANGUAGE  MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
              FunctionalDependencies, UndecidableInstances, GADTs,
              PatternSignatures   #-}  -- deprecated, but we're not using ScopedTypeVariables

-- 3-way FunDep for Nats Add ??

data ZNat   = ZNat    deriving (Eq, Show, Read)
data SNat a = SNat a  deriving (Eq, Show, Read)

oneNat = SNat ZNat
twoNat = SNat oneNat

class AddNat a b c  | a b -> c, a c -> b, b c -> a  where  -- full 3 FunDeps
  addNat :: a -> b -> c

instance AddNat ZNat b b  where
  addNat _ y  = y

instance {-# OVERLAPPABLE #-} (a ~ SNat a', c ~ SNat c', AddNat a' b c')
         => AddNat a b c  where
  addNat (SNat x) y = SNat (addNat x y)

subNat (_ :: c) (_ :: b) = reflNat :: (AddNat a b c, ReflNat a) => a

-- test:
-- *Main> :t subNat twoNat oneNat
-- subNat twoNat oneNat :: SNat ZNat

class    ReflNat a          where reflNat :: a                -- for ref
instance ReflNat ZNat       where reflNat = ZNat
instance (ReflNat a') => ReflNat (SNat a')  where
  reflNat = (SNat (reflNat :: ReflNat aa => aa))

传统上， class 上只有两个 FunDeps AddNat，第二个实例是

instance ( AddNat a' b c') 
         => AddNat (SNat a') b (SNat c')  where
  addNat (SNat x) y = SNat (addNat x y)            -- implementation is the same

Functional dependencies conflict between instance declarations:如果有 FunDep ，该实例将被拒绝b c -> a。事实上，该OVERLAPPABLE实例正在利用 GHC 的虚假 FunDep 一致性检查。

但是没有那个 FunDep，subNat就无法从参数中推断出它的结果：Ambiguous type variable 'a0'. 我猜我的测试有效，因为参数的类型是subNat完全已知的。如果它们是部分已知的，类型改进将陷入无法拒绝ZNat b b实例的困境。

Oleg Kiselyov 的 ftp 站点曾经有一个类用于 3 向改进添加自然，但它有一个复杂的辅助超类约束和辅助实例的复杂巢穴，基本上重复了中心类。我所做的似乎太简单了。哪里会出错？

4

0 回答 0