CODEWITHSUNDEEP
haskellfunctional-programmingghcdependent-typehigher-kinded-types
Vanson Samuel
Vanson Samuel

Reputation: 2089

How do I show relationships between type variables

For the types Door and Hallway:

 data DoorState :: Type where
   Opened :: DoorState
   Closed :: DoorState
   Locked :: DoorState
   deriving (Bounded, Enum, Eq, Ord, Show)

 data Door :: DoorState -> Type where
   Door :: {material :: String} -> Door s
   deriving (Show)

 data Hallway :: [DoorState] -> Type where
   Origin :: Hallway '[]
   Section :: Door ds -> Hallway dsl -> Hallway (ds : dsl)

This definition of appendHallway works:

 appendHallway :: forall (ds :: DoorState) (dsl :: [DoorState]). Door ds -> Hallway dsl -> Hallway (ds : dsl)
 appendHallway d rest = Section d rest

However this definition for appendHallway where the relationship between ds and dsl is being explicitly indicated in the forall section does not work:

 appendHallway :: forall t (ds :: t) (dsl :: [t]). (t ~ DoorState) => Door ds -> Hallway dsl -> Hallway (ds : dsl)
 appendHallway d rest = Section d rest

The error that is returned is as follows:

 error:
     • Expected kind ‘DoorState’, but ‘ds’ has kind ‘t’
     • In the first argument of ‘Door’, namely ‘ds’
       In the type signature:
         appendHallway :: forall t (ds :: t) (dsl :: [t]).
                          (t ~ DoorState) => Door ds -> Hallway dsl -> Hallway (ds : dsl)
     |
 351 | appendHallway :: forall t (ds :: t) (dsl :: [t]). (t ~ DoorState) => Door ds -> Hallway dsl -> Hallway (ds : dsl)
     |                                                                           ^^

The example above may be a little contrived, but there might be situations where indicating relationships between higher kinded type variables would be helpful or even necessary. Is this error a limitation of the current version of GHC or is the above nonsensical even in a future version of GHC? Is there another way to express the relationship between ds and dsl that would be accepted by GHC?

Upvotes: 1

Views: 105

Answers (2)

HTNW
HTNW

Reputation: 29193

The thing you have written is indeed nonsense. The constraints on the LHS of a => exist only on the value-level, in the same way things on the LHS of a -> exist only on the value-level. More specifically (though this is a faint memory), an instance of a ~ b "contains" within it a primitive type of kind a ~# b (in the same way a data Showable = forall s. Show s => Showable s holds a type of kind Type). You need the a ~# b to actually get anything done, but you'd need to unpack the a ~ b to get it. You cannot talk about the a ~ b, a value-level argument, in a type, though, in the same way you cannot talk about the DoorState in DoorState -> Door _can'tTalkAboutTheDoorState.

What you can do is this. Define

type family Cast (x :: (a :: Type)) :: (b :: Type) where
   Cast x = x
-- this seems strange, but realize the equation is actually
-- Cast @a @a (x :: a) = (x :: a)
-- Cast-ing some type from one kind to another only goes through
-- when they're actually the same kind
-- can make a, b, or both explicit instead of implicit

Then

appendHallway :: forall t (ds :: t) (dsl :: [t]).
                 (t ~ DoorState) =>
                 Door (Cast ds) ->
                 Hallway (Cast dsl) ->
                 Hallway (Cast ds : Cast dsl)
appendHallway d rest = Section d rest

Whenever t ~ DoorState is known, the type family applications Cast @t @DoorState ds and Cast @[t] @[DoorState] dsl reduce to ds and dsl respectively.

Upvotes: 2

Daniel Wagner
Daniel Wagner

Reputation: 152997

Haskell has separate namespaces for computations, types, and kinds. When you write

forall (ds :: t). ...

the variable t is the kind-level variable, but when you write

t ~ DoorState => ...

the variable t is the type-level variable t, a completely unrelated variable. Indeed, all type equalities are at the type-level only; as far as I know there is no way to express kind equalities as constraints at all in current GHC Haskell.

Upvotes: 2

Related Questions