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

On Sat, Sep 1, 2012 at 5:18 AM, 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

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, 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@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Regards, Austin

-- Regards, Austin