Non riesco a far funzionare il mio tipo Dinamico giocattolo basato su GADT con i tipi parametrici

Question

Quindi, per aiutarmi a comprendere alcune delle funzioni e dei concetti Haskell/GHC più avanzati, ho deciso di adottare un'implementazione basata su GADT funzionante dati digitati dinamicamente ed estenderli per coprire tipi parametrici. (Mi scuso per la lunghezza di questo esempio.)

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

compilazione di questo, però, non riesce sull'ultima riga (i miei numeri di riga non corrispondono all'esempio):

../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 

Il modo in cui ho letto questo, il compilatore non è in grado di capire che in Inductive :: Equal a b -> Equal (f a) (f b), a e deve essere uguale per i valori non di fondo. Così ho cercato Inductive :: Equal a a -> Equal (f a) (f a), ma che non riesce anche, nella definizione di 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)' 

Modifica del tipo di matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b) per produrre matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a) non funziona (basta leggere come una proposizione). Nemmeno lo matchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a) (un'altra proposizione banale, e questo a quanto ho capito, richiederebbe agli utenti di fromDynamic' to know the un in the tipoRep a contained in the dinamico`).

Quindi, sono perplesso. Qualche suggerimento su come andare avanti qui?

Answer 1

Il problema è che il motivo jolly del modello perde informazioni di uguaglianza. Se codifichi l'induzione in questo modo, non puoi scrivere una raccolta (finita) di pattern che copra tutti i casi. La soluzione è spostare l'induzione dal tipo di dati in un valore definito. I cambiamenti rilevanti simile a questa:

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 

questo modo i modelli in fromDynamic' sono esaustive, ma non hanno alcun jolly di informazione in perdita.