Подтвердить что ты не робот

Могу ли я магизировать равенство типа от функциональной зависимости?

Я пытаюсь понять смысл MultiParamTypeClasses и FunctionalDependencies, и следующее показалось мне очевидным:

{-# LANGUAGE MultiParamTypeClasses
           , FunctionalDependencies
           , TypeOperators #-}

import Data.Type.Equality

class C a b | a -> b

fob :: (C a b, C a b') => proxy a -> b :~: b'
fob _ = Refl

К сожалению, это не работает; GHC не заключает b ~ b' из этого контекста. Есть ли способ сделать эту работу, или функциональная зависимость не "внутренне" доступна?

4b9b3361

ОТВЕТЫ

Ответ 1

Я не думаю, что этот факт (как указано в типе fob) действительно прав. Из-за свойства open-класса классов типов вы можете нарушить функцию fundep с границами модулей.

Это показано в следующем примере. Этот код был протестирован только с GHC 7.10.3 (в старых версиях фонды были сильно разбиты - не знаю, что будет потом). Предположим, что вы действительно можете реализовать следующее:

module A 
  (module A
  ,module Data.Type.Equality
  ,module Data.Proxy
  )where 

import Data.Type.Equality
import Data.Proxy 

class C a b | a -> b 

inj_C :: (C a b, C a b') => Proxy a -> b :~: b' 
inj_C = error "oops"

Затем еще несколько модулей:

module C where 
import A

instance C () Int 

testC :: C () b => Int :~: b 
testC = inj_C (Proxy :: Proxy ())

и

module B where 
import A

instance C () Bool 

testB :: C () b => b :~: Bool 
testB = inj_C (Proxy :: Proxy ())

и

module D where 

import A 
import B
import C 

oops :: Int :~: Bool
oops = testB

oops_again :: Int :~: Bool 
oops_again = testC

Int :~: Bool, очевидно, неверно, поэтому в силу противоречия inj_C не может существовать.

Я уверен, что вы все равно можете спокойно писать inj_C с помощью unsafeCoerce, если вы не экспортируете класс C из модуля, где он определен. Я использовал эту технику и много раз пробовал, и не смог написать противоречие. Не сказать, что это невозможно, но, по крайней мере, очень сложный и редкий случай.

Ответ 2

Вам не нужно прибегать к нескольким модулям, чтобы обмануть функциональную проверку зависимостей. Вот два примера неправильных источников финансирования, которые все еще строятся с помощью HEAD. Они адаптированы из набора тестов GHC.

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
             FlexibleInstances, FlexibleContexts,
             UndecidableInstances, DataKinds, PolyKinds,
             GADTs #-}

module M where


data K x a = K x

class Het a b | a -> b where
  het :: m (f c) -> a -> m b
instance Het t t where het = undefined

class GHet (a :: * -> *) (b :: * -> *) | a -> b
instance            GHet (K a) (K [a])
instance Het a b => GHet (K a) (K b)


data HBool = HFalse | HTrue

class TypeEq x y b | x y -> b
instance {-# OVERLAPS #-} (HTrue ~ b)  => TypeEq x x b
instance {-# OVERLAPS #-} (HFalse ~ b) => TypeEq x y b

Фундаментальная проверка еще намного лучше, чем раньше!