I'm no expert, but it seems like those constructors should return
Foobar NoZoo, unless you're nesting so there could be a Zoo, in which
case the type variable a should transit, for example:
data Foobar a where
Foo :: X -> Y -> Foobar NoZoo
Bar :: X -> Y -> Foobar NoZoo
Baz :: Foobar a -> Foobar a
Zoo :: Foobar NoZoo -> Foobar Zoo
value = Zoo $ Foo (X 1) (Y 'a')
value2 = Zoo $ Baz $ Foo (X 1) (Y 'a')
-- value3 = Zoo $ Baz $ Zoo $ Foo (X 1) (Y 'a')
-- Couldn't match expected type `NoZoo' against inferred type `Zoo'
-- Expected type: Foobar NoZoo
-- Inferred type: Foobar Zoo
-- In the second argument of `($)', namely
-- `Baz $ Zoo $ Foo (X 1) (Y 'a')'
-- In the expression: Zoo $ Baz $ Zoo $ Foo (X 1) (Y 'a')
That is, if you construct a Baz with something else that doesn't have
a Zoo (e.g. NoZoo) then the resultant type is also NoZoo. The converse
is true.
Why would you want it to generate a polymorphic Foobar when it
definitely is NoZoo?
-Ross
(p.s. the example names in this thread are a bit ridiculous ;-) )
On Jun 23, 2009, at 4:01 PM, Andrew Coppin wrote:
Ross Mellgren wrote:
This works for me:
{-# LANGUAGE EmptyDataDecls, GADTs #-}
module Main where
data NoZoo
data Zoo
newtype X = X Int deriving (Show)
newtype Y = Y Char deriving (Show)
data Foobar a where
Foo :: X -> Y -> Foobar NoZoo
Bar :: X -> Y -> Foobar NoZoo
Zoo :: Foobar NoZoo -> Foobar Zoo
foobar :: Foobar a -> X
foobar f = case f of
Foo x _ -> x
Zoo g -> foobar g
main :: IO ()
main = putStrLn . show $ foobar (Zoo $ Foo (X 1) (Y 'a'))
Could you post a test case?
Thinking about this more carefully, I started out with
data Foobar a where
Foo :: X -> Y -> Foobar a
Zoo :: Foobar a -> Foobar Zoo
which is no good, because Zoo can be nested arbitrarily deep. So I
tried to change it to
data Foobar a where
Foo :: X -> Y -> Foobar NoZoo
Zoo :: Foobar NoZoo -> Foobar Zoo
But *actually*, changing the second type signature only is
sufficient. Indeed, it turns out I don't *want* to change the first
one. I want to use the type system to track whether Zoo "may" or
"may not" be present, not whether it "is" or "is not" present. In
other words, I want Foobar Zoo to mean that there *might* be a Zoo
in there, but there isn't guaranteed to be one. But I want Foobar
NoZoo to be guaranteed not to contain Zoo.
So anyway... my program now uses GADTs, I've spent ages chasing down
all the typechecker errors (and, inevitably, in some places
clarifying what the code is actually supposed to do), and my program
now typechecks and does what it did before, except with slightly
more type safety. (In particular, I've deleted several calls to
"error" now, because those case alternatives can never occur).
Thanks to all the people for your help! :-D
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
