<html><body>So after having played with it a little, it looks like GADTs are the way to go. The method of manipulating the module system won't work because of two reasons:<br><br>A) How can a user pattern match against data constructors that are hidden by the module system?<br>B) It's an awful hack.<br><p><br></p><p>Do I understand correctly that with the GADTs I have to create my own record selectors/lenses separately?</p><p><br></p><p>Thanks,</p><p>Timothy</p><p><br></p><p>---------- Původní zpráva ----------<br>Od: Austin Seipp <mad.one@gmail.com><br>Datum: 31. 8. 2012<br>Předmět: Re: [Haskell-cafe] Over general types are too easy to make.</p><blockquote>What you are essentially asking for is a refinement on the type of<br>'BadFoo' in the function type, such that the argument is provably<br>always of a particular constructor.<br><br>The easiest way to encode this kind of property safely with Haskell<br>2010 as John suggested is to use phantom types and use the module<br>system to ban people from creating BadFrog's etc directly, by hiding<br>the constructors. That is, you need a smart constructor for the data<br>type. This isn't an uncommon idiom and sometimes banning people (by<br>default) from those constructors is exactly what you have to do. It's<br>also portable and easy to understand.<br><br>Alternatively, you can use GADTs to serve witness to a type equality<br>constraint, and this will discharge some of the case alternatives you<br>need to write. It's essentially the kind of refinement you want:<br><br>data Frog<br>data Bar<br><br>data Foo x :: * where<br> Bar :: Int -> Foo Bar<br> Frog :: String -> Int -> Foo Frog<br><br>You can't possibly then pattern match on the wrong case if you specify<br>the type, because that would violate the type equality constraint:<br><br>deFrog :: Foo Frog -> String<br>deFrog (Frog x _) = x<br>-- not possible to define 'deFrog (Bar ...) ...', because that would<br>violate the constraint 'Foo x' ~ 'Foo Frog'<br><br>It's easier to see how this equality constraint works if you<br>deconstruct the GADT syntax into regular equality constraints:<br><br>data Bar<br>data Frog<br><br>data Foo x =<br> (x ~ Bar) => Bar Int<br> | (x ~ Frog) => Frog String Int<br><br>It's then obvious the constructor carries around the equality<br>constraint at it's use sites, such as the definition of 'deFrog'<br>above.<br><br>Does this solve your problem?<br><br>On Fri, Aug 31, 2012 at 1:00 PM, <timothyhobbs@seznam.cz> wrote:<br>> I'd have to say that there is one(and only one) issue in Haskell that bugs<br>> me to the point where I start to think it's a design flaw:<br>><br>> It's much easier to type things over generally than it is to type things<br>> correctly.<br>><br>> Say we have a<br>><br>>>data BadFoo =<br>>> BadBar{<br>>> badFoo::Int} |<br>>> BadFrog{<br>>> badFrog::String,<br>>> badChicken::Int}<br>><br>> This is fine, until we want to write a function that acts on Frogs but not<br>> on Bars. The best we can do is throw a runtime error when passed a Bar and<br>> not a Foo:<br>><br>>>deBadFrog :: BadFoo -> String<br>>>deBadFrog (BadFrog s _) = s<br>>>deBadFrog BadBar{} = error "Error: This is not a frog."<br>><br>> We cannot type our function such that it only takes Frogs and not Bars.<br>> This makes what should be a trivial compile time error into a nasty runtime<br>> one :(<br>><br>> The only solution I have found to this is a rather ugly one:<br>><br>>>data Foo = Bar BarT | Frog FrogT<br>><br>> If I then create new types for each data constructor.<br>><br>>>data FrogT = FrogT{<br>>> frog::String,<br>>> chicken::Int}<br>><br>>>data BarT = BarT{<br>>> foo :: Int}<br>><br>> Then I can type deFrog correctly.<br>><br>>>deFrog :: FrogT -> String<br>>>deFrog (FrogT s _) = s<br>><br>> But it costs us much more code to do it correctly. I've never seen it done<br>> correctly. It's just too ugly to do it right :/ and for no good reason. It<br>> seems to me, that it was a design mistake to make data constructors and<br>> types as different entities and this is not something I know how to fix<br>> easily with the number of lines of Haskell code in existence today :/<br>><br>>>main = do<br>>> frog <- return (Frog (FrogT "Frog" 42))<br>>> print $<br>>> case frog of<br>>> (Frog myFrog) -> deFrog myFrog<br>>> badFrog <- return (BadBar 4)<br>>> print $<br>>> case badFrog of<br>>> (notAFrog@BadBar{}) -> deBadFrog notAFrog<br>><br>> The ease with which we make bad design choices and write bad code(in this<br>> particular case) is tragically astounding.<br>><br>> Any suggestions on how the right way could be written more cleanly are very<br>> welcome!<br>><br>> Timothy Hobbs<br>><br>> _______________________________________________<br>> Haskell-Cafe mailing list<br>> Haskell-Cafe@haskell.org<br>> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>><br><br><br><br>-- <br>Regards,<br>Austin</blockquote></body></html>