[Haskell-cafe] Restrict values in type

[Nicolas Trangez]

On Wed, 2014-01-15 at 13:55 +0000, Andras Slemmer wrote:
> > I have been looking at DataKinds and GADTs, but I can't quite figure out
> if they actually help me here at all.
> You are on the right track. With DataKinds and GADTs you can create an
> index type for PenShape:
> 
> data Shape = Circle | Rectangle | Arbitrary
> 
> data PenShape s where
>     PenCircle :: Float -> PenShape Circle
>     PenRectangle :: Float -> Float -> PenShape Rectangle
>     ArbitraryPen :: PenShape Arbitrary
> 
> You can use this index 's' to restrict PenShape to a particular
> constructor, or none at all:
> 
> data Stroke where
>     Spot :: Point -> PenShape s -> Stroke -- any shape allowed
>     Arc :: Point -> Point -> Point -> PenShape Circle -> Stroke -- only
> circle
> 
> In the Spot case the type variable 's' will be existentially hidden,
> meaning any type can go there.
> 
> The tricky part comes when you want to have a notion of "or" in the case of
> Line. We basically need decidable type equality for this. Let's assume we
> have a way of deciding whether two lifted Shape types are equal and we get
> back a lifted Bool. Now we can write a type level "or" function:
> 
> type family Or (a :: Bool) (b :: Bool) :: Bool
> type instance Or False False = False
> type instance Or True b = True
> type instance Or a True = True
> 
> Now the Line case in the GADT would look something like this:
> 
>     Line :: Or (s :== Circle) (s :== Rectangle) ~ True =>       -- circle
> or rectangle
>             Point -> Point -> PenShape s -> Stroke
> 
> where :== is our type equality predicate. You can write this by hand if
> you'd like but it's pretty tedious and really should be inferred by the
> compiler or some automated process. And indeed the 'singletons' library
> does just this (and more), all you need to do is wrap your Shape definition
> in some th:
> 
> $(singletons [d|data Shape = Circle | Rectangle | Arbitrary deriving (Eq)|])
> 
> And voila you have a nice type safe datastructure:)
> 
> A full module can be found here: http://lpaste.net/98527

I never used the 'singletons' library (yet), but since you're using it
already, can't what's provided by Data.Singletons.Bool (or
Data.Singletons.Prelude) be used instead of a hand-rolled type-level
bool?

Nicolas