Re: [Haskell-cafe] Type system trickery
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
Re: [Haskell-cafe] Type system trickery
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] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon universityKF8NH PGP.sig Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
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
Re: [Haskell-cafe] Type system trickery
On Tue, Jun 23, 2009 at 9:25 PM, Ross Mellgrenrmm-hask...@z.odi.ac 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 d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
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. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
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* ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
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, so you could only have at most one Zoo constructor at the outermost level, having either a Foo or a Bar inside it. Why would that give you type check errors? If it does, you're doing something else wrong. Cheers, /Niklas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
Andrew Coppin said:
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 code snippet works for me, so I think you're doing something else
wrong or I transcribed wrong
My code in full:
-
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data NoZoo
data Zoo
data Place a where
Office :: String - Int - Place NoZoo
Home :: String - Int - Place NoZoo
Zoo:: Place NoZoo - Place Zoo
-
It works fine (but I absolutely agree the lack of deriving is frustrating):
-
*Main let x = Zoo (Office 9th street 3342)
*Main let y = Home Friends House 4422
*Main :t x
x :: Place Zoo
*Main :t y
y :: Place NoZoo
*Main
And if you want to change it wrt Niklas's comments:
---
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data NoZoo
data Zoo
data Place a where
Office :: String - Int - Place NoZoo
Home :: String - Int - Place NoZoo
Zoo:: Place a - Place Zoo
---
Which works:
---
*Main let x = Zoo (Zoo (Office 9th street 3342))
*Main let y = Home Friends House 4422
*Main :t x
x :: Place Zoo
*Main :t y
y :: Place NoZoo
-
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
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... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
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?
On Jun 22, 2009, at 3:34 PM, Andrew Coppin wrote:
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...
___
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
Re: [Haskell-cafe] Type system trickery
Am Sonntag 21 Juni 2009 21:24:24 schrieb Andrew Coppin: I have a datatype with about a dozen constructors. I'd like to find a way to use the type system to prevent one of the constructors from being used in certain places. But I can't think of a way to do that. 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. I tried this: data Zoo x = Zoo x | NoZoo x data GeneralFoobar f = Foo f | Bar f type Foobar = GeneralFoobar Foobar type FoobarZ = GeneralFoobar (Zoo FoobarZ) but the type checker seems to not like it. (Plus I now have to wade through miles of NoZoo wrappers everywhere.) The other alternative is to just duplicate the entire data declaration, sans the Zoo constructor... but I'd obviously prefer not to have to do that. (E.g., if I ever need to alter the declaration, I now have two copies to keep in sync.) Suggestions? GADTs? data Okay data HasZoo data Aye data Nay class IsOkay a b | a - b where instance IsOkay Okay Aye where instance IsOkay HasZoo Nay where data Foobar where Bling :: Foobar a Foo :: Foobar a - Foobar a Bar :: Foobar a - Foobar a Zoo :: Foobar a - Foobar HasZoo use :: (IsOkay a Aye) = Foobar a - whatever ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
Niklas Broberg wrote: On Sun, Jun 21, 2009 at 9:24 PM, Andrew Coppinandrewcop...@btinternet.com 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... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
On Sun, Jun 21, 2009 at 9:24 PM, Andrew Coppinandrewcop...@btinternet.com wrote: I have a datatype with about a dozen constructors. I'd like to find a way to use the type system to prevent one of the constructors from being used in certain places. But I can't think of a way to do that. 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 f :: Foobar NoZoo - Int f foobar = ... -- foobar cannot be Zoo here Cheers, /Niklas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
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. :-/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
That's what GADTs are for: data Flag = HasZoo | NoZoo Eh, I wrote this a bit fast obviously (no dependent types here). Like Daniel Fischer wrote, these should rather be separate data types, i.e. data HasZoo data NoZoo The rest is still correct though. 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.) Yep, you are correct. Actually, you don't have to use NoZoo, you could use e.g. Foobar () or Foobar (Maybe Bool) if you like. Anything that isn't HasZoo. Cheers, /Niklas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
On Sun, Jun 21, 2009 at 4:00 PM, Andrew Coppinandrewcop...@btinternet.com wrote: Niklas Broberg wrote: On Sun, Jun 21, 2009 at 9:24 PM, Andrew Coppinandrewcop...@btinternet.com 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 d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system trickery
David Menendez wrote: 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. Unfortunately I want to be able to print both of them out. (After all, the printing algorithm is identical whether Zoo is present or not - except that if Zoo isn't there, you don't need to handle Zoo!) Nice idea though. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
