No puedo hacer que mi tipo dinámico de juguete basado en GADT trabaje con tipos paramétricos

Question

Para ayudarme a entender algunas de las funciones y conceptos más avanzados de Haskell/GHC, decidí implementar una implementación de GADT basada en datos tipeados dinámicamente y ampliarlos para cubrir tipos paramétricos. (Me disculpo por la longitud de este ejemplo.)

{-# LANGUAGE GADTs #-} 

module Dyn (Dynamic(..), 
      toDynamic, 
      fromDynamic 
      ) where 

import Control.Applicative 

---------------------------------------------------------------- 
---------------------------------------------------------------- 
-- 
-- Equality proofs 
-- 

-- | The type of equality proofs. 
data Equal a b where 
    Reflexivity :: Equal a a 
    -- | Inductive case for parametric types 
    Induction :: Equal a b -> Equal (f a) (f b) 

instance Show (Equal a b) where 
    show Reflexivity = "Reflexivity" 
    show (Induction proof) = "Induction (" ++ show proof ++ ")" 

---------------------------------------------------------------- 
---------------------------------------------------------------- 
-- 
-- Type representations 
-- 

-- | Type representations. If @x :: TypeRep a@, then @x@ is a singleton 
-- value that stands in for type @a@. 
data TypeRep a where 
    Integer :: TypeRep Integer 
    Char :: TypeRep Char 
    Maybe :: TypeRep a -> TypeRep (Maybe a) 
    List :: TypeRep a -> TypeRep [a] 

-- | Typeclass for types that have a TypeRep 
class Representable a where 
    typeRep :: TypeRep a 

instance Representable Integer where typeRep = Integer 
instance Representable Char where typeRep = Char 

instance Representable a => Representable (Maybe a) where 
    typeRep = Maybe typeRep 

instance Representable a => Representable [a] where 
    typeRep = List typeRep 


-- | Match two types and return @Just@ an equality proof if they are 
-- equal, @Nothing@ if they are not. 
matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b) 
matchTypes Integer Integer = Just Reflexivity 
matchTypes Char Char = Just Reflexivity 
matchTypes (List a) (List b) = Induction <$> (matchTypes a b) 
matchTypes (Maybe a) (Maybe b) = Induction <$> (matchTypes a b) 
matchTypes _ _ = Nothing 


instance Show (TypeRep a) where 
    show Integer = "Integer" 
    show Char = "Char" 
    show (List a) = "[" ++ show a ++ "]" 
    show (Maybe a) = "Maybe (" ++ show a ++ ")" 


---------------------------------------------------------------- 
---------------------------------------------------------------- 
-- 
-- Dynamic data 
-- 

data Dynamic where 
    Dyn :: TypeRep a -> a -> Dynamic 

instance Show Dynamic where 
    show (Dyn typ val) = "Dyn " ++ show typ 

-- | Inject a value of a @Representable@ type into @Dynamic@. 
toDynamic :: Representable a => a -> Dynamic 
toDynamic = Dyn typeRep 

-- | Cast a @Dynamic@ into a @Representable@ type. 
fromDynamic :: Representable a => Dynamic -> Maybe a 
fromDynamic = fromDynamic' typeRep 

fromDynamic' :: TypeRep a -> Dynamic -> Maybe a 
fromDynamic' target (Dyn source value) = 
    case matchTypes source target of 
     Just Reflexivity -> Just value 
     Nothing -> Nothing 
     -- The following pattern causes compilation to fail. 
     Just (Induction _) -> Just value 

Compilación de esto, sin embargo, un error en la última línea (mis números de línea no coinciden con el ejemplo):

../src/Dyn.hs:105:34: 
    Could not deduce (a2 ~ b) 
    from the context (a1 ~ f a2, a ~ f b) 
     bound by a pattern with constructor 
       Induction :: forall a b (f :: * -> *). 
           Equal a b -> Equal (f a) (f b), 
       in a case alternative 
     at ../src/Dyn.hs:105:13-23 
     `a2' is a rigid type variable bound by 
      a pattern with constructor 
      Induction :: forall a b (f :: * -> *). 
          Equal a b -> Equal (f a) (f b), 
      in a case alternative 
      at ../src/Dyn.hs:105:13 
     `b' is a rigid type variable bound by 
      a pattern with constructor 
      Induction :: forall a b (f :: * -> *). 
         Equal a b -> Equal (f a) (f b), 
      in a case alternative 
      at ../src/Dyn.hs:105:13 
    Expected type: a1 
     Actual type: a 
    In the first argument of `Just', namely `value' 
    In the expression: Just value 
    In a case alternative: Just (Induction _) -> Just value 

La forma en que leo esto, el compilador no puede darse cuenta de que en Inductive :: Equal a b -> Equal (f a) (f b), a y b debe ser igual para valores que no sean inferiores. Así que he intentado Inductive :: Equal a a -> Equal (f a) (f a), pero esto también falla, en la definición de matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b):

../src/Dyn.hs:66:60: 
    Could not deduce (a2 ~ a1) 
    from the context (a ~ [a1]) 
     bound by a pattern with constructor 
       List :: forall a. TypeRep a -> TypeRep [a], 
       in an equation for `matchTypes' 
     at ../src/Dyn.hs:66:13-18 
    or from (b ~ [a2]) 
     bound by a pattern with constructor 
       List :: forall a. TypeRep a -> TypeRep [a], 
       in an equation for `matchTypes' 
     at ../src/Dyn.hs:66:22-27 
     `a2' is a rigid type variable bound by 
      a pattern with constructor 
      List :: forall a. TypeRep a -> TypeRep [a], 
      in an equation for `matchTypes' 
      at ../src/Dyn.hs:66:22 
     `a1' is a rigid type variable bound by 
      a pattern with constructor 
      List :: forall a. TypeRep a -> TypeRep [a], 
      in an equation for `matchTypes' 
      at ../src/Dyn.hs:66:13 
    Expected type: TypeRep a1 
     Actual type: TypeRep a 
    In the second argument of `matchTypes', namely `b' 
    In the second argument of `(<$>)', namely `(matchTypes a b)' 

Cambiar el tipo de matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b) para producir matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a) no funciona (solo leerlo como una proposición). Tampoco lo hace matchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a) (otra proposición trivial, y esto como lo entiendo requeriría usuarios de fromDynamic' to know the a in the TypeRep a contained in the Dynamic`).

Así que, estoy perplejo. ¿Alguna sugerencia sobre cómo avanzar aquí?

Answer 1

El problema es que el patrón de comodín de su patrón pierde información de igualdad. Si codifica la inducción de esta manera, no puede escribir una colección (finita) de patrones que cubra todos los casos. La solución es mover la inducción desde su tipo de datos a un valor definido. Los cambios pertinentes tener este aspecto:

data Equal a b where 
    Reflexivity :: Equal a a 

induction :: Equal a b -> Equal (f a) (f b) 
induction Reflexivity = Reflexivity 

matchTypes (List a) (List b) = induction <$> matchTypes a b 
matchTypes (Maybe a) (Maybe b) = induction <$> matchTypes a b 

fromDynamic' :: TypeRep a -> Dynamic -> Maybe a 
fromDynamic' target (Dyn source value) = 
    case matchTypes source target of 
     Just Reflexivity -> Just value 
     Nothing -> Nothing 

esta manera los patrones en fromDynamic' son exhaustivos, pero no tienen ningún comodín de información-perder.