使用 TypeInType 进行数据族实例的种类提升

Question

我正在尝试为强类型文件路径创建一个通用的自由类别（路径）和文件系统实例。我希望新的TypeInType扩展能够使这种更通用的路径类型成为可能，我在 2013 年的早期工作似乎需要将文件系统部分绑定到类别部分，但我遇到了一个问题，我似乎不这样做即使它被:kindGHCI接受，也可以将数据族实例提升到类型级别。

\n\n

我可能会遗漏一些明显的东西；我已经离开 Haskell 和编程有一段时间了，即使那时我也不是高级类型级编程的专家。

\n\n

我想要在 GHC 8 中实现的目标可能吗？

\n\n

代码

\n\n

{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}\n\nimport Data.Kind\n\ndata family Vertex g\n\ndata family Edge g (a :: Vertex g) (b :: Vertex g)\n\ndata Path g (a :: Vertex g) (b :: Vertex g) where\n    Nil :: Path g a a\n    Cons :: Edge g a b -> Path g b c -> Path g a c\n\ndata FileSystem\n\ndata instance Vertex FileSystem = Root | Home | Working | Directory | File\n\ndata instance Edge FileSystem where\n    RootDirectory :: Edge FileSystem Root Directory\n    HomeDirectory :: Edge FileSystem Home Directory\n    WorkingDirectory :: Edge FileSystem Working Directory\n    DirectoryName :: String -> Edge FileSystem Directory Directory\n    FileName :: String -> Edge FileSystem Directory File\n    FileExtension :: String -> Edge FileSystem File File\n

\n\n

编译错误

\n\n

$ ghc Path.hs \n[1 of 1] Compiling Main             ( Path.hs, Path.o )\n\nPath.hs:18:38: error:\n    \xe2\x80\xa2 Data constructor \xe2\x80\x98Root\xe2\x80\x99 cannot be used here\n        (it comes from a data family instance)\n    \xe2\x80\xa2 In the second argument of \xe2\x80\x98Edge\xe2\x80\x99, namely \xe2\x80\x98Root\xe2\x80\x99\n      In the type \xe2\x80\x98Edge FileSystem Root Directory\xe2\x80\x99\n      In the definition of data constructor \xe2\x80\x98RootDirectory\xe2\x80\x99\n

\n\n

GHCI

\n\n

注释掉Edge FileSystem代码编译的声明，我可以在 GHCi 中尝试一些东西。

\n\n

*Main> :set -XTypeInType -XTypeFamilies -XGADTs\n*Main> :k Edge FileSystem \nEdge FileSystem :: Vertex FileSystem -> Vertex FileSystem -> *\n*Main> :k Root\nRoot :: Vertex FileSystem\n*Main> :k Edge FileSystem Root Directory\nEdge FileSystem Root Directory :: *\n

\n

Answer 1

我认为你的解决方案过于复杂了。这些Node和Edge数据系列是导致错误的原因 -数据系列不会升级，即使有TypeInType- 并且它们不会在以下更简单的设计上添加任何内容：

infixr 5 :>
data Path (g :: k -> k -> *) (x :: k) (y :: k) where
    Nil :: Path g x x
    (:>) :: g x y -> Path g y z -> Path g x z

Path g是 s 的类型对齐列表g，使得gs 的类型像多米诺骨牌一样连接起来。或者，将类型视为集合，Path g是有向图的自由范畴中的态射类型，其中节点为k，边为g :: k -> k -> *。或者，将 视为g逻辑关系，Path g是g的自反传递闭包。

在本例中，k和g分别是以下FileSystemItem类型FileSystemPart：

data FileSystemItem = Root | Home | Working | Directory | File
data FileSystemPart (dir :: FileSystemItem) (base :: FileSystemItem) where
    RootDirectory    ::           FileSystemPart Root      Directory
    HomeDirectory    ::           FileSystemPart Home      Directory
    WorkingDirectory ::           FileSystemPart Working   Directory
    DirectoryName    :: String -> FileSystemPart Directory Directory
    FileName         :: String -> FileSystemPart Directory File
    FileExtension    :: String -> FileSystemPart File      File

type FileSystemPath = Path FileSystemPart

FileSystemPaths范畴中的态射集合也是如此FileSystemItem：

ghci> :k FileSystemPath
FileSystemPath :: FileSystemItem -> FileSystemItem -> *

例如：

myDocument :: FileSystemPath Home File
myDocument = HomeDirectory :> DirectoryName "documents" :> FileName "foo" :> FileExtension "hs" :> Nil

请注意，您不需要TypeInType或TypeFamilies重型机械 - 您只需要为文件系统本身PolyKinds定义 kind-polymorphicPath和DataKindsplus 。GADTs