Объяснение несоответствия общего типа

#haskell #generics #ghc

#haskell #общие #ghc

Вопрос:

Я пытался получить имя конструктора данных по значению. Я нашел решение здесь.

 {-# LANGUAGE DeriveGeneric, TypeFamilies, TypeOperators,
    FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
import GHC.Generics
undef2 :: mi f p -> f p
undef2 _ = undefined
data Tt = Cc deriving (Show, Generic)
> conName $ undef2 (from Cc)
"Cc"
  

Я подумал, что это все, что мне нужно, и попытался поместить приведенный выше код в экземпляр класса для D1.

 >:t (from Cc)
from Cc
  :: D1
       ('MetaData "Tt" "Main" "main" 'False)
       (C1 ('MetaCons "Cc" 'PrefixI 'False) U1)
       x
  

Я предположил, что если «from Cc» — это D1, то реализация для D1 должна работать.

 class GDConstrName a where
  gname :: a x -> String

instance GDConstrName (D1 m x) where
  gname x = conName $ undef2 x

  

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

 Main.hs:37:23: error:
    • Couldn't match type ‘x’ with ‘t0 c0 f0’
      ‘x’ is a rigid type variable bound by
        the instance declaration
        at Main.hs:36:10-30
      Expected type: t0 c0 f0 x1
        Actual type: x x1In the second argument of ‘($)’, namely ‘undef2 x’
      In the expression: conName $ undef2 x
      In an equation for ‘gname’: gname x = conName $ undef2 x
    • Relevant bindings include
        x :: D1 m x x1 (bound at Main.hs:37:9)
        gname :: D1 m x x1 -> String (bound at Main.hs:37:3)
   |
37 |   gname x = conName $ undef2 x
  

Поэтому для меня загадка, почему один и тот же код работает (x = (из Cc)) в одном случае, но терпит неудачу в другом.

Я нашел решение вообще без conName, но оно выглядит странно и на гораздо более низком уровне.

 instance (KnownSymbol dcn) => GDConstrName (D1 m (C1 ('MetaCons dcn p f) gg)) where
  gname x = symbolVal (undefined :: Proxy dcn)

  

Я запускаю Ghc 8.4.4

Ответ №1:

Написав немного больше типов и разновидностей, мы имеем

 undef2 :: forall {k} {mi :: (k -> Type) -> k -> Type} {f :: k -> Type} {p :: k}.  mi f p -> f p
  

и для D1 конструктора типа

 D1 :: forall {k}. Meta -> (k -> Type) -> k -> Type
  

В вашем экземпляре

 instance GDConstrName (D1 m x) where
  gname z = conName $ undef2 z
  

x Тип имеет вид k -> Type , потому что он вписывается во 2-й параметр D1 конструктора типа.

Итак, экземпляр говорит, что «для каждого типа вида Meta и для каждого конструктора типа вида k -> Type вот реализация gname «.

Однако undef2 требуется больше «структуры» для его типа ввода. mi имеет вид (k -> Type) -> k -> Type : он принимает два параметра типа, один из которых является конструктором типа.

Следующий (бесполезный) тип подходит для вашего экземпляра: D1 (MetaData "" "" "" True) Proxy , потому что Proxy имеет вид k -> Type . Но вы не можете использовать undef2 с чем-то типа Proxy z , независимо от z :

 ghci> :t undef2 (undefined :: Proxy Int)

<interactive>:1:9: error:
* Couldn't match kind `forall {k}. k -> Type'
                 with `(Type -> Type) -> Type -> Type'