(Как) возможно ли иметь полиморфные значения в GADT `зависимой карты`? - PullRequest
Новая
       24

(Как) возможно ли иметь полиморфные значения в GADT `зависимой карты`?

0 голосов
/ 26 апреля 2018

Кто-нибудь знает, как / если возможно расширить Foo GADT в этот код : 

{-# language GADTs #-}
{-# language DeriveGeneric #-}
{-# language DeriveAnyClass #-}
{-# language TemplateHaskell #-}
{-# language StandaloneDeriving #-}

import Prelude                  (Int, String, print, ($))
import Data.GADT.Show           ()
import Data.GADT.Compare        ()
import Data.Dependent.Map       (DMap, fromList, (!))
import Data.Dependent.Sum       ((==>))
import Data.GADT.Compare.TH     (deriveGEq, deriveGCompare)
import Data.Functor.Identity    (Identity)

data Foo a where
  AnInt   :: Foo Int
  AString :: Foo String

deriveGEq      ''Foo
deriveGCompare ''Foo

dmap1 :: DMap Foo Identity
dmap1 = fromList [AnInt ==> 1, AString ==> "bar"]

main = do
  print $ dmap1 ! AnInt
  print $ dmap1 ! AString

  -- Prints:
  -- Identity 1
  -- Identity "bar"

с 

  ANum :: Num n => Foo n

(или что-то подобное), чтобы учесть полиморфные значения в dependent-map?

При попытке получить сообщение об ошибке типа: 

exp-dep-map.hs:20:1: error:
    • Couldn't match type ‘a’ with ‘b’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          geq :: forall a b. Foo a -> Foo b -> Maybe (a := b)
        at exp-dep-map.hs:20:1-20
      ‘b’ is a rigid type variable bound by
        the type signature for:
          geq :: forall a b. Foo a -> Foo b -> Maybe (a := b)
        at exp-dep-map.hs:20:1-20
      Expected type: Maybe (a := b)
        Actual type: Maybe (a :~: a)
    • In a stmt of a 'do' block: return Refl
      In the expression: do return Refl
      In an equation for ‘geq’: geq ANum ANum = do return Refl
    • Relevant bindings include
        geq :: Foo a -> Foo b -> Maybe (a := b)
          (bound at exp-dep-map.hs:20:1)
   |
20 | deriveGEq      ''Foo
   | ^^^^^^^^^^^^^^^^^^^^

Редактировать: Я продолжал работать над этим вместе с echatav и isovector (имена пользователей GitHub), и мы смогли разобраться в этом вопросе дальше, и мы также обнаружили, что определение экземпляров GEq и GCompare вручную помогает. Спасибо, @rampion, ваш ответ также подтверждает то, что мы нашли.

Хотя гораздо меньше, чем идеально, определять их вручную для больших типов записей. Интересно, можно ли было бы обновить генераторы TemplateHaskell (deriveGCompare, deriveGEq) {для поддержки полиморфизма?

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

data Foo n a where
  AnInt :: Foo n Int
  AString :: Foo n String
  ANum :: (Num n, Typeable n, Show n) => Foo n n

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

instance GEq (Foo n) where
  geq AnInt AnInt = return Refl
  geq AString AString = return Refl
  geq ANum ANum = return Refl
  geq _ _ = Nothing

instance GCompare (Foo n) where
  gcompare AnInt AnInt = GEQ
  gcompare AnInt _ = GLT
  gcompare _ AnInt = GGT
  gcompare AString AString = GEQ
  gcompare AString _ = GLT
  gcompare _ AString = GGT
  gcompare (ANum :: Foo n a) (ANum :: Foo n b) = (eqT @a @b) & \case
    Just (Refl :: a :~: b) -> GEQ
    Nothing   -> error "This shouldn't happen"
  gcompare ANum _ = GLT
  gcompare _ ANum = GGT

Пытаясь использовать TH, (например, deriveGEq ''Foo или deriveGEq ''(Foo n)) я сталкиваюсь с любезными вопросами. 

exp-dep-map.hs:39:1: error:
    • Expecting one more argument to ‘Foo’
      Expected kind ‘* -> *’, but ‘Foo’ has kind ‘* -> * -> *’
    • In the first argument of ‘GEq’, namely ‘Foo’
      In the instance declaration for ‘GEq Foo’
   |
39 | deriveGEq      ''Foo
   | ^^^^^^^^^^^^^^^^^^^^


exp-dep-map.hs:40:19: error: parse error on input ‘Foo’
   |
40 | deriveGEq      ''(Foo n)
   |                   ^^^

Может быть актуально: https://github.com/mokus0/dependent-sum-template/pull/6

1 Ответ

0 голосов
/ 26 апреля 2018

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

Посмотрите на определение GEq: 

class GEq f where
  geq :: f a -> f b -> Maybe (a := b)

Мы не получаем никаких дальнейших ограничений на a или b, поэтому нам нужно доказать (или опровергнуть) равенство типов только для конструкторов GADT.

Что вышеописанное ANum не дает нам.

Это исправимо, если мы добавим еще одно ограничение к ANum - Typeable

ANum :: (Num n, Typeable n) => n -> Foo n

Теперь мы можем использовать eqT, чтобы засвидетельствовать равенство типов 

geq (ANum _) (ANum _) = eqT
...