Multi-way FunDeps и согласованность с перекрывающимися экземплярами: (почему) это работает? - PullRequest
Новая
       59

Multi-way FunDeps и согласованность с перекрывающимися экземплярами: (почему) это работает?

2 голосов
/ 08 марта 2020

Это вариант старого каштана. Я написал это, ожидая, что это не сработает, но это сработало. Или это хитроумно? (На GH C 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))

Традиционно в классе AddNat есть только два FunDeps, и этот второй экземпляр равен 

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 использует поддельную проверку целостности FunDep GH C .

Но без этого FunDep subNat не может вывести свой результат из аргументы: Ambiguous type variable 'a0'. Я предполагаю, что мой тест работает, потому что типы аргументов subNat известны полностью. Если бы они были частично известны, улучшение типов застряло бы, если бы не было возможности отклонить экземпляр ZNat b b.

На ftp-сайте Олега Киселева был класс для 3-стороннего улучшения добавления натуральных объектов, но у него были сложные крысы. гнездо вспомогательных ограничений суперкласса и вспомогательных экземпляров, которые по существу повторяли центральный класс. То, что я сделал, кажется слишком упрощенным c. Где это будет go неправильно?

...