I think so, yes. Singleton library already provides Bool and (:||)
type family (or)
On Wed, Jan 15, 2014 at 6:13 PM, 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
-- Sincerely yours, -- Daniil