这个GADT实际上是否具有代表性的类型角色 [英] does this GADT actually have type role representational

问题描述

这个数据类型可以有类型的角色HCons代表性，它允许使用 coerce 添加或删除新类型应用于元素，而不需要遍历列表。

  data HNil'= HNil'
数据HCons'ab = HCons'ab 
  

然而这些列表的语法并不如下面的GADT

  data HList（l :: [*]）其中
 HNil :: HList'[] 
 HCons :: e  - > HList l  - > HList（e'：l）
  

我有一个类在这两种表示之间进行转换，使得 Prime（HList [a，b]）〜HCons'a（HCons'b HNil'）。这个类是否使得

  coerceHList :: Coercible（Prime a）（Prime b）=> HList a  - > HList b 
 coerceHList = unsafeCoerce 
  

安全吗？

解决方案

我不认为自己存在转换就足够了。例如，以下内容也允许我在GADT和强制对类型之间进行转换，但直接强制GADT并不安全：

  newtype Age = Age Int 
 
 data Foo a where 
 I :: Bool  - > Int  - > Foo Int 
 A ::年龄 - >布尔 - > Foo年龄
 
类ConvFoo a其中
 toFoo ::（Bool，a） - > Foo a 
 fromFoo :: Foo a  - > （Bool，a）
 
实例ConvFoo Int其中
 toFoo（b，i）= I bi 
 fromFoo（I bi）=（b，i）
 
实例ConvFoo Age其中
 toFoo（b，a）= A ab 
 fromFoo（A ab）=（b，a）
  

我也可以简单地定义类似于 Prime 的 UnFoo 类型函数我认为这两个例子之间的主要区别在于，在我的 Age 和<$ c中，

$ c> Int 具有相同的表示形式，而在'[] 和 e'中：l 没有相同的表示形式。

因此，在标题中提到 l 具有代表型的角色，因为很明显， HList l1 和 HList l2 如果 l1 和 l2 具有相同的表示形式，则表示形式相同。

然而，由于理论上的表述是依赖于实现的在GHC直接接受它之前，我认为你绝对不会认为这是绝对安全的。

This data type can have type role HCons' representational representational, which allows using coerce to add or remove newtypes applied to the elements, without needing to traverse the list.

data HNil' = HNil'
data HCons' a b = HCons' a b

However the syntax for those lists is not as nice as those with the following GADT

data HList (l::[*]) where
    HNil  :: HList '[]
    HCons :: e -> HList l -> HList (e ': l)

I have a class to convert between these two representations, such that Prime (HList [a,b]) ~ HCons' a (HCons' b HNil'). Does that class make

coerceHList :: Coercible (Prime a) (Prime b) => HList a -> HList b
coerceHList = unsafeCoerce

safe?

解决方案

I don't think the existence of a conversion on its own is enough. For example, the following also lets me convert between a GADT and a coercible pair of types, but it certainly wouldn't be safe to directly coerce the GADT:

newtype Age = Age Int

data Foo a where
   I :: Bool -> Int -> Foo Int
   A :: Age -> Bool -> Foo Age

class ConvFoo a where
   toFoo :: (Bool, a) -> Foo a
   fromFoo :: Foo a -> (Bool, a)

instance ConvFoo Int where
   toFoo (b, i) = I b i
   fromFoo (I b i) = (b, i)

instance ConvFoo Age where
   toFoo (b, a) = A a b
   fromFoo (A a b) = (b, a)

I could also trivially define an UnFoo type function similar to Prime.

I think the key difference between the two examples is that in mine, Age and Int do have the same representation, whereas in yours '[] and e':l don't have the same representation.

So there's still a case for saying, as you suggest in the title, that l has type role representational, because it's kind of obvious that HList l1 and HList l2 have the same representations if l1 and l2 have the same representations.

However since in theory representations are implementation-dependent, I don't think you can ever consider this absolutely safe until GHC accepts it directly.

这篇关于这个GADT实际上是否具有代表性的类型角色的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！