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

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

应该可以。 las，它没有：

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

每个输入只是 returns 空列表。所以我认为我的理解是缺乏的。为了测试它，我定义了以下内容：

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' 再次总是 returns 空列表。我相信 "having identical runtime representations" 一定是一个对称关系，所以这似乎没有意义。

我开始认为 "primitive" 类型可能有一些有趣的地方 - 但我一直认为 [] 只是语法上的特殊，而不是语义上的特殊。好像是这样:

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 段错误而不是总是返回空列表。

对于使用 "built-in" 语法的类型，它似乎始终不对称。回到Vec例子，下面

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

也很好用！ GADT真的没什么特别的。

问题是：使用 "built-in" 语法的类型的运行时表示与不使用语法的类型有何不同？

或者，如何编写从 Vec n a 到 [a] 的零成本强制转换？这不能回答问题，但可以解决问题。

测试是使用 GHC 7.10.3 完成的。

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

Answer 1

要仅回答您的备选问题，您可以创建一个带有非导出构造函数的 newtype 来为列表提供类型级长度和对列表的零成本强制转换：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

module Vec (Nat(..), Vec, v0, (>:>), vec2list) where

data Nat = Z | S Nat

newtype Vec (n :: Nat) a = Vec { unVec :: [a] }

v0 :: Vec Z a
v0 = Vec []

infixr 5 >:>
(>:>) :: a -> Vec n a -> Vec ('S n) a
a >:> (Vec as) = Vec (a : as)

vec2list :: Vec n a -> [a]
vec2list (Vec as) = as

只要Vec构造函数不在范围内（所以只有v0和>:>可以用来构造向量）类型级数字代表的不变量长度不能违反。

（我肯定比 unsafeCoerce 更喜欢这种方法，因为任何带有 unsafeCoerce 的东西都可能随着 GHC 的每次更新或在不同平台上而中断。）

Answer 2

现在回答您的主要问题，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 有一些缺点：编译时间更长，只在范围内引入导出函数，但它有额外的优点，运行代码速度更快。

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

Special runtime representation of [] type?

haskell

ghc