相关疑难解决方法(0)

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

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 …

举一个简单的例子，假设我想要一个类型来表示井字游戏标记：

data Mark = Nought | Cross

这与 Bool

Prelude> :info Bool
data Bool = False | True    -- Defined in ‘GHC.Types’

但是Coercible Bool Mark它们之间没有，即使我导入GHC.Types（我最初认为 GHC 可能需要Bool定义可见的位置），获得此实例的唯一方法似乎是通过newtype.

也许我可以这样来定义newtype Mark = Mark Bool和界定Nought，并Cross具有双向模式，我希望有东西比这更简单。