Специальное представление времени выполнения []?

Рассмотрим простое определение вектора, проиндексированного по длине:

data Nat = Z | S Nat 

infixr 5 :> 
data Vec (n :: Nat) a where 
  V0 :: Vec 'Z a 
  (:>) :: a -> Vec n a -> Vec ( 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 и []. Хотя в этом случае pair2tup segfaults, а не всегда возвращает пустой список.

Кажется, он асимметричен по отношению к типам, которые используют "встроенный" синтаксис. Вернемся к примеру Vec, следуя

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

отлично работает! GADT действительно не особенный.

Вопрос: как представления представления типов, которые используют "встроенный" синтаксис, отличаются от тех, которые этого не делают?

В качестве альтернативы, как написать однозадачное принуждение от Vec n a до [a]? Это не отвечает на вопрос, но решает проблему.

Тестирование проводилось с помощью GHC 7.10.3.

Как заметил комментатор, это поведение присутствует только при интерпретации. При компиляции все функции работают должным образом. Вопрос по-прежнему применяется, только для представления времени выполнения при интерпретации.

Ответ 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"

Модули, содержащие [] и (,), скомпилированы, что приводит к тому, что их представление во время выполнения отличается от изоморфных типов данных в интерпретируемых модулях. Согласно Симону Марлоу, в потоке, который я связал, интерпретируемые модули добавляют аннотации к отладчику. Я думаю, что это также объясняет, почему tup2pair работает, а pair2tup - нет: отсутствующие аннотации не являются проблемой для интерпретируемых модулей, но скомпилированные модули задыхаются над дополнительными аннотациями.

-fobject-code имеет некоторые недостатки: более длительное время компиляции, только приносит экспортируемые функции в область видимости, но имеет дополнительное преимущество в том, что запуск кода происходит намного быстрее.

Ответ 2

Чтобы ответить только на ваш альтернативный вопрос, вы можете создать 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 ( n) a
a >:> (Vec as) = Vec (a : as)

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

Пока конструктор Vec не входит в область видимости (поэтому для построения векторов можно использовать только v0 и >:>), инвариант, который не может быть нарушен, номер уровня уровня представляет собой длину.

(Этот подход определенно имеет мои предпочтения над unsafeCoerce, поскольку все, что с unsafeCoerce может ломаться при каждом обновлении GHC или на разных платформах.)