我无法让基于 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 -> 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 b)
的类型更改为matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a)
是行不通的(将其视为命题)。 matchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a)
也没有(另一个微不足道的提议,据我了解,这需要fromDynamic' to know the
ain the
TypeRep acontained in the
Dynamic` 的用户)。
所以,我被难住了。关于如何在此处前进的任何指示?
【问题讨论】:
你不能放弃Induction
构造函数并推导出相同的原理induction :: Eq a b -> 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 -> Equal a a
函数将所有 Induction
案例转换为 Reflexivity
来解决这个问题,但这也失败了,原因我不记得了......
您确实可以将这种类型的数据 data EqI :: * -> * -> * where ReflI :: EqI a a; RespI :: EqI a b -> EqI (f a) (f b)
标准化为这种类型的数据 data EqR :: * -> * -> * where Refl :: EqR a a
像这样:fact :: EqI a b -> EqR a b; fact ReflI = Refl; fact (RespI p) = case fact p of Refl -> Refl
@sacundim 我猜你可以让normalizeEqual :: Equal a b -> Equal a b
工作,但你建议的类型对我来说看起来很奇怪。你总是可以构造一个Equal a a
类型的值——提供a
等于其他东西的证明似乎是不必要的。以上是关于我无法让基于 GADT 的玩具动态类型与参数类型一起使用的主要内容,如果未能解决你的问题,请参考以下文章