[Haskell-cafe] Restrict values in type
Luke Clifton
ltclifton at gmail.com
Thu Jan 16 02:36:40 UTC 2014
Thanks Andras and Daniil for pointing out the singletons package.
I will need to look into this in more detail to fully understand what is
going on. Seems I'm jumping into the deep end with this. Type families have
move up in my reading list!
On Wed, Jan 15, 2014 at 9: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
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140116/19fc8c79/attachment.html>
More information about the Haskell-Cafe
mailing list