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
