Construct GADT while parsing json

Question

I have a data structure that I have created with GADT and I want to parse some json to this GADT using aeson. But the type checker complains that It's only possible to create one of the constructors of the GADT in all the cases. See this example:

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

So I want to be able to parse the "hello" string to SHello and the "world" string to SWorld. The type checker complains with the following error:

• 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’

How can I parse some json to a GADT structure like this?

You're trying to have the parsing function return different types depending on the input. This cannot happen, a function must have a single return type. You have to pack both variants into the same type and return that. — Fyodor Soikin

HTNW HTNW · Accepted Answer · 2020-07-15T13:46:36

This

instance FromJSON (SFoo a) where

doesn't fly. You'd get

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

which means that the caller gets to choose which a they want, and parseJSON is not in control of parsing the a from the JSON. Instead, you want

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!

where now

fromJSON :: Value -> Result SomeFoo

does not tell you which branch of SFoo it will be returning in its type. SomeFoo is now a pair of a a :: Foo type and a SFoo a value. fromJSON is now in charge of parsing the entire pair, so it controls both the returned type and the value. When you use it and match on the SomeFoo, that will tell you which type you have to deal with:

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 ()

Note that SomeFoo is basically isomorphic to Foo. You may as well write

instance FromJSON Foo where ..

and then

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

Note that you can write the following two instances:

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"

...but they're not particularly useful, except as another way to write FromJSON SomeFoo:

instance FromJSON SomeFoo where
    parseJSON x = prependFailure "SomeFoo: " $
        SomeFoo @Hello <$> parseJSON x <|> SomeFoo @World <$> parseJSON x

Construct GADT while parsing json

1 Answers