[Haskell-cafe] Free lunch with GADTs

[Tristan Ravitch]

Hi cafe,

I'm playing around with GADTs and was hoping they would let me have my
cake and eat it too.  I am trying to use GADTs to tag a type with some
extra information.  This information is very useful in a few cases,
but the more common case is that I just have a list of items without
the tags.  Ideally I'll be able to recover the tags from the common
case via pattern matching.  What I have right now is:



{-# LANGUAGE GADTs, ExistentialQuantification, EmptyDataDecls, RankNTypes, LiberalTypeSynonyms #-}
data Tag1
data Tag2

data T tag where
  T1 :: Int -> T Tag1
  T2 :: Double -> T Tag2

f1 :: [T t] -> Int
f1 = foldr worker 0
  where
    worker (T1 i) a = i+a
    worker _ a = a

f2 :: [T Tag1] -> Int
f2 = foldr worker 0
  where
    worker :: T Tag1 -> Int -> Int
    worker (T1 i) a = a + i



In f2 I can work with just values with one tag, but f1 is also
important to me (working with the untagged values).  f1 type checks
but I do not know how to make a list [T t].  If I try the naive thing
in ghci, it understandably tells me:

> let l = [T1 5, T2 6.0]

<interactive>:6:16:
    Couldn't match type `Tag2' with `Tag1'
    Expected type: T Tag1
      Actual type: T Tag2
    In the return type of a call of `T2'
    In the expression: T2 6.0
    In the expression: [T1 5, T2 6.0]


Fair enough.  Is there any magical way to make this possible?  I am
hoping to avoid making a separate existential wrapper around my type.
I know that approach works, but that would make the more common case
much less convenient.  I also remember trying to use a type synonym
with -XLiberalTypeSynonyms:

type SimpleT = forall tag . T tag

I managed to basically get that working with another variant of my
list processing function, but it required -XImpredicativeTypes, which
apparently did very unfortunate things to type inference.


Thanks
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130213/613ab114/attachment.pgp>