Типовое приведение GADT

Допустим, я пишу DSL и хочу иметь поддержку как поддержки фантомных типов, так и плохо типизированных выражений. Мои типы значений могут быть

{-# LANGUAGE GADTs, DataKinds #-}

data Ty = Num | Bool deriving (Typeable)

data Val a where
  VNum  :: Int  -> Val Num
  VBool :: Bool -> Val Bool

и я могу работать с фантомной стертой версией

{-# LANGUAGE ExistentialQuantification #-}

data Valunk = forall a . Valunk (V' a)

Теперь я могу работать со значениями Valunk, caseвыделяя как VNum, так и VBool, и даже таким образом восстанавливать свои фантомные типы.

getNum :: Valunk -> Maybe (Val Num)
getNum (Valunk n@(VNum _)) = Just n
getNum _                   = Nothing

Но это просто похоже на то, что я заново реализую механизм Typeable. К сожалению, GHC не позволяет мне получить Typeable для Val.

src/Types/Core.hs:97:13:
    Can't make a derived instance of `Typeable (Val a)':
      Val must only have arguments of kind `*'
    In the data declaration for Val

Есть ли способ обойти это ограничение? я бы хотел написать

getIt :: Typeable a => Valunk -> Maybe (Val a)
getIt (Valunk v) = cast v

но сейчас я должен прибегнуть к такой технике

class Typeably b x where kast :: x a -> Maybe (x b)
instance Typeably Num Val where 
  kast n@(VNum _) = Just n
  kast _          = Nothing

для всех моих видов.


haskell existential-type gadt
person J. Abrahamson    schedule 07.08.2013    source источник
comment
Похоже, механизм deriving (Typeable) еще не приспособлен для работы с DataKinds. DataKinds не дает вам ничего удивительного, просто дополнительная проверка. Вы можете использовать data Num и data Bool вместо своего вида Ty.   -  person luqui    schedule 08.08.2013

Ответы (2)


arrow_upward
1
arrow_downward

Прежде всего, вам нужно сохранить свидетельство того, что квантифицированный тип в Valunk находится в Typeable:

data Valunk = forall a . Typeable a => Valunk (Val a)

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

getIt :: Typeable a => Valunk -> Maybe (Val a)
getIt (Valunk v) = gcast v

Это было протестировано с:

data Val a where
  VNum  :: Int  -> Val Int
  VBool :: Bool -> Val Bool
person emilaxelsson    schedule 15.08.2013

arrow_upward
1
arrow_downward

Вы можете получить Data.Typeable самостоятельно:

{-# LANGUAGE GADTs, DataKinds, DeriveDataTypeable, ExistentialQuantification #-}

import Data.Typeable

data Ty = TNum | TBool deriving Typeable 

data Valunk = forall a. Typeable a => Valunk a 

data Val a where 
    VInt :: Int -> Val TNum
    VBool :: Bool -> Val TBool 

instance Show (Val a) where 
    show (VInt a) = show a
    show (VBool a) = show a 

valtypenam = mkTyCon3 "package" "module" "Val"

instance Typeable (Val a) where 
    typeOf _ = mkTyConApp valtypenam []

getIt :: Valunk -> Maybe (Val a)
getIt (Valunk p) = cast p

Это обеспечит функцию получения. Просто убедитесь, что вы правильно назвали свой тип (таким образом, правильно укажите пакет, модуль и тип), иначе другие пакеты могут столкнуться с проблемами.

Дополнительные примеры написания этих экземпляров см. в: Data.Derive.Typeable source.

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

person Edgar Klerks    schedule 11.08.2013