GADT 기반 장난감을 사용할 수 없습니다. 파라 메트릭 유형으로 작동하는 동적 유형

Question

더 진보 된 Haskell/GHC 기능 및 개념을 이해할 수 있도록 GADT 기반 구현을 수행하기로 결정했습니다. 동적으로 형식이 지정된 데이터를 확장하고 매개 변수 유형을 포함하도록 확장합니다. (내 줄 번호가 예까지 일치하지 않는)이의

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

컴파일 (. 나는이 예제의 길이에 대해 사과) 그러나, 마지막 줄에 실패

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

내가 읽는 방식으로, 컴파일러는 Inductive :: Equal a b -> Equal (f a) (f b)에서 a과 b이 비 - 하단 값에 대해 같아야한다는 것을 알 수 없습니다. 그래서 Inductive :: Equal a a -> Equal (f a) (f a)을 시도했지만, 그 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)' 

가 (단지 명제로 읽기) 작동하지 않습니다 matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a)을 생산하는 matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b)의 유형을 변경. matchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a)도 없다. (또 다른 간단한 명제가 아니고, 나는 사용자가 fromDynamic' to know thein the TypeRep contained in the Dynamic을 요구할 것이라고 이해한다.).

그래서 나는 혼란 스럽습니다. 여기로 나아갈 수있는 방법에 대한 조언이 있습니까?

Answer 1

패턴의 와일드 카드 패턴이 평등 정보를 잃어 버리는 것이 문제입니다. 이러한 방식으로 유도를 인코딩하면 모든 경우를 다루는 (유한) 패턴 모음을 작성할 수 없습니다. 해결 방법은 데이터 유형에서 정의 된 값으로 유도를 이동하는 것입니다. fromDynamic'에서

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 

이 방법 패턴이 철저하지만, 어떤 정보 손실 와일드 카드가없는 : 관련 변화는 다음과 같습니다.