On Fri, Mar 19, 2010 at 03:15:02PM +0000, Ozgur Akgun wrote:
Hi Cafe!
Disclaimer: I know what I'm going to ask is now available as a language feature normally. And sorry for the subject of this message, I couldn't compe up with a good&descriptive subject.
Is there any way to limit a functions type, not by a data type but by a group of constructors of a data type? If not, what would be the *right* thing to do to achieve this level of type safety?
data DT1 = X | Y | Z data DT2 = A | B | C | D
func1 :: DT1 -> DT2 -- instead of this func1' :: (X|Y) -> (B|C) -- i want sth. like this. (| means or)
The standard way to do this is with GADTs and phantom type parameters. Something like this:
data XY data NotXY data BC data NotBC
data DT1 a where X :: DT1 XY Y :: DT1 XY Z :: DT1 NotXY
data DT2 a where A :: DT1 NotBC ... etc.
func1 :: DT1 XY -> DT2 BC ...
Every value of DT1 is tagged with an extra piece of information at the type level saying whether it is X or Y, or not. These extra types are known as "phantom type parameters" since nothing of those types actually show up in the values of the data type (indeed, XY, NotXY, and so on have no values) but they are only there to provide some extra information at the type level. Of course, the only problem with this approach is that if you want another function that only takes Y or Z, you are out of luck without some fancier type hackery. However, if you wish to know about a nice approach to said fancier type hackery, see Wouter Swierstra's paper "Data Types a la Carte" [1]. -Brent [1] http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf