Re: [Haskell-cafe] Restrict values in type

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"] -}

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

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
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Sincerely yours, -- Daniil

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

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

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
participants (3)
-
Daniil Frumin
-
Luke Clifton
-
oleg@okmij.org