UnionType and UnionInputType, analogues of RecordType and RecordInputType

[mstksg]

Allows us to generate an Input for a union:

data Status = Queued Natural
            | Result Text
            | Errored Text

status :: Type Status
status =
  union
    ( (Queued  <$> constructor "Queued"  natural)    -- or `constructor "Queued" (Queued <$> natural)`
   <> (Result  <$> constructor "Result"  string )
   <> (Errored <$> constructor "Errored" string )
    )

And (potentially partially) create an InputType:

injectStatus :: InputType Status
injectStatus =
  inputUnion
    (  inputConstructor "Queued"  (\case Queued n  -> Just n; _ -> Nothing)
    <> inputConstructor "Result"  (\case Result t  -> Just t; _ -> Nothing)
    <> inputConstructor "Errored" (\case Errored e -> Just e; _ -> Nothing)
    )
-- (could potentially be simplified with a prism-based interface, but this would incur a profunctors dep)

I couldn't really think of a way to write inputUnion in a way that would make sure it was total without a "two-pass" solution, where the user provides the "injecting" logic and the "specify type" logic in two different places; one alternative was a quasi-one-pass system where the user specifies the total logic up-front, but the result can be optionally "validated" by providing a proof of totality before being used. However, that requires encoding the number of branches in the type level, so I'm not sure if the benefit pays for the cost in complexity.

Let me know if this isn't something that fits in the vision of the library, or if there's anything I could fix :)

[Gabriella439]

The CI build is failing on GHC 7.10.3 mainly due to needing to import the Semigroup class

[Gabriella439]

Would it be possible to avoid the partial implementation by changing UnionInputType to:

data UnionInputType a = UnionInputType (Map Text (Expr Src X)) (a -> Maybe (Map Expr Src X))

[mstksg]

This representation makes more sense, since we only consume injector in the asum'd form. However, I don't quite see how this can directly help us fix the partiality.

However, this representation gives a hint about how we could make it non-partial; we might be able to write a variant of inputUnion that gives a fallback option that would be used if anything was Maybe.

[mstksg]

17fd6c3 now incorporates this new representation! It's actually nicer because we get a derivable Contravariant and almost a derivable Monoid instance (waiting for base-4.12, which has Monoid for :*:).

Still curious about what you had in mind for resolving the partiality issue, though! :)

[ocharles]

At work, we are using what I suppose is a simpler variation of this:

makeUnion :: Map.InsOrdHashMap LazyText.Text ( Dhall.Type a ) -> Dhall.Type a
makeUnion alts =
  let
    extract expr = do
      Expr.UnionLit ctor v _ <-
        return expr

      t <-
        Map.lookup ctor alts

      Dhall.extract t v

    expected =
      Expr.Union ( Dhall.expected <$> alts )

  in Dhall.Type { .. }

It looks like yours is the same idea though, and I like not leaking Map 👍

[Gabriella439]

@mstksg: I believe you can fix the partiality using a trick similar to RecordInputType, except replacing Divisible with Decidable.

In other words, the user interface we supply looks like this:

-- I'm not sure if this is the right representation to use, so focus more
-- on the type signatures than the implementation
newtype UnionInputType a = UnionInputType (Map Text (InputType a))

inputConstructorWith :: Text -> InputType a -> UnionInputType a
inputConstructorWith k v = UnionInputType (Data.Map.singleton k v)

inputConstructor :: Inject a => Text -> UnionInputType a
inputConstructor k = inputConstructorWith k inject

instance Contravariant UnionInputType where …
instance Divisible     UnionInputType where …
instance Decidable     UnionInputType where …

(>|<) :: Decidable f => f a -> f b -> f (Either a b)
(>|<) = Data.Functor.Contravariant.chosen

-- I haven't thought through if this can be implemented.  Feel free to
-- change the implementation of `UnionInputType` if this function isn't
-- total
inputUnion :: UnionInputType a -> InputType a
inputUnion = …

... so that the user can write this:

injectStatus :: InputType Status
injectStatus =
          adapt
    >$< inputConstructor "Queued"
    >|< inputConstructor "Result"
    >|< inputConstructor "Errored"
  where
    adapt (Queued  n) = Left (Left n)
    adapt (Result  t) = Left (Right t)
    adapt (Errored e) = Right e

[mstksg]

A Decidable-inspired interface might work! Although I don't think we could actually use Decidable, because the Divisible instance might not necessarily make sense (this is the reason also why I use Monoid instead of Alternative for UnionType...because Applicative UnionType doesn't quite work). On that note, we could actually maybe be able to unify RecordType and UnionType, to some extent, by providing a type that is both Applicative and Alternative, and also unify RecordInputType and UnionInputType by providing a type that is both Divisible and Decidable. These would basically allow the user to construct/define records of unions of records of records of unions of (etc.), of arbitrary nesting. This isn't actually too bad, but it might be difficult to predict the resulting shape for non-complex usage.

I'll see if I can whip up a "Decidable-inspired" interface (using an analog of chosen), and also maybe play around with arbitrary nesting so we could unify RecordType and UnionType perhaps, if that might be cleaner.

[mstksg]

The Decidable-inspired method (implemented in cc140c3) works and ensures totality! :D

However, as feared, it is impossible to actually use Decidable, because Decidable requires Divisible. The issue is conquer; there isn't any way to implement:

conquer :: forall a. UnionInputType a

because this would allow the user to construct something silly like a conquer :: UserInputType Natural, but without specifying any constructor names. inputUnion (conquer @Natural) is unimplementable in a total way, other than always serializing it to something constant like {}.

However, dropping in a custom >|< detached from chosen works, and we can re-use >$< for Contravariant.

One small note: it's possible to implement lose :: forall a. (a -> Void) -> UnionType a; however, I'm not sure if there is any benefit to doing so, so it might not be worth writing out and providing.

I'll still continue to play around with a combined RecordUnionType and RecordUnionInputType where <*>/>*< correspond to combining records, and <|>/>|< correspond to combining unions in the meantime, but for now I think this version's API isn't too bad already, with the partiality handled :)

[Gabriella439]

@mstksg: Yeah, a monomorphic (>|<) is fine

Also, this branch still needs to import Semigroup for older versions of GHC before CI will pass

[mstksg]

New changes should appease GHC 8.0 and above! However, I couldn't get the dependencies to work with GHC 7.10, but I'm not sure if these versions were still officially supported.

[Gabriella439]

@mstksg: Are you sure your changes don't work with GHC 7.10? CI passed and that requires GHC 7.10 to work

The reason Dhall supports GHC 7.10 is for Eta since Dhall is a supported configuration format for Eta packages and Eta is built using GHC 7.10

[Gabriella439]

I will go ahead and merge this since CI thinks this is GHC 7.10-ready

[mstksg]

Ah, nice! I couldn't get to the build part, I got stuck in the dependency resolution part. But if it works, then I'll take your word for it :) Thanks!