Biểu diễn thời gian chạy đặc biệt của loại []?

Question

xem xét định nghĩa đơn giản của một vector chiều dài-lập chỉ mục:

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 

Đương nhiên tôi sẽ tại một số điểm cần các chức năng sau:

vec2list :: Vec n a -> [a] 

Tuy nhiên, chức năng này thực sự chỉ là một bản sắc ưa thích. Tôi tin rằng các biểu diễn thời gian chạy của hai loại này giống nhau, vì vậy,

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

sẽ hoạt động. Than ôi, nó không:

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

Mọi đầu vào chỉ trả về danh sách trống. Vì vậy, tôi cho rằng sự hiểu biết của tôi là thiếu. Để kiểm tra nó, tôi xác định như sau:

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) 

Đáng ngạc nhiên là công trình này! Nó chắc chắn không phải là một vấn đề với GADT sau đó (suy nghĩ ban đầu của tôi).

Tôi nghĩ rằng loại List thực sự giống hệt nhau khi chạy đến []. Tôi cũng cố gắng thử nghiệm điều này:

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

test2 = list2list "abc" 

và nó hoạt động! Dựa trên thực tế này, tôi phải kết luận rằng [a] và List a phải có cùng một biểu diễn thời gian chạy. Tuy nhiên, sau

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

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

không hoạt động. list2list' lại luôn trả về danh sách trống. Tôi tin rằng "có biểu diễn thời gian chạy giống hệt nhau" phải là một mối quan hệ đối xứng, vì vậy điều này dường như không có ý nghĩa.

Tôi bắt đầu nghĩ rằng có thể có điều gì đó hài hước với các kiểu "nguyên thủy" - nhưng tôi luôn tin rằng [] chỉ là cú pháp đặc biệt, không phải ngữ nghĩa. Có vẻ như đó là trường hợp:

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 

Các công trình chức năng đầu tiên và lần thứ hai không - giống như trong trường hợp của List và []. Mặc dù trong trường hợp này, pair2tup segfaults như trái ngược với luôn luôn trả về danh sách trống.

Dường như là nhất quán không đối xứng đối với các loại sử dụng cú pháp "được tích hợp sẵn". Quay lại ví dụ Vec, sau đây

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

cũng hoạt động tốt! GADT thực sự không phải là đặc biệt.

Câu hỏi đặt ra là: cách trình bày thời gian chạy của các loại sử dụng cú pháp "dựng sẵn" khác với cú pháp không?

Cách khác, cách viết một lần ép buộc không có chi phí từ Vec n a đến [a]? Điều này không trả lời câu hỏi nhưng giải quyết được vấn đề.

Thử nghiệm được thực hiện với GHC 7.10.3.

---

Được ghi chú bởi người nhận xét, hành vi này chỉ xuất hiện khi diễn giải. Khi được biên dịch, tất cả các hàm hoạt động như mong đợi. Câu hỏi vẫn được áp dụng, chỉ để hiển thị thời gian chạy khi diễn giải.

Answer 1

Bây giờ để trả lời câu hỏi chính của bạn, this thread appears to have the answer: bắt đầu ghci với -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) 
"" 

Với -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" 

Các mô-đun chứa [] và (,) đều được biên dịch, làm cho biểu diễn thời gian chạy của chúng khác với các kiểu dữ liệu đẳng cấu trong các mô-đun diễn giải. Theo Simon Marlow về chủ đề tôi đã liên kết, các mô-đun diễn giải sẽ thêm chú thích cho trình gỡ lỗi. Tôi nghĩ rằng điều này cũng giải thích lý do tại sao tup2pair hoạt động và pair2tup không: thiếu chú thích không phải là vấn đề đối với mô-đun được diễn giải, nhưng các mô đun đã biên dịch bị nghẹt thở trên các chú thích bổ sung.

-fobject-code có một số nhược điểm: thời gian biên dịch dài hơn, chỉ mang lại chức năng được xuất trong phạm vi, nhưng có lợi thế bổ sung là chạy mã nhanh hơn nhiều.

Answer 2

Để trả lời duy nhất câu hỏi lựa chọn của bạn, bạn có thể tạo một newtype với một constructor không xuất khẩu để cung cấp cho một danh sách dài loại cấp và ép buộc zero-chi phí vào các danh sách:

{-# 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 

Chừng nào các nhà xây dựng Vec không nằm trong phạm vi (vì vậy chỉ có v0 và >:> có thể được sử dụng để xây dựng vectơ) bất biến mà số loại cấp đại diện cho độ dài không thể bị vi phạm.

(Cách tiếp cận này chắc chắn có sở thích của tôi trên unsafeCoerce, như bất cứ điều gì với unsafeCoerce có thể phá vỡ với tất cả các bản cập nhật của GHC hoặc trên các nền tảng khác nhau.)