[Haskellcafe] 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.
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: [Haskellcafe] 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 _______________________________________________ 
Re: [Haskellcafe] 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. _______________________________________________ 
Re: [Haskellcafe] 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: [Haskellcafe] Restrict values in type  Luke Clifton  1/12/14 8:12 PM  Hi Bob,
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: [Haskellcafe] 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 nonexhaustive 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 > _______________________________________________ Sincerely yours,  Daniil 
Re: [Haskellcafe] Restrict values in type  Andras Slemmer  1/15/14 5:55 AM 
You are on the right track. With DataKinds and GADTs you can create an index type for PenShape: 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 [ddata 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: [Haskellcafe] 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: [Haskellcafe] 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 handrolled typelevel bool? Nicolas 
Re: [Haskellcafe] 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)  
Re: [Haskellcafe] 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 class Rectangle a where class (Circle a, Rectangle a) => PenShape a where data Stroke = forall p. (Circle p, Rectangle p) => Line Point Point p  Jake _______________________________________________ 
Re: [Haskellcafe] Restrict values in type  Jake McArthur  1/15/14 6:26 AM  Sorry, I used existential types but should have used universal types. 
Re: [Haskellcafe] 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) 
Re: [Haskellcafe] 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: [Haskellcafe] Restrict values in type  Luke Clifton  1/15/14 6:36 PM  Thanks Andras and Daniil for pointing out the singletons package. 
Re: [Haskellcafe] Restrict values in type  ol...@okmij.org  1/15/14 8:19 PM  The problem you have posed calls for socalled 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 extensibleeffects package. Using singletons is yet another, quite heavyweight solution. I'd like to stress a much simpler solution, which requires no type equality or GADTs or bleeding edge. It is a taglessfinal 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 I will define it as an expression in a very simple domainspecific 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 patternmatch on pen shapes. The answer is that in tagglessfinal style, you don't patternmatch. You interpret. Quite often the code becomes clearer. Enclosed is the complete code. For (far) more explanation of taglessfinal, please see the first part of http://okmij.org/ftp/taglessfinal/course/lecture.pdf {# LANGUAGE RankNTypes #} module Im where  As a data structure { data PenShape = Circle Float}  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: finitedim 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} 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: [Haskellcafe] 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.
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: [Haskellcafe] 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 > _______________________________________________  
Re: [Haskellcafe] Restrict values in type  Luke Clifton  1/16/14 6:55 AM 
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: [Haskellcafe] Restrict values in type  ol...@okmij.org  1/16/14 7:30 PM 
> To me this reads that repr should be both a CirclePen and a RectPen inThis 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 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, becomes > (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 picalculus.) 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: [Haskellcafe] Restrict values in type  Luke Clifton  1/16/14 8:06 PM 
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: [Haskellcafe] 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/toinfinityandbeyond/pickoftheweek/typefamiliesandpokemon 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/enus/um/people/simonpj/papers/assoctypes/funwithtypefuns/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 multiparametertypeclasses (and/or type families) to enable exclusionofbadprogramms via instances. I'd be interested to follow along and see what you discover. Simon Yarde 
Re: [Haskellcafe] 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: [Haskellcafe] 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 nonexhaustive warning, even though Line can only have Circle and Rectangle pens. 