[Haskell-cafe] Strange typing?

[Brent Yorgey]

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