這個GADT實際上是否具有代表性的類型角色

該數據類型可以有type role HCons' representational representational，允許使用coerce添加或刪除應用於元素的新類型，而不需要遍歷列表。這個GADT實際上是否具有代表性的類型角色

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

然而，對於這些列表的語法是不是像你一樣的有以下GADT

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

我有一類convert between these two representations，這樣Prime (HList [a,b]) ~ HCons' a (HCons' b HNil')。請問這種類型的產品是

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

安全嗎？

來源

2014-06-14 aavogt

FWIW，是的，我認爲是。但是我對角色的內部知識不夠了解，無法真正做出令人信服的論證。你的例子似乎是當前角色系統不夠充分表達的另一種情況。 – kosmikus

我不認爲自己存在轉換就足夠了。例如，下面也讓我一個GADT和強制轉換對類型之間轉換，但肯定不會是安全的直接要挾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)

我也可以平凡定義類似的UnFoo型功能到Prime。

我覺得這兩個例子之間的主要區別是，在礦山，Age和Int確實有相同的表示，而在你的'[]和e':l不具有相同的表示。

所以還是有這麼說的情況下，當你在標題中表明，該l有類型的角色代表性，因爲它是一種明顯的是HList l1和HList l2具有相同的表示，如果l1和l2具有相同的表示。

但是，由於理論上的表示是依賴於實現的，所以我認爲在GHC直接接受它之前，您絕對不會認爲這是絕對安全的。

來源

2014-06-24 05:57:29

我不太確定「如果l1和l2具有相同的表示形式，那麼HList l1和HList l2具有相同的表示方式是很明顯的」。我們可以寫出'HCons ::（el〜（e'：l））=> e - > HList l - > HList el'。那麼有可能ghc存儲'el〜（e'：l）'的東西，它引用了原來的'e，el，l'類型，而不是當前在構造函數中的類型？ – aavogt

即使如此，每個'HCons'仍然會有與其他'HCons'相同的曲面表示，不是嗎？所以如果'e'和'HList l'也具有相同的表示，那麼整個'HCons'會。 –

我認爲關鍵是''：''和''[]'是必須不同的具體類型，所以不會混淆'HCons'和'HNil'。我完全不知道如何準確地制定條件！ –

這個GADT實際上是否具有代表性的類型角色

回答

相關問題