Как я могу выразить это ограничение?

Я хотел бы выразить Constraint по типам типа k -> k -> Type, что может быть сформулировано на английском языке как:

Тип s такой, что для всех x x', y и y', где Coercible x x' и Coercible y y', Coercible (s x y) (s x' y')

Или на еще более простом английском языке:

Тип s, который всегда является принудительным, если два его параметра являются принудительными.

Последний кажется уже мучительно близким к haskell, и у меня есть код, который действительно выглядит так, как будто он должен это делать:

type Representational2 (s :: k -> k -> Type) =
  forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y')

Однако это не работает, ghc хочет, чтобы Coercible (s x y) (s x' y') был типом, но это Constraint (включены ConstraintKinds и QuantifiedConstraints).

• Expected a type, but
  ‘Coercible (s x y) (s x' y')’ has kind
  ‘Constraint’
• In the type ‘forall x x' y y'.
               (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y')’
  In the type declaration for ‘Representational2’

Я не совсем понимаю, что происходит, но я понимаю, что ghc не нравится, когда Constraint находится справа от => внутри type. Так как я могу создавать псевдонимы типов с Constraint видами и я могу создавать псевдонимы type с =>, проблем нет.

В чем проблема и как я могу выразить это ограничение для ghc приемлемым для него образом?


haskell constraint-kinds
person Éamonn Olive    schedule 26.02.2020    source источник

Ответы (1)


arrow_upward
6
arrow_downward

Это работает:

{-# LANGUAGE ConstraintKinds, PolyKinds, RankNTypes, QuantifiedConstraints #-}

import Data.Kind
import Data.Coerce

type Representational2 (s :: k -> k -> Type) =
  forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y') :: Constraint

Все, что я сделал, это добавил :: Constraint к вашему типу. Поскольку GHC уже знал, что тип RHS был Constraint (из-за сообщения об ошибке), у меня действительно нет хорошего объяснения, почему это заставляет его работать.

Изменить: у меня есть частичное объяснение: добавив такую ​​подпись в RHS, ваш синоним типа теперь имеет CUSK (см. вики GHC):

  • Синоним типа имеет CUSK тогда и только тогда, когда все его переменные типа и его RHS аннотированы видами.
person Joseph Sible-Reinstate Monica    schedule 26.02.2020
comment
Спасибо, ваш ответ полезен, и я могу двигаться дальше, но мне действительно любопытно, почему это вообще помогает. - person Éamonn Olive; 26.02.2020
comment
@SriotchilismO'Zaic Я нашел частичное объяснение. - person Joseph Sible-Reinstate Monica; 26.02.2020