我无法让基于 GADT 的玩具动态类型与参数类型一起使用

Posted

技术标签:

【中文标题】我无法让基于 GADT 的玩具动态类型与参数类型一起使用【英文标题】:I can't get my GADT-based toy Dynamic type to work with parametric types 【发布时间】:2012-06-14 15:57:08 【问题描述】:

因此,为了帮助我理解一些更高级的 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 -&gt; Equal (f a) (f b)ab 中非底部值必须相等。所以我试过Inductive :: Equal a a -&gt; Equal (f a) (f a),但也失败了,在matchTypes :: TypeRep a -&gt; TypeRep b -&gt; 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 -&gt; TypeRep b -&gt; Maybe (Equal a b) 的类型更改为matchTypes :: TypeRep a -&gt; TypeRep b -&gt; Maybe (Equal a a) 是行不通的(将其视为命题)。 matchTypes :: TypeRep a -&gt; TypeRep a -&gt; Maybe (Equal a a) 也没有(另一个微不足道的提议,据我了解,这需要fromDynamic' to know theain theTypeRep acontained in theDynamic` 的用户)。

所以,我被难住了。关于如何在此处前进的任何指示?

【问题讨论】:

你不能放弃Induction构造函数并推导出相同的原理induction :: Eq a b -&gt; Eq (f a) (f b); induction Reflexivity = Reflexivity吗? 【参考方案1】:

问题在于您的模式的通配符模式丢失了相等信息。如果以这种方式编码归纳,则无法编写涵盖所有情况的(有限)模式集合。解决方案是将归纳从您的数据类型移出到定义的值。相关更改如下所示:

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

这样fromDynamic' 中的模式是详尽无遗的,但没有任何丢失信息的通配符。

【讨论】:

是的,我一直怀疑通配符。有一次,我尝试通过编写 normalizeEqual :: Equal a b -&gt; Equal a a 函数将所有 Induction 案例转换为 Reflexivity 来解决这个问题,但这也失败了,原因我不记得了...... 您确实可以将这种类型的数据 data EqI :: * -&gt; * -&gt; * where ReflI :: EqI a a; RespI :: EqI a b -&gt; EqI (f a) (f b) 标准化为这种类型的数据 data EqR :: * -&gt; * -&gt; * where Refl :: EqR a a 像这样:fact :: EqI a b -&gt; EqR a b; fact ReflI = Refl; fact (RespI p) = case fact p of Refl -&gt; Refl @sacundim 我猜你可以让normalizeEqual :: Equal a b -&gt; Equal a b 工作,但你建议的类型对我来说看起来很奇怪。你总是可以构造一个Equal a a 类型的值——提供a 等于其他东西的证明似乎是不必要的。

以上是关于我无法让基于 GADT 的玩具动态类型与参数类型一起使用的主要内容,如果未能解决你的问题,请参考以下文章

Scala 中单例类型的 GADT 类型细化

使用 Haskell 类型族或 GADT 的模块化算术?

对类型的维度进行抽象

GADT 可以用来证明 GHC 中的类型不等式吗?

如何在Morte上代表任意GADT?

用于处理基于参数的不同数组类型的 C 向量