Niklas Broberg wrote:

On Sun, Jun 21, 2009 at 9:24 PM, Andrew Coppin wrote:

...

data Foobar = Foo Foobar | Bar Foobar | Zoo Foobar

I want the type system to track whether or not Zoo has been used in a specific value. Sure, you can check for it at runtime, but I'd be happier if the type system can guarantee its absence when required.

That's what GADTs are for:

data Flag = HasZoo | NoZoo

data Foobar a where Foo :: Foobar a -> Foobar a Bar :: Foobar a -> Foobar a Zoo :: Foobar a -> Foobar HasZoo

...so I use "Foobar x" to mean any kind of value, "Foobar NoZoo" for a value that definitely doesn't contain Zoo, and "Foobar HasZoo" for... one that definitely does? Or maybe does? (Not that I care about this, but for completeness I'd like to know.) A slight complication is that Foobar refers to a second type which exhibits a similar behaviour - but presumably I can utilise the same solution there also...

On Sun, Jun 21, 2009 at 4:00 PM, Andrew Coppin wrote:

Niklas Broberg wrote:

...

On Sun, Jun 21, 2009 at 9:24 PM, Andrew Coppin wrote:

...

I want the type system to track whether or not Zoo has been used in a specific value. Sure, you can check for it at runtime, but I'd be happier if the type system can guarantee its absence when required.

That's what GADTs are for:

... ...so I use "Foobar x" to mean any kind of value, "Foobar NoZoo" for a value that definitely doesn't contain Zoo, and "Foobar HasZoo" for... one that definitely does? Or maybe does? (Not that I care about this, but for completeness I'd like to know.)

If you don't need code that's polymorphic between Foobar HasZoo and Foobar NoZoo, you could just newtype Foobar and only export smart constructors. module NoZoo (NoZoo, noZoo, mkNZ, mkNZ', unNZ) where newtype NoZoo = NZ Foobar noZoo :: Foobar -> Bool noZoo = ... mkNZ :: Foobar -> NoZoo mkNZ = NZ . assert "Zoo" . noZoo mkNZ' :: Foobar -> Maybe NoZoo mkNZ' x | noZoo x = Just x | otherwise = Nothing unNZ :: NoZoo -> Foobar unNZ (NZ x) = x Assuming noZoo is written correctly, this is enough to guarantee that unNZ never produces a value of Foobar containing Zoo. Oleg Kiselyov and Chung-chieh Shan have written about this. Try http://okmij.org/ftp/Computation/lightweight-dependent-typing.html or search for "lightweight static capabilities". -- Dave Menendez http://www.eyrie.org/~zednenem/

Niklas Broberg wrote:

That's what GADTs are for:

data Flag = HasZoo | NoZoo

data Foobar a where Foo :: Foobar a -> Foobar a Bar :: Foobar a -> Foobar a Zoo :: Foobar a -> Foobar HasZoo

Ouch #1: This appears to instantly disable deriving the Eq, Ord and Show instances I want. :-/

Brent Yorgey wrote:

On Sun, Jun 21, 2009 at 09:16:12PM +0100, Andrew Coppin wrote:

...

Niklas Broberg wrote:

...

That's what GADTs are for:

data Flag = HasZoo | NoZoo

data Foobar a where Foo :: Foobar a -> Foobar a Bar :: Foobar a -> Foobar a Zoo :: Foobar a -> Foobar HasZoo

Ouch #1: This appears to instantly disable deriving the Eq, Ord and Show instances I want. :-/

Ah, yes, that is a pain. Maybe try playing around with tools like Data.Derive? I haven't played with them much myself so I don't know if they will help.

Not nearly as annoying as this: data Foobar a where Foo :: X -> Y -> Foobar NoZoo Bar :: X -> Y -> Foobar NoZoo Zoo :: Foobar NoZoo -> Foobar Zoo For some reason, if I do this I get endless type check errors. I have to change the top two back to Foobar a before it will work. *sigh*

Niklas Broberg wrote:

...

Not nearly as annoying as this:

data Foobar a where Foo :: X -> Y -> Foobar NoZoo Bar :: X -> Y -> Foobar NoZoo Zoo :: Foobar NoZoo -> Foobar Zoo

For some reason, if I do this I get endless type check errors. I have to change the top two back to Foobar a before it will work. *sigh*

Well, that means something very different obviously. It means Zoo constructors can never take Zoo arguments.

...which would be precisely what I want, yes. :-)

Why would that give you type check errors? If it does, you're doing something else wrong.

I think (I'm not sure) it's because of stuff like this: foobar :: Foobar a -> X foobar f = case f of Foo x y -> ... Zoo g -> foobar g The first case implies that f :: Foobar NoZoo, while the second implies that f :: Foobar Zoo. Apparently this seemingly reasonable construct does not type-check...

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

On Tue, Jun 23, 2009 at 9:25 PM, Ross Mellgren wrote:

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?

You might have a higher-arity constructor and want to construct things like, Qux (Foo X Y) (Zoo (Bar X Y)) What's the type of Qux? If Foobar Zoo means "might contain a Zoo", then you can just declare data Foobar a where Foo :: X -> Y -> Foobar a Bar :: X -> Y -> Foobar a Zoo :: Foobar NoZoo -> Foobar Zoo Qux :: Foobar a -> Foobar a -> Foobar a and everything is fine. On the other hand, if Foobar Zoo means "definitely contains a Zoo", then you need type families to express the type of Qux. Qux :: Foobar a -> Foobar b -> Foobar (EitherZoo a b) type family EitherZoo a b :: * type instance EitherZoo Zoo Zoo = Zoo type instance EitherZoo NoZoo Zoo = Zoo type instance EitherZoo Zoo NoZoo = Zoo type instance EitherZoo NoZoo NoZoo = NoZoo -- Dave Menendez http://www.eyrie.org/~zednenem/

On Jun 22, 2009, at 14:43 , Andrew Coppin wrote:

data Foobar a where Foo :: X -> Y -> Foobar NoZoo Bar :: X -> Y -> Foobar NoZoo Zoo :: Foobar NoZoo -> Foobar Zoo

For some reason, if I do this I get endless type check errors. I have to change the top two back to Foobar a before it will work. *sigh*

That's probably because ghc can't fix a type for Foobar a if you never actually use a anywhere. Functional dependencies could solve that, but giving ghc a way to infer a type for it by using it where it doesn't affect anything important is easier and doesn't risk possible(?) weird interactions between FDs and GADTs. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH