Как мне показать отношения между переменными типа - PullRequest
Новая
       21

Как мне показать отношения между переменными типа

0 голосов
/ 25 января 2019

Для типов 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, где отношениемежду ds и dsl явно указывается в разделе forall, не работает: 

 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?

Ответы [ 2 ]

0 голосов
/ 26 января 2019

То, что вы написали, на самом деле бессмыслица.Ограничения на LHS для => существуют только на уровне значений, точно так же, как на LHS для -> существуют только на уровне значений.Более конкретно (хотя это слабое воспоминание), экземпляр a ~ b «содержит» в себе примитивный тип вида a ~# b (таким же образом data Showable = forall s. Show s => Showable s содержит тип вида Type).Вам нужно a ~# b, чтобы действительно что-то сделать, но вам нужно распаковать a ~ b, чтобы получить это.Вы не можете говорить о a ~ b, аргумент уровня значения, в типе, однако, вы не можете говорить о DoorState в DoorState -> Door _can'tTalkAboutTheDoorState.

Что вы можете сделать, это,Определите 

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 соответственно.

0 голосов
/ 26 января 2019

Haskell имеет отдельные пространства имен для вычислений, типов и видов. Когда ты пишешь 

forall (ds :: t). ...

переменная t является переменной уровня рода, но когда вы пишете 

t ~ DoorState => ...

переменная t - это переменная уровня типа t, совершенно не связанная переменная. Действительно, все равенства типов находятся только на уровне типов; насколько я знаю, в нынешнем GHC Haskell нет способа выразить добрые равенства как ограничения вообще.

...