problema al mezclar las clases de tipos y familias de tipo

Question

Este código compila bien:

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

pero tan pronto como añado el GHC R predicado falla:

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

quejándose de que:

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

¿Qué significa y (lo más importante) cómo lo soluciono?

Gracias

Answer 1

Las familias de tipo de letra son unidireccionales: puede expandir Rec a a su tipo calculado, pero no puede (de forma única) pasar de la expansión a Rec a. Esto hace que las aplicaciones de las funciones tipo no sean aptas, por ejemplo, firmas, ya que nunca pueden desencadenar la aplicación para aplicar.

Usted podría intentar su lugar:

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

Esto significa otra cosa: dice cualquier función b -> (c, reca) es un ejemplo, y luego, cuando se ha emparejados de forma irrevocable, el compilador comprueba que Rec a ~ reca. Pero esto podría ser lo suficientemente bueno como para querer en tu caso.

Answer 2

Rec no es un constructor de tipos; es una función de tipo. ¿Tal vez solo puede usarlo en el tipo de valor de definición de tipo, no en una declaración de clase? Estoy adivinando locamente aquí; No entiendo todas las reglas para las familias tipográficas.

no sé cómo solucionarlo, pero algunas cosas para tratar de incluir:

• Deshacerse de la clase Sel y justo defino type family Res a s b :: *. Use type instance en lugar del mecanismo de clase.

• Es apenas posible que hacer el tipo Rec inyectar usando data ayudará, pero no lo creo.

• Reduzca al mínimo número de extensiones de idioma que posiblemente podrían funcionar — hará que sea más fácil para otros ayudarlo, y también podría ayudar al compilador.

Answer 3

Significa que no está permitido utilizar familias de tipo synomym al declarar instancias de tipo. Consulte la sección "Type families and instance declarations" del manual de GHC.

La única forma de solucionarlo es refactorizar para no necesitarlo de alguna manera.