Разворачивание экзистенциально количественно оцененного GADT - PullRequest
Новая
       67

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

6 голосов
/ 20 июня 2020

У меня есть настраиваемый тип значения 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 по отдельности, но как мне определить полиморф c unwrap?

Ответы [ 4 ]

7 голосов
/ 20 июня 2020

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

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
3 голосов
/ 20 июня 2020

В качестве еще одной альтернативы использование 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))
1 голос
/ 21 июня 2020

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

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

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

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

1 голос
/ 20 июня 2020

возможное решение, определенное классом типов для уточнения типов 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

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

...