4

I'm currently having a fight with the typechecker when I try to create a function returning Thing a (where Thing is a GADT). A minimal contrived example:

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data TFoo
data TBar
data Thing a where
  Foo :: Int -> Thing TFoo
  Bar :: String -> Thing TBar

combine :: [Thing a]
combine = [Foo 1, Bar "abc"]

main :: IO ()
main = undefined

The typechecker gets unhappy that a doesn't match TBar. Presumably this is because it has already inferred that a is TFoo. But, this is surprising, because with regular sum types you can do:

data Thing = Foo Int | Bar String

combine :: [Thing]
combine = [Foo 1, Bar "abc"]

Is there anyway to return a type parametric over the GADT parameter?

Outside of the context of the contrived examples, I need GADTs so I can type certain functions to only take a Foo, but before that I need to also be able to just return a list of Things.

Bailey Parker
  • 15,599
  • 5
  • 53
  • 91
  • I think your problem is that lists must be homogeneous. Like you noted, you can have `[Thing]`, but you can't but two different `Thing a`'s in the same list. – jkeuhlen Mar 02 '18 at 22:04
  • @jkeuhlen Right. That makes sense for clearly disparate types like `[1, "a"]`, but I'm a little confused with the parity between GADTs and sum types. Is `Thing a` not the "final return type" of `Foo` and `Bar`. Is there any type that encompass the result of both `Foo 1` and `Bar "abc"`? – Bailey Parker Mar 02 '18 at 22:06
  • 1
    No, `Thing a` is *not* the final return type of your constructors. They explicitly create a `Thing TFOO` and a `Thing TBar`. – jkeuhlen Mar 02 '18 at 22:11

1 Answers1

5

You've got your quantifiers mixed up.

combine :: [Thing a]

means (the forall is implicit in the syntax)

combine :: forall a. [Thing a]

Essentially, combine needs to be a [Thing a] no matter what a is, because a is chosen by the code that calls combine. Or, in another sense,

-- psuedo-Haskell
combine :: (a :: *) -> [Thing a]

combine is a function that takes a type as argument and promises to construct a list of Things of that type. The only possible definition of combine with this type signature is combine = [], plus a bunch of dumb ones like [undefined], etc. E.g. combine = [Foo 1] would not work either, because a is not being inferred, because it's not combine that sets a; it's the user.

You want

-- psuedo-Haskell
combine :: [exists a. Thing a]

which means "combine is a list of things, and each thing is a Thing of some unknown type" (and every Thing can be of a different type). The exists quantifier is the flipside of forall. It means the definition of combine can set whatever type it wants and the user will have to deal with it. Haskell doesn't support exists out-of-the-box, so you need to define an intermediate data type:

data SomeThing = forall a. SomeThing (Thing a)

The syntax is a bit backwards for using the universal quantifier to create existential quantification, but the idea is that you get

SomeThing :: forall a. Thing a -> SomeThing

which essentially erases the knowledge of what a is.

You can then have

combine :: [SomeThing]
combine = [SomeThing $ Foo 1, SomeThing $ Bar "abc"]
HTNW
  • 27,182
  • 1
  • 32
  • 60
  • Wow! Fantastic answer. Thank you so much. That works perfectly. It's a bit unfortunate that to get the benefit of GADTs (insofar as you can limit which "children?" are passed into other functions) you now can't use them homogeneously without wrapping. Do you know if `exists` is something that could exist in Haskell in the future or is wrapping just the accepted approach the everyone uses? – Bailey Parker Mar 02 '18 at 22:19
  • @BaileyParker The accepted approach is just wrapping. Another approach is higher-rankedly-typed continuations (`forall ret. (forall a. Thing a -> ret) -> ret`) ([e.g. this is how you must do it in Typescript](https://stackoverflow.com/a/46186356/5684257)), but it's a lot more painful than this wrapping (and you still need wrapping because of impredicativity). I don't think there are plans to add `exists` to Haskell because having both `exists` and `forall` would probably make the typechecker too complicated. – HTNW Mar 02 '18 at 22:27
  • What you call `exist` is called `forall` in a number of attempts to add impredicative polymorphism. All is not lost with the latest proposal on *guarded instantiation*, but implementation is still far from finish, more on this here: https://mail.haskell.org/pipermail/ghc-devs/2018-February/015407.html – Artem Pelenitsyn Mar 03 '18 at 17:07
  • @ArtemPelenitsyn Sorry, what? `exists` and `forall` are literally opposites. `[forall a. Show a => a]` means a list of things where each thing can be of any type that satisfies `Show`. The only values of that type are `[]`, `[undefined]`, etc. `[exists a. Show a => a]` means a list of things where each thing has some `Show`able type. This has many values, e.g. `[5, "abc", 'a', [10]]`. For some arbitrary type `A` with `Show A`, `[forall a. Show a => a]` is a subtype of `[A]` is a subtype of `[exists a. Show a => a]`. – HTNW Mar 03 '18 at 17:33
  • @HTNW don't you know that even ExistentialTypes extensions in GHC use `forall` keyword? – Artem Pelenitsyn Mar 03 '18 at 17:55
  • @ArtemPelenitsyn Yes, I mention that in my answer. But having impredicative polymorphism with `forall` will still not solve the problem. You'd be allowed a `[forall ret. (forall a. Thing a -> ret) -> ret]`, which is isomorphic to `[exists. a Thing a]` and removes the need for a wrapper `data` type, but it is *still* not as simple as just having `exists` as a primitive. – HTNW Mar 03 '18 at 18:01
  • @ArtemPelenitsyn Or, in other words: `ExistentialTypes` allows for *non-primitive* existential quantification by using *universal* quantification (thus `forall`) plus some identities between the two. `forall` does not directly cause existential quantification. `forall` always causes universal quantification. It's just that `ExistentialTypes` allows you to use universal quantification in a place where it can be turned inside out to cause existential quantification. But it's not primitive. `forall a. Thing a` is a subtype of `Thing TFoo`, but `Thing TFoo` is not a subtype of `SomeThing`. – HTNW Mar 03 '18 at 18:09