Развертывание экзистенциально квантифицированного GADT

У меня есть пользовательский тип значения Value, помеченный своим типом ValType:

data ValType
  = Text
  | Bool

data Value (tag :: ValType) where
  T :: Text -> Value 'Text
  B :: Bool -> Value 'Bool

и я хотел бы определить функцию, которая разворачивает экзистенциально квантифицированный Value, то есть она должна иметь следующую сигнатуру типа:

data SomeValue = forall tag. SomeValue (Value tag)

unwrap :: SomeValue -> Maybe (Value tag)

Я могу определить развертку для 'Bool и 'Text отдельно, но как определить полиморфный unwrap?


haskell existential-type dependent-type gadt
person Poscat    schedule 20.06.2020    source источник
comment
Одним из возможных обходных путей является использование открытого союза, но мне все еще любопытно, можно ли это сделать для GADT.   -  person Poscat    schedule 20.06.2020
comment
в основном, как мне сопоставить шаблон для продвигаемых типов? Я думаю, вы можете сделать это на уровне типов с семействами типов, но как вы делаете это на уровне терминов?   -  person Poscat    schedule 20.06.2020

Ответы (4)


arrow_upward
7
arrow_downward

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

data SValType v where
  SText :: SValType 'Text
  SBool :: SValType 'Bool

class KnownValType (v :: ValType) where
  knownValType :: SValType v
instance KnownValType 'Text where
  knownValType = SText
instance KnownValType 'Bool where
  knownValType = SBool

unwrap :: forall tag. KnownValType tag => SomeValue -> Maybe (Value tag)
unwrap (SomeValue v) = case knownValType @tag of
  SText
    | T _ <- v -> Just v
    | otherwise -> Nothing
  SBool
    | B _ <- v -> Just v
    | otherwise -> Nothing

В отличие от класса IsType вашего собственного ответа, KnownValType позволяет получить информацию о типе, а также тег значения из совпадения с образцом. Таким образом, вы можете использовать его гораздо более широко для обработки этих типов.

Для случаев, когда вашего typeOf достаточно, мы можем написать его без проблем:

 typeOf :: KnownValType a => Proxy a -> ValType
 typeOf (_ :: Proxy a) = case knownValType @a of
   SBool -> Bool
   SText -> Text
person dfeuer    schedule 20.06.2020
comment
Для этого конкретного примера также подходит unwrap :: SomeValue -> Either (Value 'Text) (Value 'Bool). - person chi; 20.06.2020

arrow_upward
3
arrow_downward

В качестве еще одной альтернативы использование Typeable и cast дает довольно лаконичное решение. Вам все еще нужно носить с собой словарь, но вам не нужно создавать его самостоятельно:

{-# LANGUAGE DataKinds, FlexibleInstances, GADTs,
    KindSignatures, StandaloneDeriving, OverloadedStrings #-}

import Data.Text (Text)
import Data.Typeable

data ValType
  = Text
  | Bool

data Value (tag :: ValType) where
  T :: Text -> Value 'Text
  B :: Bool -> Value 'Bool
deriving instance Show (Value 'Text)
deriving instance Show (Value 'Bool)

data SomeValue = forall tag. SomeValue (Value tag)

unwrap :: (Typeable tag) => SomeValue -> Maybe (Value tag)
unwrap (SomeValue (T t)) = cast (T t)
unwrap (SomeValue (B b)) = cast (B b)

main = do
  print (unwrap (SomeValue (T "foo")) :: Maybe (Value 'Text))
  print (unwrap (SomeValue (T "foo")) :: Maybe (Value 'Bool))
person K. A. Buhr    schedule 20.06.2020
comment
Typeable кажется излишним для закрытой вселенной. - person dfeuer; 20.06.2020
comment
Наверное, но то же самое можно сказать и о написании полиморфного unwrap. - person K. A. Buhr; 20.06.2020

arrow_upward
1
arrow_downward

возможное решение, определил класс типов для повторения типов типа ValType обратно в термины:

class IsType a where
  typeOf :: Proxy a -> ValType

instance IsType 'Text where
  typeOf _ = Text

instance IsType 'Bool where
  typeOf _ = Bool

unwarp :: IsType tag => SomeValue -> Maybe (Value tag)
unwarp (SomeValue v) =
  case typeOf (Proxy @tag) of
    Bool ->
      case v of
        B _ -> Just v
        _ -> Nothing
    Text ->
      case v of
        T _ -> Just v
        _ -> Nothing

Но мне придется носить с собой этот словарь классов типов, который не очень элегантен.

person Poscat    schedule 20.06.2020

arrow_upward
1
arrow_downward

Будет ли это приемлемо?

data SomeValue = forall tag. (Typeable tag) => SomeValue (Value tag)

unwrap :: (Typeable tag) => SomeValue -> Maybe (Value tag)
unwrap (SomeValue t) = cast t

Приведение общего типа к шаблону конкретного типа Maybe в значительной степени является тем, для чего предназначен Typeable.

person luqui    schedule 21.06.2020