如何显示类型变量之间的关系

Question

对于 Door 和 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)

appendHallway 的这个定义有效：

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

但是 appendHallway 的定义在 forall 部分中明确指出 ds 和 dsl 之间的关系不起作用：

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

返回错误如下：

 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)
     |                                                                           ^^

上面的例子可能有点做作，但在某些情况下，指示更高种类的类型变量之间的关系可能会有所帮助，甚至是必要的。这个错误是当前版本的 GHC 的限制，还是即使在未来版本的 GHC 中，上述错误也是荒谬的？是否有另一种表达 ds 和 dsl 之间关系的方式可以被 GHC 接受？

Answer 1

Haskell 具有用于计算、类型和种类的独立命名空间。当你写

forall (ds :: t). ...

变量t是kind-level变量，但是当你写

t ~ DoorState => ...

变量t是类型级变量t，一个完全不相关的变量。实际上，所有类型的相等性都只是在类型级别；据我所知，在当前的 GHC Haskell.

中，根本无法将种类平等表达为约束

Answer 2

你写的真是胡说八道。 => 的 LHS 上的约束仅存在于值级别上，就像 -> 的 LHS 上的事物仅存在于值级别上一样。更具体地说（虽然这是一个微弱的记忆），a ~ b "contains" 的一个实例在它里面是一种原始类型 a ~# b （以同样的方式 data Showable = forall s. Show s => Showable s 持有一个类型种类 Type)。您需要 a ~# b 才能真正完成任何事情，但您需要解压缩 a ~ b 才能获得它。但是，您不能在类型中谈论 a ~ b，一个值级参数，就像您不能在 DoorState -> Door _can'tTalkAboutTheDoorState.

中谈论 DoorState 一样

你能做的就是这个。定义

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

然后

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

每当 t ~ DoorState 已知时，类型族应用程序 Cast @t @DoorState ds 和 Cast @[t] @[DoorState] dsl 分别减少到 ds 和 dsl。

如何显示类型变量之间的关系

How do I show relationships between type variables

haskell

functional-programming

ghc

higher-kinded-types

dependent-type