problema quando si mescolano le classi di tipo e le famiglie tipo

Question

Questo codice compila bene:

{-# 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)) 

ma non appena aggiungo GHC R predicato fallisce:

{-# 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)) 

lamentando che:

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

cosa significa e (cosa più importante) come lo risolvo?

Grazie

Answer 1

Le famiglie di tipi sono a senso unico: è possibile espandere Rec a per il tipo calcolato, ma non è possibile (in modo univoco) passare dall'espansione a Rec a. Ciò rende le applicazioni delle funzioni di tipo inadatte alle firme di istanza, poiché non possono mai attivare l'istanza da applicare.

Si potrebbe provare invece:

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

Questo significa un'altra cosa: si dice qualsiasi funzione b -> (c, reca) è un esempio, e poi quando si è irrevocabilmente abbinate, i controlli del compilatore che Rec a ~ reca. Ma questo potrebbe essere abbastanza buono da volere nel tuo caso.

Answer 2

Rec non è un costruttore di tipo; è una funzione di tipo. Forse puoi usarlo solo nel tipo di un valore di definizione del tipo, non in una dichiarazione di classe? Sto indovinando selvaggiamente qui; Non capisco tutte le regole per le famiglie di tipi.

non so come risolvere il problema, ma alcune cose da provare sono:

• Sbarazzarsi della classe Sel ed appena definisco type family Res a s b :: *. Utilizzare type instance anziché il meccanismo di classe.

• È a malapena possibile che l'inserimento del tipo Rec iniettore con data sia di aiuto, ma non credo.

• Riduci il numero più piccolo di estensioni della lingua che potrebbero funzionare — renderà più semplice per gli altri l'assistenza e potrebbe aiutare anche il compilatore.

Answer 3

vuol dire che non ti è permesso di utilizzare tipo famiglie synomym quando si dichiara istanze di tipo. Vedere la sezione "Type families and instance declarations" del manuale GHC.

L'unico modo per risolverlo è refactoring in modo da non averne bisogno in qualche modo.