Restrict values in type

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
22 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Restrict values in type

Luke Clifton
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Carter Schonwald
Hey Luke,
have you seen the diagrams project? http://projects.haskell.org/diagrams/
they've struggled through some of the same problems, and they've worked very hard to write a power user friendly expressive DSL lib for that problem domain.
check it out!
-Carter


On Sun, Jan 12, 2014 at 10:38 PM, Luke Clifton <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Bob Ippolito
In reply to this post by Luke Clifton
You can have a heterogeneous list of items that implement a typeclass if you have a wrapper that uses ExistentialQuantification. See http://www.haskell.org/haskellwiki/Heterogenous_collections

I don't have enough experience with the type system to properly answer your actual question though.


On Sun, Jan 12, 2014 at 7:38 PM, Luke Clifton <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Luke Clifton
In reply to this post by Carter Schonwald
Hi Carter,

Yes, I have seen the diagrams project, and in fact am hoping to use them when I actually get to rendering.

Perhaps, I should have provided more info to try and explain why I am doing this.

I am trying to implement a Gerber file viewer (and maybe editor... we'll see)


I am using parsec to parse the gerber format and build my gerber data type so that I can make modifications to it, and write it back out.

I'll take a closer look at diagrams source and see if I can come up with some inspiration.

Thanks,

Luke



On Mon, Jan 13, 2014 at 11:55 AM, Carter Schonwald <[hidden email]> wrote:
Hey Luke,
have you seen the diagrams project? http://projects.haskell.org/diagrams/
they've struggled through some of the same problems, and they've worked very hard to write a power user friendly expressive DSL lib for that problem domain.
check it out!
-Carter


On Sun, Jan 12, 2014 at 10:38 PM, Luke Clifton <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Luke Clifton
In reply to this post by Bob Ippolito
Hi Bob,

You can have a heterogeneous list of items that implement a typeclass if you have a wrapper that uses ExistentialQuantification. See http://www.haskell.org/haskellwiki/Heterogenous_collections

Hmm.. I'll take a closer look at that. It might be good enough, though I would prefer to be able to pattern match on the elements in the list.

Regards,

Luke

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Daniil Frumin
In reply to this post by Luke Clifton
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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Sincerely yours,
-- Daniil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Andras Slemmer
> 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 <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Sincerely yours,
-- Daniil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Daniil Frumin
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
>> > [hidden email]
>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >
>>
>>
>>
>> --
>> Sincerely yours,
>> -- Daniil
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>



--
Sincerely yours,
-- Daniil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Nicolas Trangez
In reply to this post by Andras Slemmer
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Jake McArthur
In reply to this post by Luke Clifton

You can get some kind of subtyping out of type classes. Then it's just a matter of making a few different instances so you can do what you want with them.

class Circle a where
  circle :: Float -> a

class Rectangle a where
  rectangle :: Float -> Float -> a

class (Circle a, Rectangle a) => PenShape a where
  arbitraryPen :: ... -> a

data Stroke = forall p. (Circle p, Rectangle p) => Line Point Point p
            | forall p. Circle p => Arc Point Point Point p
            | forall p. PenShape p => Spot Point p

- Jake

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Jake McArthur

Sorry, I used existential types but should have used universal types.

On Jan 15, 2014 9:25 AM, "Jake McArthur" <[hidden email]> wrote:

You can get some kind of subtyping out of type classes. Then it's just a matter of making a few different instances so you can do what you want with them.

class Circle a where
  circle :: Float -> a

class Rectangle a where
  rectangle :: Float -> Float -> a

class (Circle a, Rectangle a) => PenShape a where
  arbitraryPen :: ... -> a

data Stroke = forall p. (Circle p, Rectangle p) => Line Point Point p
            | forall p. Circle p => Arc Point Point Point p
            | forall p. PenShape p => Spot Point p

- Jake

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Jake McArthur

This is what it should have been. Also, sorry for segmenting my emails.

data Stroke = Line Point Point (forall p. (Circle p, Rectangle p) => p)
            | Arc Point Point Point (forall p. Circle p => p)
            | Spot Point (forall p. PenShape p => p)

On Jan 15, 2014 9:26 AM, "Jake McArthur" <[hidden email]> wrote:

Sorry, I used existential types but should have used universal types.

On Jan 15, 2014 9:25 AM, "Jake McArthur" <[hidden email]> wrote:

You can get some kind of subtyping out of type classes. Then it's just a matter of making a few different instances so you can do what you want with them.

class Circle a where
  circle :: Float -> a

class Rectangle a where
  rectangle :: Float -> Float -> a

class (Circle a, Rectangle a) => PenShape a where
  arbitraryPen :: ... -> a

data Stroke = forall p. (Circle p, Rectangle p) => Line Point Point p
            | forall p. Circle p => Arc Point Point Point p
            | forall p. PenShape p => Spot Point p

- Jake

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Luke Clifton
Well that works wonderfully for parts of the problem.

listOfStrokes = [ Line point point (circle 5)
                , Line point point (rectangle 2 3)
                , Arc point point point (circle 2)
                , Spot point arbitraryPen
                , Spot point (circle 1)
                , Spot point (rectangle 1 1)
                ]


*Tmp> :t listOfStrokes
listOfStrokes :: [Stroke]

But how can I extract the information about the PenShape from such a structure?

I can't pattern match (unless there is some language extension I am missing).

case Arc point point point (circle 1) of
    (Arc _ _ _ (circle r)) -> r

<interactive>:67:14: Parse error in pattern: circle

This seems obvious to me because pattern matching works on data constructors (though I have often found that what I think is obvious is not always correct...). This would leave me to believe that, because there are no data constructors for Circle, Rectangle and PenShape that I couldn't pattern match on it.

I tried to add some functions to the various classes to figure it out, but that didn't seem to take me anywhere.






On Wed, Jan 15, 2014 at 10:29 PM, Jake McArthur <[hidden email]> wrote:

This is what it should have been. Also, sorry for segmenting my emails.

data Stroke = Line Point Point (forall p. (Circle p, Rectangle p) => p)
            | Arc Point Point Point (forall p. Circle p => p)
            | Spot Point (forall p. PenShape p => p)

On Jan 15, 2014 9:26 AM, "Jake McArthur" <[hidden email]> wrote:

Sorry, I used existential types but should have used universal types.

On Jan 15, 2014 9:25 AM, "Jake McArthur" <[hidden email]> wrote:

You can get some kind of subtyping out of type classes. Then it's just a matter of making a few different instances so you can do what you want with them.

class Circle a where
  circle :: Float -> a

class Rectangle a where
  rectangle :: Float -> Float -> a

class (Circle a, Rectangle a) => PenShape a where
  arbitraryPen :: ... -> a

data Stroke = forall p. (Circle p, Rectangle p) => Line Point Point p
            | forall p. Circle p => Arc Point Point Point p
            | forall p. PenShape p => Spot Point p

- Jake

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Luke Clifton
In reply to this post by Andras Slemmer
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Sincerely yours,
-- Daniil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

oleg-30
In reply to this post by Luke Clifton

The problem you have posed calls for so-called open unions. Open
unions come up all the time, and lots of solutions exists. Alas, they
are all a bit ad hoc. At Haskell Symposium I was advocating designing
a good solution once and for all.

The paper that introduced monad transformers showed one implementation
of open unions (of effects). The paper `data types a la carte' showed
another (essentially the same, trying to deemphasize its use of
overlapping instances). The Extensible effects paper has two more
solutions, one with Typeable and one without. You can use OpenUnions
from that paper if you install extensible-effects package. Using
singletons is yet another, quite heavy-weight solution.

I'd like to stress a much simpler solution, which requires no type
equality or GADTs or bleeding edge. It is a tagless-final solution. In
fact, it has been demonstrated already by Jake McArthur. I elaborate
and show the whole code.

Your original code defined PenShape as a data structure

> data PenShape = Circle Float
>     | Rectangle Float Float
>     | ArbitraryPen -- Stuff (not relevant)

I will define it as an expression in a very simple domain-specific
language of pen shapes.

> class CirclePen repr where
>     circle :: Float -> repr
>     -- other ways of constructing circles go here
>
> class RectPen repr where
>     rectangle :: Float -> Float -> repr
>
> class ArbitraryPen repr where
>     arbitrary :: () -> repr -- () stands for irrelevant stuff

Here repr is the meaning of a pan shape in a particular
interpretation. The same term can be interpreted in many ways
(compare: a Haskell code can be loaded into GHCi, compiled with GHC or
processed with Haddoc). One interpretation of pen shapes is to print
them out nicely:

data S = S{unS :: String}

instance CirclePen S where
  circle x = S $ "circle pen of radius " ++ show x

instance RectPen S where
  rectangle x y = S $ "rect pen " ++ show (x,y)
 
instance ArbitraryPen S where
  arbitrary () = S $ "arbitrary pen"

There probably will be other representations: defined only for
specific sets of pens (rather than all of them), see below for an example.

You ask how can you pattern-match on pen shapes. The answer is that in
taggless-final style, you don't pattern-match. You interpret. Quite
often the code becomes clearer. Enclosed is the complete code. For
(far) more explanation of tagless-final, please see the first part of

        http://okmij.org/ftp/tagless-final/course/lecture.pdf

{-# LANGUAGE RankNTypes #-}

module Im where

data Image = Image [Stroke]


-- As a data structure
{-
data PenShape = Circle Float
    | Rectangle Float Float
    | ArbitraryPen -- Stuff (not relevant)
-}

-- As a term in a simple language of shapes

class CirclePen repr where
    circle :: Float -> repr
    -- other ways of constructing circles go here

class RectPen repr where
    rectangle :: Float -> Float -> repr

class ArbitraryPen repr where
    arbitrary :: () -> repr -- () stands for irrelevant stuff

-- Let's define a few interpretations of pens

-- the Show interpretation, to print them
-- All pens support this interpretation
data S = S{unS :: String}

instance CirclePen S where
  circle x = S $ "circle pen of radius " ++ show x

instance RectPen S where
  rectangle x y = S $ "rect pen " ++ show (x,y)
 
instance ArbitraryPen S where
  arbitrary () = S $ "arbitrary pen"



-- Another interpretation: finite-dim pens. Only CirclePen and RectPen
-- support it
data FiniteDim = FiniteDim{unFD:: Float}

instance CirclePen FiniteDim where
  circle x = FiniteDim x
 
instance RectPen FiniteDim where
  rectangle x y = FiniteDim $ max x y


{-
data Stroke = Line Point Point PenShape
    | Arc Point Point Point PenShape
    | Spot Point PenShape
-}

type Point = (Float,Float)
p0 = (0,0)
p1 = (1,1)

data Stroke =
    Line Point Point (forall repr. (CirclePen repr, RectPen repr) => repr)
  | Arc Point Point (forall repr. (CirclePen repr) => repr)
  | Spot Point (forall repr.
                (CirclePen repr, RectPen repr, ArbitraryPen repr) => repr)


-- Let's make a an image

im1 = Image [
  Line p0 p1 (circle 10),
  Line p0 p1 (rectangle 1 2),
  -- The following will be a type error, as expected
  -- Arc p0 p1 (rectangle 1 2),
  Arc p0 p1 (circle 3),
  Spot p0 (rectangle 1 2),
  Spot p0 (arbitrary ())
  ]

-- If we add
--   Line p0 p1 (arbitrary ())
-- we get a type error with an informative message
{-
    Could not deduce (ArbitraryPen repr)
      arising from a use of `arbitrary'
    from the context (CirclePen repr, RectPen repr)
      bound by a type expected by the context:
                 (CirclePen repr, RectPen repr) => repr
-}

-- Let's print the list of strokes

show_strokes :: Image -> [String]
show_strokes (Image l) = map f l
 where
 f (Line p1 p2 pensh) = unwords ["Line", show (p1,p2), unS pensh]
 f (Arc p1 p2 pensh) = unwords ["Arc", show (p1,p2), unS pensh]
 f (Spot p1 pensh) = unwords ["Spot", show p1, unS pensh]

tshow = show_strokes im1
{-
["Line ((0.0,0.0),(1.0,1.0)) circle pen of radius 10.0",
 "Line ((0.0,0.0),(1.0,1.0)) rect pen (1.0,2.0)",
 "Arc ((0.0,0.0),(1.0,1.0)) circle pen of radius 3.0",
 "Spot (0.0,0.0) rect pen (1.0,2.0)","Spot (0.0,0.0) arbitrary pen"]
-}

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Luke Clifton
Thanks, that really cleared up a few of the questions I had about Jake McArthurs' code as well. The link you provided was a good read and shed some more light on the situation.

The only bit I don't quite understand is why the following code implies an "or" relation in the type constraint of repr.

> data Stroke =
>    Line Point Point (forall repr. (CirclePen repr, RectPen repr) => repr)
>  | Arc Point Point (forall repr. (CirclePen repr) => repr)
>  | Spot Point (forall repr.
>                (CirclePen repr, RectPen repr, ArbitraryPen repr) => repr)

To me this reads that repr should be both a CirclePen and a RectPen in order to satisfy the type constraint in the case of Line, but it seems that it is accepting a CirclePen or a RectPen (which is the desired behaviour, so I'm not complaining). 



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Daniil Frumin
Ah, it is a little bit confusing.

The type (forall repr. (CirclePen repr, RectPen repr) => repr) is
inhabited by a _represtentation_ that can be constructed  both by
'circle' and by 'rectangle'. So we can use any of those two functions
to construct a value of that type. (Such type is FiniteDim for
example). The Arc constructor, on the other hand, accepts only values
of type (forall repr. (CirclePen repr) => repr). We don't know
anything about the concrete representation type, we only know that we
can construct it using 'circle'.

Hth
-dan

On Thu, Jan 16, 2014 at 6:16 PM, Luke Clifton <[hidden email]> wrote:

> Thanks, that really cleared up a few of the questions I had about Jake
> McArthurs' code as well. The link you provided was a good read and shed some
> more light on the situation.
>
> The only bit I don't quite understand is why the following code implies an
> "or" relation in the type constraint of repr.
>
>> data Stroke =
>>    Line Point Point (forall repr. (CirclePen repr, RectPen repr) => repr)
>>  | Arc Point Point (forall repr. (CirclePen repr) => repr)
>>  | Spot Point (forall repr.
>>                (CirclePen repr, RectPen repr, ArbitraryPen repr) => repr)
>
> To me this reads that repr should be both a CirclePen and a RectPen in order
> to satisfy the type constraint in the case of Line, but it seems that it is
> accepting a CirclePen or a RectPen (which is the desired behaviour, so I'm
> not complaining).
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Sincerely yours,
-- Daniil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

Luke Clifton
In reply to this post by Luke Clifton

To me this reads that repr should be both a CirclePen and a RectPen in order to satisfy the type constraint in the case of Line, but it seems that it is accepting a CirclePen or a RectPen (which is the desired behaviour, so I'm not complaining). 


Having thought about it, it _IS_ saying that repr is an instance of both CirclePen and RectPen, which is why I can call either circle or rectangle in that context. The called function then decides the type, rather than the calling function.

PS: I got out of bed with this epiphany, so I may be incoherent and tired and not making any sense at all... 


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrict values in type

oleg-30

> The only bit I don't quite understand is why the following code implies an
> "or" relation in the type constraint of repr.

> > data Stroke =
> >    Line Point Point (forall repr. (CirclePen repr, RectPen repr) => repr)
> >  | Arc Point Point (forall repr. (CirclePen repr) => repr)
> >  | Spot Point (forall repr.
> >                (CirclePen repr, RectPen repr, ArbitraryPen repr) => repr)

> To me this reads that repr should be both a CirclePen and a RectPen in
> order to satisfy the type constraint in the case of Line, but it seems that
> it is accepting a CirclePen or a RectPen (which is the desired behaviour,
> so I'm not complaining).

This point is indeed confusing. Perhaps yet another explanation might
be helpful. Added to the already given, it might help reaching the
critical mass.

First, it seems that the dictionary passing implementation of type
classes makes things clearer. This implementation realizes,
informally, double arrow as a simple arrow. For example, the declaration

> class CirclePen repr where
>     circle :: Float -> repr

is translated to a dictionary declaration

> data CirclePenDict repr = CirclePenDict{circle :: Float -> repr}

and a bounded polymorphic function or value like

> CirclePen repr => repr
is realized as
> CirclePenDict repr -> repr
Double arrow turns simple arrow.

Therefore,

> data Stroke =
>     Line Point Point (forall repr. (CirclePen repr, RectPen repr) => repr)

becomes

> data Stroke =
>     Line Point Point (forall repr.
>         (CirclePenDict repr, RectPenDict repr) -> repr)

We can make two different lines, with the circle pen shape:
> -- Line p1 p2 (circle 10)
> stroke1 = Line' p0 p1 (\(circledict, rectdict) -> circle circledict 10)

or with the rectangular pen shape.
> -- Line p1 p2 (circle 10 20)
> stroke2 = Line' p0 p1 (\(circledict, rectdict) -> rectangle rectdict 10 20)

Obviously we cannot make Lines with the Arbitrary pen shape since we
will receive from the user only circledict and rectdict but no
arbitrarypendict.

Suppose we are communicating over a network. If I can send you
_either_ a boolean or an integer, you have to be prepared to handle
_both_. From a different point of view: if you send me the handler for
a boolean _and_ the handler for an integer, it becomes my choice which
one to invoke. (Incidentally, what I just described is a subset of
session types for pi-calculus.)

At this point de Morgan laws may spring to mind. Here is a related
explanation of using open records to implement open unions.

        http://okmij.org/ftp/Haskell/generics.html#PolyVariant








_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12