Kind-promotion of data family instance with TypeInType

Question

I'm experimenting with making a generic free category (Path) and an instance for filesystems for strongly-typed filepaths. I was hoping the new TypeInType extension would make possible this more generalized path type where my earlier efforts back in 2013 seemed to necessitate tying the filesystem parts into the category parts, but I'm running into an issue where I don't seem to be permitted to promote a data family instance to the kind level even though it's accepted by :kind in GHCI.

I might be missing something obvious; I've been mostly away from Haskell and programming for some time now and even then I was hardly an expert at advanced type-level programming.

Is what I'm trying to achieve here possible in GHC 8?

The Code

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

Compilation Error

$ 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

Commenting out the Edge FileSystem declaration the code compiles and I can try some things in 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 :: *

For what purpose do you need data families? I don't yet see any need for them. — András Kovács
@AndrásKovács Interface design sensibilities and probably also being stuck in OOP-think. Nonetheless, I'm still curious why it doesn't work. — Dag

Benjamin Hodgson Benjamin Hodgson · Accepted Answer · 2016-09-09T14:24:35

I think you've overcomplicated your solution. Those Node and Edge data families are the cause of your error - data families aren't promoted, even with TypeInType - and they're not adding anything over the following simpler design:

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 is a type-aligned list of gs, such that the gs' types join up like dominoes. Or, viewing types as sets, Path g is the type of morphisms in the free category of a directed graph with nodes in k and edges in g :: k -> k -> *. Or, viewing g as a logical relation, Path g is g's reflexive transitive closure.

In this instance k and g are, respectively, the following FileSystemItem and FileSystemPart types:

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

So FileSystemPath is the set of morphisms in the category of FileSystemItems:

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

For example:

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

Note that you don't need the TypeInType or TypeFamilies heavy machinery for this - you only need PolyKinds to define the kind-polymorphic Path, and DataKinds plus GADTs for the filesystem itself.

Kind-promotion of data family instance with TypeInType

The Code

Compilation Error

GHCi

1 Answers