[Haskell-cafe] Restrict values in type
Daniil Frumin
difrumin at gmail.com
Wed Jan 15 14:13:07 UTC 2014
Oh, I didn't know that the singletons library provides the equality
type family, that's nice
On Wed, Jan 15, 2014 at 5:55 PM, Andras Slemmer <0slemi0 at gmail.com> 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
>
>
> On 13 January 2014 16:25, Daniil Frumin <difrumin at gmail.com> wrote:
>>
>> I devised the following (unarguably verbose) solution using the
>> singletons [1] library
>>
>> {-# LANGUAGE DataKinds, TypeFamilies, MultiParamTypeClasses #-}
>> {-# LANGUAGE TemplateHaskell, GADTs, FlexibleContexts #-}
>> module Image where
>> import Data.Singletons
>>
>> type Point = (Float,Float)
>>
>> $(singletons [d|
>> data Shape' = Circle' | Rectangle' | Arbitrary'
>> deriving (Eq)
>> data Stroke' = Line' | Arc' | Spot'
>> deriving (Eq)
>> |])
>>
>>
>> data PenShape shape where
>> Circle :: SingI Circle' => Float -> PenShape Circle'
>> Rectangle :: SingI Rectangle' => Float -> Float -> PenShape Rectangle'
>> ArbitraryPen :: PenShape Arbitrary'
>>
>> class AllowedStroke (a::Stroke') (b::Shape') where
>>
>> instance AllowedStroke Line' Circle'
>> instance AllowedStroke Line' Rectangle'
>> instance AllowedStroke Arc' Circle'
>> instance AllowedStroke Spot' Circle'
>> instance AllowedStroke Spot' Rectangle'
>> instance AllowedStroke Spot' Arbitrary'
>>
>> data Stroke where
>> Line :: AllowedStroke Line' a
>> => Point -> Point -> PenShape a -> Stroke
>> Arc :: AllowedStroke Arc' a
>> => Point -> Point -> Point -> PenShape a -> Stroke
>> Spot :: AllowedStroke Spot' a
>> => Point -> PenShape a -> Stroke
>>
>> {-
>> h> :t Line (1,1) (1,1) (Circle 3)
>> Line (1,1) (1,1) (Circle 3) :: Stroke
>> h> :t Line (1,1) (1,1) (Rectangle 3 3)
>> Line (1,1) (1,1) (Rectangle 3 3) :: Stroke
>> h> :t Line (1,1) (1,1) ArbitraryPen
>>
>> <interactive>:1:1:
>> No instance for (AllowedStroke 'Line' 'Arbitrary')
>> arising from a use of `Line'
>> Possible fix:
>> add an instance declaration for (AllowedStroke 'Line' 'Arbitrary')
>> In the expression: Line (1, 1) (1, 1) ArbitraryPen
>> -}
>>
>> --- unfortunately this still gives non-exhaustive pattern match
>> --- warning :(
>> showStroke :: Stroke -> String
>> showStroke (Line _ _ (Circle _)) = "Line + Circle"
>> showStroke (Line _ _ (Rectangle _ _)) = "Line + Rect"
>> showStroke (Arc _ _ _ (Circle _)) = "Arc"
>> showStroke (Spot _ _) = "Spot"
>>
>> The shortcomings of this approach are the following:
>> - verbosity and repetition (eg: Shape' and Shape)
>> - still gives pattern matching warning ( I suspect that's because
>> typeclasses are open and there is really no way of determining whether
>> something is an 'AllowedStroke' or not)
>>
>> Feel free to improve the code and notify the list :)
>>
>> [1] http://hackage.haskell.org/package/singletons
>>
>> On Mon, Jan 13, 2014 at 7:38 AM, Luke Clifton <ltclifton at gmail.com> wrote:
>> > Hi,
>> >
>> > I'm quite new to Haskell, and have been loving exploring it. I've always
>> > been a huge fan of languages that let me catch errors at compile time,
>> > finding dynamic languages like Python a nightmare to work in. I'm
>> > finding
>> > with Haskell I can take this compile time checking even further than
>> > most
>> > static languages and it has gotten me rather excited. So I was wondering
>> > if
>> > there is a Haskell way of solving my problem.
>> >
>> > I'm trying to represent an image made up of a list of strokes. Strokes
>> > are
>> > either lines, arcs or spots, and can be made using different pen shapes.
>> >
>> > data Image = Image [Stroke]
>> >
>> > data Stroke = Line Point Point PenShape
>> > | Arc Point Point Point PenShape
>> > | Spot Point PenShape
>> >
>> > data PenShape = Circle Float
>> > | Rectangle Float Float
>> > | ArbitraryPen -- Stuff (not relevant)
>> >
>> > And this is all great and works.
>> >
>> > But now I have a problem. I want to extend this such that Arc strokes
>> > are
>> > only allowed to have the Circle pen shape, and Lines are only allowed to
>> > have the Rectangle or Circle pen shapes.
>> >
>> > What is the best way of enforcing this in the type system.
>> >
>> > I could make more Strokes like LineCircle, LineRectangle, Arc,
>> > PointCircle,
>> > PointRectangle, PointArbitrary and get rid of the PenShape type
>> > altogether.
>> > But this doesn't really feel good to me (and seems like the amount of
>> > work I
>> > have to do is bigger than it needs to be, especially if I added more
>> > basic
>> > pen shapes).
>> >
>> > I thought about making the different PenShapes different types, using
>> > typeclasses and making Stroke an algebraic data type, but then my
>> > strokes
>> > would be of different types, and I wouldn't be able to have a list of
>> > strokes.
>> >
>> > I have been looking at DataKinds and GADTs, but I can't quite figure out
>> > if
>> > they actually help me here at all.
>> >
>> > I'm sure there is a way to do this, I'm just not googling properly.
>> >
>> > What I want to write is...
>> >
>> > data Image = Image [Stroke]
>> >
>> > data Stroke = Line Point Point (Circle or Rectangle)
>> > | Arc Point Point Point Circle
>> > | Spot Point PenShape
>> >
>> > data PenShape = Circle Float
>> > | Rectangle Float Float
>> > | ArbitraryPen -- Stuff (not relevant)
>> >
>> > Regards,
>> >
>> > Luke
>> >
>> > _______________________________________________
>> > Haskell-Cafe mailing list
>> > Haskell-Cafe at haskell.org
>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >
>>
>>
>>
>> --
>> Sincerely yours,
>> -- Daniil
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
--
Sincerely yours,
-- Daniil
More information about the Haskell-Cafe
mailing list