Приведение экземпляров классов типов с фантомным параметром - PullRequest
Новая
       66

Приведение экземпляров классов типов с фантомным параметром

0 голосов
/ 02 октября 2018

У меня есть 

{-# LANGUAGE RankNTypes, TypeInType #-}

import Data.Coerce
import Data.Kind

newtype IFix f i = IFix { unIFix :: f (IFix f) i }

class IFunctor (f :: (i -> Type) -> i -> Type) where
  imap :: (forall i'. a i' -> b i') -> (forall i'. f a i' -> f b i')

f :: IFunctor f => forall i. IFix f i -> IFix f i
f = undefined

g :: IFunctor f => forall i. IFix f i -> IFix f i
g = IFix . imap f . unIFix

h :: IFunctor f => forall i. IFix f i -> IFix f i
h = coerce . imap f . coerce

i :: IFunctor f => forall i. IFix f i -> IFix f i
i = coerce (imap f)

, где IFix - фиксированная точка уровня типа конструкторов индексированного типа, i - индекс (фантомный параметр), IFunctor - класс такого индексированногоконструкторы типов, которые на самом деле являются функторами, f - это просто случайная функция, g, h, i пытаются распространить f в оболочке IFix.Примечание: это упрощенный пример, и я часто сталкиваюсь с подобными проблемами в других настройках, где ручная перемотка становится немного утомительной (для одной я хотел бы избежать отображения функции unwrap-rewrap на списки или другие структуры). 

input:18:5: error:
    • Couldn't match representation of type ‘f (IFix f) i’
                               with that of ‘f0 (IFix f1) i0’
        arising from a use of ‘coerce’
   |
18 | h = coerce . imap f . coerce
   |     ^^^^^^

input:21:5: error:
    • Couldn't match representation of type ‘f (IFix f) i’
                               with that of ‘f2 (IFix f3) i1’
        arising from a use of ‘coerce’
   |
21 | i = coerce (imap f)
   |     ^^^^^^^^^^^^^^^

и, честно говоря, я не очень удивлен, но, поскольку я не вижу под капотом принуждений, мне интересно, есть ли способ изменить мои определения, чтобы можно было применить coerce?Я попытался RoleAnnotations, но

  1. type role IFix nominal phantom недопустимо
  2. Я понятия не имею, как требовать роли типов для класса типов (и я боюсь, что нет никакого способа, так какВ документе упоминается, что классы типов предполагают, что параметры являются номинальными)

Поэтому мой вопрос заключается в том, есть ли способ заставить принудительную работу работать в этом параметре, и если нет, есть ли серьезные причины, почему нет, или это простоограничение текущей роли вывода реализации.Мой наивный взгляд заставляет меня думать, что класс типов может налагать ограничения на роли аргументов, и экземпляры должны будут удовлетворять этому ограничению.Есть ли хороший источник некоторых полезных уловок принуждения?

1 Ответ

0 голосов
/ 02 октября 2018

На самом деле, g и h не проверяют тип, потому что тип imap f неоднозначен. 

imap :: IFunctor f => (a ~> b) -> (f a ~> f b)

Например, в h, imap f выводится следующеетип со свободными переменными объединения ?f0, ?f1, ?i0: 

h = coerce . (imap f :: ?f0 (IFix ?f1) ?i0 -> ?f0 (IFix ?f1) ?i0) . coerce

Обычно контекст позволяет нам создавать эти переменные, но здесь контекст: 

coerce . _ . coerce

обратите внимание на тип coerce :: Coercible a b => a -> b, который полностью разъединяет типы ввода и вывода в том, что касается вывода типа.

Мы можем использовать расширение ScopedTypeVariables для аннотирования imap f: 

h :: forall f i. IFunctor f => IFix f i -> IFix f i
h = coerce . (imap f :: f (IFix f) i -> f (IFix f) i) . coerce

или специализируйте coerce для ограничения его формы: 

type E a = a -> a

i :: IFunctor f => IFix f i -> IFix f i
i = (coerce :: E (f (IFix f) i) -> E (IFix f i)) (imap f)

coerce само по себе слишком общее, поэтому обычно приходится добавлять такие аннотации.Возможно, стоит иметь библиотеку общих специализаций.

...