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

[Austin Seipp]

On Sat, Sep 1, 2012 at 5:18 AM,  <timothyhobbs at seznam.cz> wrote:
> 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?

You can't directly, but the correct way to do this if you want it is
to use view patterns and export a view specifically for your hidden
data type. This gives you some extra flexibility in what you give to
clients, although view patterns add a little verbosity.

> B) It's an awful hack.

To each his own. The module system in Haskell serves as nothing more
than a primitive namespace really, so I don't see why hiding things by
default in namespaces seems like a hack (you should of course export
hidden stuff too, but in another module, as a last ditch effort in
case users need it. Sometimes this is very very useful.)

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

I don't know. I suppose it depends on the lens library in question.
Ones that use template haskell to drive accessors may, or may not,
work (I suppose it would depend on whether or not the derivation is
prepared to deal with GADTs when invoked, which isn't guaranteed -
Template Haskell is kind of awful like that.)

> 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
>>
>
>
>
> --
> Regards,
> Austin



-- 
Regards,
Austin