Функциональные зависимости в конкретном случае

Question

В качестве введения см. this question и my answer. В конце я отмечаю, что кажется, что вы можете удалить необходимость в посторонней спецификации типа с функциональной зависимостью. Вот код, как он стоит:

{-# LANGUAGE GADTs, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-} 

data Nil 
data TList a b where 
    TEmpty :: TList Nil Nil 
    (:.) :: c -> TList d e -> TList c (TList d e) 
infixr 4 :. 

class TApplies f h t r where 
    tApply :: f -> TList h t -> r 

instance TApplies a Nil Nil a where 
    tApply a _ = a 

instance TApplies f h t r => TApplies (a -> f) a (TList h t) r where 
    tApply f (e :. l) = tApply (f e) l] 

Теперь, интуитивная вещь для меня, чтобы сделать, кажется, добавить fundep f h t -> r к TApplies класса типов. Однако, когда я делаю это, GHC жалуется на возвратном экземпляре TApplies следующим образом:

Illegal instance declaration for 
‘TApplies (a -> f) a (TList h t) r’ 
The coverage condition fails in class ‘TApplies’ 
    for functional dependency: ‘f h t -> r’ 
Reason: lhs types ‘a -> f’, ‘a’, ‘TList h t’ 
    do not jointly determine rhs type ‘r’ 

Последние две строки, кажется мне неправильным, хотя я ожидаю, что я просто неправильно понять что-то. Мои рассуждения заключается в следующем:

1. Если мы имеем a -> f и a, то мы имеем f.
2. Если у нас есть TList h t, то у нас есть h и t.
3. Поскольку у нас есть TApplies f h t r, у нас есть fundep f h t -> r.
4. Поэтому, поскольку у нас есть f, h и t, у нас есть r.

Это подразумевает, что функциональная зависимость является satified. Может ли кто-то указать на недостаток в моей логике, а также, возможно, предложить более подходящий выбор функциональной зависимости? (Обратите внимание, что что-то вроде разрешено GHC, но, похоже, не дает большого количества указаний по типу.)

Answer 1

Во-первых, я понятия не имею, почему вы используете такой сложный тип данных, поэтому я буду использовать упрощенный для решения вашего вопроса. Тем не менее, этот же принцип применяется к вашему точному сценарию.

Определите тип данных просто:

data TList (xs :: [*]) where 
    Nil :: TList '[] 
    (:.) :: x -> TList xs -> TList (x ': xs) 

infixr 4 :. 

Тогда ваш класс имеет один меньше параметра типа:

class TApplies f (xs :: [*]) r | f xs -> r where ... 

и проблематичный экземпляр будет выглядеть

instance TApplies g ys q => TApplies (y -> g) (y ': ys) q where 

Теперь рассмотрим ошибка возникает (по сути, такая же, как и в вашем вопросе) - а именно, обратите внимание, что в ней говорится: «Th условие покрытия не выполняется в классе «TApplies». Итак, что это за «Состояние покрытия»? user guide имеет право:

Состояние покрытия. Для каждой функциональной зависимости tvsleft -> tvsright класса, каждая переменная типа в S (tvsright) должна отображаться в S (tvsleft), где S является заменой, сопоставляющей каждую переменную типа в объявлении класса соответствующему типу в заявке .

Это слишком технический, но в основном это говорит о том, что набор переменных типа в правой части - в этом случае, то есть {q}, должно быть подмножеством множества переменных в левой стороне - здесь {y, g, ys}. Это, очевидно, не так.

Вы заметите, что условие покрытия ничего не говорит о контексте экземпляра. Это корень вашей проблемы! Контекст - это , а не, который учитывается при определении функциональной зависимости. Я думаю, вы согласитесь со мной в том, что он явно не подходит для экземпляра instance TApplies (y -> g) (y ': ys) q where ..., что и видит компилятор.

Решение прост: добавьте {-# LANGUAGE UndecidableInstances #-} в начало вашего файла. Цель условия покрытия, среди прочего, заключается в том, чтобы обеспечить разрешение экземпляра. Если вы включите UndecidableInstances, вы говорите: «Поверьте мне, оно завершается».

---

В качестве побочного примечания, нынешняя формулировка не очень приятна в использовании. Например, tApply (+) (1 :. 2 :. Nil) создает ошибку «неоднозначного типа» или что-то в этом роде. Хуже того, tApply (+) (1 :. "s" :. Nil) создает ту же самую ошибку «неоднозначного типа»! Не очень полезно для тех, кто пытается написать код с этим классом. Вам нужно будет указывать мономорфные сигнатуры типа везде, чтобы заставить его работать как есть.

Решение состоит в том, чтобы случайно декларации экземпляра к следующему:

instance (a ~ a') => TApplies a '[] a' where 
instance (TApplies g ys q, y ~ y') => TApplies (y -> g) (y' ': ys) q where 

Затем первый случай компилируется как есть, тип недобросовестный умирает, и печатает «3». Во втором случае вы получаете No instance for (Num [Char]), что действительно полезно.

Причина, по которой это работает, опять же, что разрешение экземпляра касается только главы экземпляра, а не контекста. instance TApplies (y -> g) (y' ': ys) q - это то, что видит компилятор, и, очевидно, y и y' могут быть любыми, несвязанными типами. Только в конце, когда пришло время распечатать значение, компилятор должен решить ограничение y ~ y', после чего вы просто имеете выражение (+) 1 2.

---

Вы можете реализовать свой тип без типов данных следующим образом:

{-# LANGUAGE GADTs #-} 
data Cons a b 
data Nil 

data TList xs where 
    Nil :: TList Nil 
    (:.) :: x -> TList xs -> TList (Cons x xs) 

Там нет никакой реальной причины, чтобы сделать это, однако, так как DataKinds не может сломаться в противном случае рабочего кода.