GADTs in the wild

[Felipe Almeida Lessa]

On Tue, Aug 14, 2012 at 8:44 AM, Michael Snoyman <michael at snoyman.com> wrote:
> An example that came up at work (with Yitzchak Gale, he probably has more
> details) was essentially two different types of documents that shared a lot
> of the same kinds of elements (tables, lists, paragraphs, etc) but some
> elements only appeared in one of the document types. We needed to render to
> (for sake of argument) two different XML formats, and wanted to be certain
> we didn't put in elements from type 1 in type 2. The solution looked
> something like this (using data kinds and GADTs):

This is the same thing that I did on the fb library.  There are two
kinds of Facebook access tokens: an app access token and an user
access token.  Some methods require either one or the other (e.g.
[5]), but there are also some methods that may use whatever kind of
access token you have (e.g. [3,4]).  So AccessToken [1,2] is defined
as the following GADT:

  data AccessToken kind where
      UserAccessToken :: UserId -> AccessTokenData -> UTCTime ->
AccessToken UserKind
      AppAccessToken  :: AccessTokenData -> AccessToken AppKind

  data UserKind
  data AppKind

(Yes, that could be a data kind!)  And for convenience we also export
some type synonyms:

  type UserAccessToken = AccessToken UserKind
  type AppAccessToken = AccessToken AppKind

So we get the convenience of one data type and the type safety of two,
which is especially nice considering that there are functions
returning access tokens as well [6,7].

Cheers, =)

[1] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#t:AccessToken
[2] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/src/Facebook-Types.html#AccessToken
[3] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:isValid
[4] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:fqlQuery
[5] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:createCheckin
[6] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:getAppAccessToken
[7] http://hackage.haskell.org/packages/archive/fb/0.9.7/doc/html/Facebook.html#v:getUserAccessTokenStep2

-- 
Felipe.