[Haskell-cafe] Restrict values in type

Showing 1-24 of 24 messages
[Haskell-cafe] Restrict values in type Luke Clifton 1/12/14 7:38 PM
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
Re: [Haskell-cafe] Restrict values in type Carter Schonwald 1/12/14 7:55 PM
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


_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Restrict values in type Bob Ippolito 1/12/14 7:58 PM
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.


_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Restrict values in type Luke Clifton 1/12/14 8:09 PM
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

Re: [Haskell-cafe] Restrict values in type Luke Clifton 1/12/14 8:12 PM
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
Re: [Haskell-cafe] Restrict values in type Daniil Frumin 1/13/14 8:25 AM
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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskel...@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Sincerely yours,
-- Daniil
Re: [Haskell-cafe] Restrict values in type Andras Slemmer 1/15/14 5:55 AM
> 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
Re: [Haskell-cafe] Restrict values in type Daniil Frumin 1/15/14 6:13 AM
Oh, I didn't know that the singletons library provides the equality
type family, that's nice
Re: [Haskell-cafe] Restrict values in type Nicolas Trangez 1/15/14 6:13 AM
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
Re: [Haskell-cafe] Restrict values in type Daniil Frumin 1/15/14 6:19 AM
I think so, yes. Singleton library already provides Bool and (:||)
type family (or)
--
Sincerely yours,
-- Daniil
Re: [Haskell-cafe] Restrict values in type Jake McArthur 1/15/14 6:25 AM

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

_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Restrict values in type Jake McArthur 1/15/14 6:26 AM

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

Re: [Haskell-cafe] Restrict values in type Jake McArthur 1/15/14 6:29 AM

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)

Re: [Haskell-cafe] Restrict values in type Luke Clifton 1/15/14 6:07 PM
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.




Re: [Haskell-cafe] Restrict values in type Luke Clifton 1/15/14 6:36 PM
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 <0sl...@gmail.com> wrote:

Re: [Haskell-cafe] Restrict values in type ol...@okmij.org 1/15/14 8:19 PM

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"]
-}
Re: [Haskell-cafe] Restrict values in type Luke Clifton 1/16/14 6:16 AM
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). 


Re: [Haskell-cafe] Restrict values in type Daniil Frumin 1/16/14 6:31 AM
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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskel...@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Sincerely yours,
-- Daniil
Re: [Haskell-cafe] Restrict values in type Luke Clifton 1/16/14 6:55 AM

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... 

Re: [Haskell-cafe] Restrict values in type ol...@okmij.org 1/16/14 7:30 PM

> 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
Re: [Haskell-cafe] Restrict values in type Luke Clifton 1/16/14 8:06 PM
First, it seems that the dictionary passing implementation of type
classes makes things clearer. This implementation realizes,
informally, double arrow as a simple arrow.

Thank you. This explanation really helped me and was precisely what I was missing. I find an understanding of how things are implemented is often required before I feel comfortable with something (and my search for an explanation like the one you gave provided no results).

Regards,

Luke
Re: [Haskell-cafe] Restrict values in type Simon Yarde 1/17/14 2:39 AM
If it's not been mentioned, this tutorial regarding Type Families and the kinds of restrictions you mention might provide a few pointers:

https://www.fpcomplete.com/school/to-infinity-and-beyond/pick-of-the-week/type-families-and-pokemon

In general, I've found key concepts to hold in mind are 'exclusion of bad programs' mentioned in the paper Fun With Types:

http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf

I'm sorry if any of this has been mentioned previous.

I asked a related question yesterday about the relative merits of creating type restrictions using using newtypes (unions), which I agree seem unwieldy, and using multi-parameter-type-classes (and/or type families) to enable exclusion-of-bad-programms via instances.  I'd be interested to follow along and see what you discover.


Simon Yarde
Re: [Haskell-cafe] Restrict values in type Joseph Barratt 1/19/14 1:43 PM
Just for my own curiosity, I decided to see how much was possible without resorting to extensions. Not that extensions are bad.

https://gist.github.com/josuf107/8511290

I added datatype wrappers for the restricted strokes without exporting their constructors. Certain wrapped types are allowed by exporting functions to call the private constructors with only the allowed types. To make the task of unwrapping easier for the library user all pen wrappers are instances of penable, so the underlying pen type is easy to extract. Pen is also an instance of Penable, for those strokes which allow any Pen.
Re: [Haskell-cafe] Restrict values in type Joseph Barratt 1/19/14 2:24 PM
Just to be clear, this restricts creation of invalid Strokes, but doesn't help much with pattern matching only valid Strokes. To pattern match on Pen for a Stroke you'd do something like

f (Line _ _ pn) = case pen pn of
    (Circle r) -> undefined
    (Rectangle w h) -> undefined

but this will give you a non-exhaustive warning, even though Line can only have Circle and Rectangle pens.
More topics »