[Haskell-cafe] Type system trickery

[Ross Mellgren]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe