Проблема при смешивании классов типов и семейств типа

Question

Этот код компилируется нормально:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, 
    UndecidableInstances, FlexibleContexts, EmptyDataDecls, ScopedTypeVariables, 
    TypeOperators, TypeSynonymInstances, TypeFamilies #-} 
class Sel a s b where 
    type Res a s b :: * 

instance Sel a s b where 
    type Res a s b = (s -> (b,s)) 

instance Sel a s (b->(c,a)) where 
    type Res a s (b->(c,a)) = (b -> s -> (c,s)) 

, но как только я добавить R предикат GHC не удается:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, 
    UndecidableInstances, FlexibleContexts, EmptyDataDecls, ScopedTypeVariables, 
    TypeOperators, TypeSynonymInstances, TypeFamilies #-} 
class Sel a s b where 
    type Res a s b :: * 

instance Sel a s b where 
    type Res a s b = (s -> (b,s)) 

class R a where 
    type Rec a :: * 
    cons :: a -> Rec a 
    elim :: Rec a -> a 
instance Sel a s (b->(c,Rec a)) where 
    type Res a s (b->(c,Rec a)) = (b -> s -> (c,s)) 

жалуется, что:

Illegal type synonym family application in instance: 
     b -> (c, Rec a) 
    In the instance declaration for `Sel a s (b -> (c, Rec a))' 

Что это значит и (самое главное), как я могу это исправить?

Благодаря

Answer 1

Тип семейства в одну сторону: вы можете развернуть Rec a его вычисленному типу, но вы не можете (однозначно) перейти от расширения обратно к Rec a. Это делает приложения типа функций непригодными, например, подписями, поскольку они никогда не могут инициировать применение экземпляра.

Вы можете попробовать вместо:

instance Rec a ~ reca => Sel a s (b->(c,reca)) 

Это означает что-то другое: он говорит, что любая функция b -> (c, reca) является экземпляром, а затем, когда он окончательно совпадающая, компилятор проверяет, что Rec a ~ reca. Но это может быть достаточно хорошим, чтобы хотеть в вашем случае.

Answer 2

Rec не является конструктором типа; это функция типа. Может быть, вы можете использовать его только в типе значения определения типа, а не в объявлении класса? Я угадываю дико здесь; Я не понимаю всех правил для семейств типов.

Я не знаю, как это исправить, но некоторые вещи, чтобы попробовать включают:

• Избавьтесь от класса Сел и просто определить type family Res a s b :: *. Используйте вместовместо класса.

• Едва ли возможно, что изготовление типа Rec инъекционного использования с помощью data поможет, но я так не думаю.

• Сокращение до наименьшего числа языковых расширений, которое могло бы работать —, это облегчит вам помощь другим, и это может помочь компилятору.

Answer 3

Это означает, что при объявлении экземпляров типа вам не разрешено использовать типы синонимичных семейств. См. Раздел "Type families and instance declarations" руководства GHC.

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