[Haskell-cafe] Restrict values in type

[Daniil Frumin]

I think so, yes. Singleton library already provides Bool and (:||)
type family (or)

On Wed, Jan 15, 2014 at 6:13 PM, Nicolas Trangez <nicolas at incubaid.com> wrote:
> 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