[Haskell-cafe] Over general types are too easy to make.

[timothyhobbs at seznam.cz]

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:

A) How can a user pattern match against data constructors that are hidden by
the module system?
B) It's an awful hack.




Do I understand correctly that with the GADTs I have to create my own record
selectors/lenses separately?




Thanks,

Timothy




---------- Původní zpráva ----------
Od: Austin Seipp <mad.one at gmail.com>
Datum: 31. 8. 2012
Předmět: Re: [Haskell-cafe] Over general types are too easy to make.
"What you are essentially asking for is a refinement on the type of
'BadFoo' in the function type, such that the argument is provably
always of a particular constructor.

The easiest way to encode this kind of property safely with Haskell
2010 as John suggested is to use phantom types and use the module
system to ban people from creating BadFrog's etc directly, by hiding
the constructors. That is, you need a smart constructor for the data
type. This isn't an uncommon idiom and sometimes banning people (by
default) from those constructors is exactly what you have to do. It's
also portable and easy to understand.

Alternatively, you can use GADTs to serve witness to a type equality
constraint, and this will discharge some of the case alternatives you
need to write. It's essentially the kind of refinement you want:

data Frog
data Bar

data Foo x :: * where
Bar :: Int -> Foo Bar
Frog :: String -> Int -> Foo Frog

You can't possibly then pattern match on the wrong case if you specify
the type, because that would violate the type equality constraint:

deFrog :: Foo Frog -> String
deFrog (Frog x _) = x
-- not possible to define 'deFrog (Bar ...) ...', because that would
violate the constraint 'Foo x' ~ 'Foo Frog'

It's easier to see how this equality constraint works if you
deconstruct the GADT syntax into regular equality constraints:

data Bar
data Frog

data Foo x =
(x ~ Bar) => Bar Int
| (x ~ Frog) => Frog String Int

It's then obvious the constructor carries around the equality
constraint at it's use sites, such as the definition of 'deFrog'
above.

Does this solve your problem?

On Fri, Aug 31, 2012 at 1:00 PM, <timothyhobbs at seznam.cz> wrote:
> I'd have to say that there is one(and only one) issue in Haskell that bugs
> me to the point where I start to think it's a design flaw:
>
> It's much easier to type things over generally than it is to type things
> correctly.
>
> Say we have a
>
>>data BadFoo =
>> BadBar{
>> badFoo::Int} |
>> BadFrog{
>> badFrog::String,
>> badChicken::Int}
>
> This is fine, until we want to write a function that acts on Frogs but not
> on Bars. The best we can do is throw a runtime error when passed a Bar and
> not a Foo:
>
>>deBadFrog :: BadFoo -> String
>>deBadFrog (BadFrog s _) = s
>>deBadFrog BadBar{} = error "Error: This is not a frog."
>
> We cannot type our function such that it only takes Frogs and not Bars.
> This makes what should be a trivial compile time error into a nasty 
runtime
> one :(
>
> The only solution I have found to this is a rather ugly one:
>
>>data Foo = Bar BarT | Frog FrogT
>
> If I then create new types for each data constructor.
>
>>data FrogT = FrogT{
>> frog::String,
>> chicken::Int}
>
>>data BarT = BarT{
>> foo :: Int}
>
> Then I can type deFrog correctly.
>
>>deFrog :: FrogT -> String
>>deFrog (FrogT s _) = s
>
> But it costs us much more code to do it correctly. I've never seen it done
> correctly. It's just too ugly to do it right :/ and for no good reason. It
> seems to me, that it was a design mistake to make data constructors and
> types as different entities and this is not something I know how to fix
> easily with the number of lines of Haskell code in existence today :/
>
>>main = do
>> frog <- return (Frog (FrogT "Frog" 42))
>> print $
>> case frog of
>> (Frog myFrog) -> deFrog myFrog
>> badFrog <- return (BadBar 4)
>> print $
>> case badFrog of
>> (notAFrog at BadBar{}) -> deBadFrog notAFrog
>
> The ease with which we make bad design choices and write bad code(in this
> particular case) is tragically astounding.
>
> Any suggestions on how the right way could be written more cleanly are 
very
> welcome!
>
> Timothy Hobbs
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
(http://www.haskell.org/mailman/listinfo/haskell-cafe)
>



-- 
Regards,
Austin"
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120901/48d33b38/attachment.htm>