Создайте GADT при разборе json

У меня есть структура данных, которую я создал с помощью GADT, и я хочу проанализировать некоторый json для этого GADT, используя aeson. Но средство проверки типов жалуется, что во всех случаях возможно создать только один из конструкторов GADT. См. Этот пример:

data Foo = Hello | World

data SFoo :: Foo -> Type where
  SHello :: SFoo 'Hello 
  SWorld :: SFoo 'World

instance FromJSON (SFoo a) where
  parseJSON = withText "Foo" \case
    "hello" -> pure SHello
    "world" -> pure SWorld

Итак, я хочу иметь возможность разобрать строку приветствия на SHello и строку мира на SWorld. Средство проверки типов выдает следующую ошибку:

• Couldn't match type ‘'World’ with ‘'Hello’
  Expected type: Parser (SFoo 'Hello)
    Actual type: Parser (SFoo 'World)
• In the expression: pure SWorld
  In a case alternative: "world" -> pure SWorld
  In the second argument of ‘withText’, namely
    ‘\case
       "hello" -> pure SHello
       "world" -> pure SWorld’

Как я могу разобрать некоторый json на такую ​​структуру GADT?


haskell text-parsing aeson gadt
person CryptoNoob    schedule 15.07.2020    source источник
comment
Вы пытаетесь заставить функцию синтаксического анализа возвращать разные типы в зависимости от ввода. Этого не может быть, функция должна иметь единственный возвращаемый тип. Вы должны упаковать оба варианта в один и тот же тип и вернуть его.   -  person Fyodor Soikin    schedule 15.07.2020

Ответы (1)


arrow_upward
5
arrow_downward

Этот

instance FromJSON (SFoo a) where

не летает. Ты получишь

parseJSON :: forall a. Value -> Parser (SFoo a)

это означает, что вызывающий может выбирать, какие a они хотят, а parseJSON не контролирует синтаксический анализ a из JSON. Вместо этого вы хотите

data SomeFoo = forall a. SomeFoo (SFoo a)
instance FromJSON SomeFoo where
    parseJSON = withText "Foo" \case
        "hello" -> pure $ SomeFoo SHello
        "world" -> pure $ SomeFoo SWorld
        _ -> fail "not a Foo" -- aeson note: without this you get crashes!

где сейчас

fromJSON :: Value -> Result SomeFoo

не сообщает вам, какую ветвь SFoo он будет возвращать в своем типе. SomeFoo теперь является парой типа a :: Foo и значения SFoo a. fromJSON теперь отвечает за синтаксический анализ всей пары, поэтому он контролирует как возвращаемый тип, так и значение. Когда вы используете его и сопоставляете SomeFoo, that сообщит вам, с каким типом вам придется иметь дело:

example :: Value -> IO ()
example x = case fromJSON x of
    Error _ -> return ()
    Success (SomeFoo x) -> -- know x :: SFoo a where a is a type extracted from the match; don't know anything about a yet
        case x of
            SHello -> {- now know a ~ Hello -} return ()
            SWorld -> {- now know a ~ World -} return ()

Обратите внимание, что SomeFoo в основном изоморфен Foo. Вы также можете написать

instance FromJSON Foo where ..

а потом

someFoo :: Foo -> SomeFoo
someFoo Hello = SomeFoo SHello
someFoo World = SomeFoo SWorld
instance FromJSON SomeFoo where parseJSON = fmap someFoo . parseJSON

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

instance FromJSON (SFoo Hello) where
    parseJSON = withText "SFoo Hello" \case
        "hello" -> pure SHello
        _ -> fail "not an SFoo Hello"
instance FromJSON (SFoo World) where
    parseJSON = withText "SFoo World" \case
        "world" -> pure SWorld
        _ -> fail "not an SFoo World"

... но они не особо полезны, за исключением другого способа написать FromJSON SomeFoo:

instance FromJSON SomeFoo where
    parseJSON x = prependFailure "SomeFoo: " $
        SomeFoo @Hello <$> parseJSON x <|> SomeFoo @World <$> parseJSON x
person HTNW    schedule 15.07.2020
comment
Последний шаблон очень распространен при использовании GADT с вводом времени выполнения: сначала выполните синтаксический анализ нетипизированного представления ADT, затем «проверьте его тип», чтобы получить типизированный GADT, упакованный как экзистенциальный или sigma. - person Jon Purdy; 15.07.2020