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

Question

我正在尝试为强类型文件路径创建一个通用的自由类别(路径)和一个文件系统实例。我希望新的 TypeInType 扩展能够使这种更通用的路径类型成为可能，其中 my earlier efforts早在 2013 年，似乎有必要将文件系统部分绑定(bind)到类别部分，但我遇到了一个问题，即我似乎不被允许将数据系列实例提升到种类级别，即使它已被 接受:kind 在 GHCI 中。

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

我想在 GHC 8 中实现的目标是否可行？

代码

{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}

import Data.Kind

data family Vertex g

data family Edge g (a :: Vertex g) (b :: Vertex g)

data Path g (a :: Vertex g) (b :: Vertex g) where
    Nil :: Path g a a
    Cons :: Edge g a b -> Path g b c -> Path g a c

data FileSystem

data instance Vertex FileSystem = Root | Home | Working | Directory | File

data instance Edge FileSystem where
    RootDirectory :: Edge FileSystem Root Directory
    HomeDirectory :: Edge FileSystem Home Directory
    WorkingDirectory :: Edge FileSystem Working Directory
    DirectoryName :: String -> Edge FileSystem Directory Directory
    FileName :: String -> Edge FileSystem Directory File
    FileExtension :: String -> Edge FileSystem File File

编译错误

$ ghc Path.hs 
[1 of 1] Compiling Main             ( Path.hs, Path.o )

Path.hs:18:38: error:
    • Data constructor ‘Root’ cannot be used here
        (it comes from a data family instance)
    • In the second argument of ‘Edge’, namely ‘Root’
      In the type ‘Edge FileSystem Root Directory’
      In the definition of data constructor ‘RootDirectory’

GHCi

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

*Main> :set -XTypeInType -XTypeFamilies -XGADTs
*Main> :k Edge FileSystem 
Edge FileSystem :: Vertex FileSystem -> Vertex FileSystem -> *
*Main> :k Root
Root :: Vertex FileSystem
*Main> :k Edge FileSystem Root Directory
Edge FileSystem Root Directory :: *

Answer 1

我认为您的解决方案过于复杂。这些 Node 和 Edge 数据系列是导致错误的原因 - data families aren't promoted ，即使使用 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 是一个 g 的类型对齐列表，这样 g 的类型就像多米诺骨牌一样连接起来。或者，将类型视为集合，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

因此，FileSystemPath 是 FileSystemItem 类别中的态射集合:

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

例如:

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

请注意，您不需要 TypeInType 或 TypeFamilies 重型机械 - 您只需要 PolyKinds 来定义种类多态Path、DataKinds 以及文件系统本身的 GADT。