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

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类型在运行时真的相同[].我也试着测试一下:

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和[].虽然在这种情况下,pair2tupsegfaults相反总是返回空列表.

对于使用"内置"语法的类型,它似乎始终是不对称的.回到Vec例子,以下

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

工作得很好!GADT真的不特别.

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

另外,一个人如何从写一个零成本的胁迫Vec n a到[a]？这不回答问题,但解决了问题.

使用GHC 7.10.3进行测试.

---

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

Answer 1

现在回答你的主要问题,这个主题似乎有答案:启动ghci -fobject-code:

$ 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 有一些缺点:编译时间较长,只在范围内引入导出的函数,但它具有运行代码更快的额外优势.