Использование Type.Equality с PolyKinds

Этот код компиляции представляет собой свернутый пример этого кода из ответа на эта проблема с syntactic-2.0. Я также использую определение sameModType, полученное из sameNat в Data.Type.Equality.

Я использовал это решение без проблем, но я хотел бы, чтобы модуль q был полиморфным, с конкретной целью сделать Proxy (nat :: Nat) просто nat :: Nat (при этом можно было использовать модули вида *).

{-# LANGUAGE GADTs, 
             MultiParamTypeClasses, 
             FunctionalDependencies, 
             FlexibleContexts, 
             FlexibleInstances,
             TypeOperators, 
             ScopedTypeVariables,
             DataKinds,
             KindSignatures #-}

import Data.Tagged
import Data.Proxy
import Data.Type.Equality
import Data.Constraint
import Unsafe.Coerce
import GHC.TypeLits

newtype Zq q i = Zq i

data ZqType q
  where
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

class (Integral i) => Modulus a i | a -> i where
    value :: Tagged a i

instance (KnownNat q) => Modulus (Proxy (q :: Nat)) Int where 
    value = Tagged $ fromIntegral $ natVal (Proxy :: Proxy q)

sameModType :: (Modulus p i, Modulus q i) 
            => Proxy p -> Proxy q -> Maybe (p :~: q)
sameModType p q | (proxy value p) == (proxy value q) = 
                     Just $ unsafeCoerce Refl
                | otherwise = Nothing

typeEqSym :: ZqType p -> ZqType q -> Maybe (Dict (p ~ q))
typeEqSym (ZqType p) (ZqType q) = do
        Refl <- sameModType p q  -- LINE 39
        return Dict              -- LINE 40

Но когда я добавляю расширение -XPolyKinds к приведенному выше коду, я получаю несколько ошибок компиляции:

Foo.hs:39:36:
    Could not deduce (k1 ~ k)
    ...
    Expected type: Proxy q0
      Actual type: Proxy q2
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the second argument of ‘sameFactoredType’, namely ‘q’
    In a stmt of a 'do' block: Refl <- sameFactoredType p q

Foo.hs:40:16:
    Could not deduce (k ~ k1)
    ...
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the first argument of ‘return’, namely ‘Dict’
    In a stmt of a 'do' block: return Dict
    In the expression:
      do { Refl <- sameFactoredType p q;
           return Dict }

Foo.hs:40:16:
    Could not deduce (q1 ~ q2)
    ...
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the first argument of ‘return’, namely ‘Dict’
    In a stmt of a 'do' block: return Dict
    In the expression:
      do { Refl <- sameFactoredType p q;
           return Dict }

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


haskell higher-kinded-types ghc
person crockeea    schedule 20.05.2014    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Я не знаю, это то, что вы ищете, но вы можете просто указать тип основного аргумента для последующего использования:

data ZqType q k where
  ZqType :: Modulus q Int => Proxy (q :: k) -> ZqType (Zq q Int) ('KProxy :: KProxy k)

typeEqSym :: ZqType p k -> ZqType q k -> Maybe (Dict (p ~ q))
typeEqSym (ZqType p) (ZqType q) = do
        Refl <- sameModType p q  
        return Dict              

instance Modulus Int Int where 
instance Modulus (n :: Nat) Int where

KProxy должно быть в Data.Proxy, но это всего лишь data KProxy (x :: *) = KProxy.

Надуманный пример:

>let x = ZqType (Proxy :: Proxy (10 :: Nat))
>let y = ZqType (Proxy :: Proxy Int)
>typeEqSym x y
<interactive>:25:13:
    Couldn't match kind `*' with `Nat'
    Expected type: ZqType (Zq Int Int) 'KProxy
      Actual type: ZqType (Zq Int Int) 'KProxy
    In the second argument of `typeEqSym', namely `y'
    In the expression: typeEqSym x y
person user2407038    schedule 20.05.2014

arrow_upward
5
arrow_downward

Я могу объяснить проблему, но поскольку я не совсем уверен, что вы хотите сделать, я не уверен, как лучше всего это исправить.

Проблема в определении ZqType:

data ZqType q
  where
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

Несколько вводит в заблуждение, что параметр типа ZqType называется q. Это GADT, и параметры типа не имеют ничего общего с параметрами типа, появляющимися в конструкторах. Вместо этого я предпочитаю добрую подпись. Что за ZqType? Ну, Zq q Int — это тип данных, поэтому он имеет тип *. Вы применяете ZqType к Zq q Int, поэтому тип ZqType равен * -> * (несмотря на PolyKinds). Итак, у нас есть

data ZqType :: * -> * where
  ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

Теперь давайте посмотрим, какой тип у конструктора ZqType? Без полигональных видов это то, что вы записали:

ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

Но с PolyKinds q появляется только в видо-полиморфных позициях, так что это становится:

ZqType :: forall (q :: k). (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

Теперь давайте посмотрим, как вы используете это в sameModType:

typeEqSym :: ZqType a -> ZqType b -> Maybe (Dict (a ~ b))
typeEqSym (ZqType p) (ZqType q) = do
  ...

Я переименовал переменные типа, чтобы избежать путаницы. Итак, a — это неизвестный тип вида *, а b — другой неизвестный тип вида *. Вы выполняете сопоставление с образцом в GADT. В это время GHC узнает, что a на самом деле Zq q1 Int для какого-то неизвестного q1 неизвестного вида k1. Кроме того, GHC узнает, что b на самом деле Zq q2 Int для какого-то неизвестного q2 неизвестного вида k2. В частности, мы понятия не имеем, что k1 и k2 — это одно и то же, потому что это нигде не соблюдается.

Затем вы продолжаете вызывать sameModType, который ожидает, что оба прокси будут одного типа, что приводит к первой из ваших ошибок. Все остальные ошибки являются следствием одной и той же проблемы.

person kosmikus    schedule 20.05.2014
comment
Отличное объяснение, спасибо! Возможно, кто-то еще знает, что делать. - person crockeea; 20.05.2014
comment
Причина, по которой я не знаю, что делать, заключается в том, что это небольшой пример, которому не хватает мотивации (аналогично другому примеру, на который вы ссылались). Мне нужно знать, почему вы определяете ZqType именно так, как вы его определяете, а также почему вы считаете, что здесь нужен типичный полиморфизм, прежде чем я смогу дать совет, как заставить его работать. - person kosmikus; 21.05.2014
comment
Разработчик библиотеки предложил это определение для ZqType как решение для использования моего типа Zq с библиотекой (т.е. типа с бесконечными возможностями для фантомного параметра). Я думаю, что ZqType может измениться, насколько я понимаю, он должен иметь вид *->*. Функция typeEqSym принадлежит классу самой библиотеки, поэтому ее тип фиксирован (но определение может измениться). - person crockeea; 21.05.2014
comment
Я хотел бы полиморфизм вида, чтобы вид модуля не ограничивался одним типом/видом. Конечный пользователь должен выбрать реализацию Modulus. Раньше я тестировал реализацию с типом *, теперь меня интересует использование TypeLits с типом Nat, и мне кажется безумным обертывать его в Proxy. - person crockeea; 21.05.2014