haskell - [] 类型的特殊运行时表示？

Question

考虑一个长度索引向量的简单定义:

data Nat = Z | S Nat 

infixr 5 :> 
data Vec (n :: Nat) a where 
  V0 :: Vec 'Z a 
  (:>) :: a -> Vec n a -> Vec ('S n) a 

自然，我会在某些时候需要以下功能:

vec2list :: Vec n a -> [a]  

然而，这个功能真的只是一个花哨的身份。我相信这两种类型的运行时表示是相同的，所以

vec2list :: Vec n a -> [a]  
vec2list = unsafeCoerce 

应该管用。唉，它没有:

>vec2list ('a' :> 'b' :> 'c' :> V0)
""

每个输入都只返回空列表。所以我认为我的理解不足。为了测试它，我定义了以下内容:

data List a = Nil | Cons a (List a) deriving (Show) 

vec2list' :: Vec n a -> List a 
vec2list' = unsafeCoerce 

test1 = vec2list' ('a' :> 'b' :> 'c' :> V0)

data SomeVec a = forall n . SomeVec (Vec n a) 

list'2vec :: List a -> SomeVec a 
list'2vec x = SomeVec (unsafeCoerce x) 

令人惊讶的是，这有效!那肯定不是 GADT 的问题(我最初的想法)。

我认为 List type 在运行时与 [] 完全相同.我也尝试对此进行测试:

list2list :: [a] -> List a 
list2list = unsafeCoerce 

test2 = list2list "abc" 

它有效!基于这个事实，我不得不得出结论 [a]和 List a必须具有相同的运行时表示。然而，以下

list2list' :: List a -> [a] 
list2list' = unsafeCoerce 

test3 = list2list' (Cons 'a' (Cons 'b' (Cons 'c' Nil)))

不起作用。 list2list'再次总是返回空列表。我相信“具有相同的运行时表示”必须是对称关系，所以这似乎没有意义。

我开始认为“原始”类型可能有些有趣 - 但我一直认为 []只是在句法上特殊，在语义上没有。似乎是这样的:

data Pair a b = Pair a b deriving (Show, Eq, Ord)  

tup2pair :: (a,b) -> Pair a b 
tup2pair = unsafeCoerce 

pair2tup :: Pair a b -> (a,b) 
pair2tup = unsafeCoerce 

第一个功能有效，第二个功能无效 - 与 List 的情况相同和 [] .虽然在这种情况下， pair2tup段错误而不是总是返回空列表。

对于使用“内置”语法的类型，它似乎始终是不对称的。返回 Vec例如，以下

list2vec :: [a] -> SomeVec a 
list2vec x = SomeVec (unsafeCoerce x) 

工作得很好! GADT 真的没有什么特别之处。

问题是: 使用“内置”语法的类型的运行时表示与不使用的类型有何不同？

或者，如何从 Vec n a 编写零成本强制转换？至 [a] ?这并没有回答问题，而是解决了问题。

使用 GHC 7.10.3 进行测试。

正如评论者所指出的，这种行为仅在解释时出现。编译后，所有函数都按预期工作。这个问题仍然适用，仅适用于解释时的运行时表示。

Answer 1

现在回答您的主要问题，this thread appears to have the answer : 用 -fobject-code 启动 ghci :

$ ghci /tmp/vec.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> print $ vec2list ('a' :> 'b' :> 'c' :> V0)
""

与 -fobject-code :

$ ghci -fobject-code /tmp/vec.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/vec.hs, /tmp/vec.o )
Ok, modules loaded: Main.
Prelude Main> print $ vec2list ('a' :> 'b' :> 'c' :> V0)
"abc"

包含 [] 的模块和 (,)都是编译的，这导致它们的运行时表示与解释模块中的同构数据类型不同。根据我链接的线程上的 Simon Marlow 所说，解释模块为调试器添加了注释。我想这也解释了为什么 tup2pair作品和 pair2tup没有:缺少注释对于解释模块来说不是问题，但是编译的模块会因额外的注释而窒息。
-fobject-code有一些缺点:编译时间更长，只会在作用域内引入导出的函数，但它还有一个额外的优点是运行代码要快得多。