A Question of Restriction
Hello all. I would like to define a data type that is the super-set of several types and then each of the proper subset types. For example: data Foo = One | Two | Three | Four data Odd = One | Three data Even = Two | Four This, of course, does not work. It seems that such a thing should possible to express entirely in the type system, but I cannot think of how. Would someone be so kind as to explain how this sort of thing can be accomplished? Thanks, Brian
I've seen this expressed with GADTs (which I guess many things can), though I'm not sure if it's the best way, and I'm no type system wizard. If I recall correctly, this use is normally called phantom types. {-# LANGUAGE EmptyDataDecls, GADTs #-} data Even data Odd data Foo a where One :: Foo Odd Two :: Foo Even Three :: Foo Odd Four :: Foo Even Then you can write functions that accept only evens: f :: Foo Even -> ... or only odds: f :: Foo Odd -> ... or either: f :: Foo a -> ... Hope that helps, -Ross On Jul 27, 2009, at 12:01 AM, Brian Troutwine wrote:
Hello all.
I would like to define a data type that is the super-set of several types and then each of the proper subset types. For example:
data Foo = One | Two | Three | Four data Odd = One | Three data Even = Two | Four
This, of course, does not work. It seems that such a thing should possible to express entirely in the type system, but I cannot think of how. Would someone be so kind as to explain how this sort of thing can be accomplished?
Thanks, Brian _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Sun, Jul 26, 2009 at 09:01:22PM -0700, Brian Troutwine wrote:
Hello all.
I would like to define a data type that is the super-set of several types and then each of the proper subset types. For example:
data Foo = O !Odd | E !Even
data Odd = One | Three data Even = Two | Four
This, of course, does not work. It seems that such a thing should possible to express entirely in the type system, but I cannot think of how. Would someone be so kind as to explain how this sort of thing can be accomplished?
Do you have any reason not to do the above? -- Felipe.
Do you have any reason not to do the above?
Yes, the subset types that I wish to define are not clean partitions,
though my example does suggest this. Let's say that the definition of
Foo is now
data Foo = One | Two | Three | Four | Five | Six
while Odd and Even remain the same. I would further like to define
Triangular, which I will do incorrectly for consistency.
data Triangular = One | Three | Six
I could not accommodate this definition using your scheme, correct?
Thanks,
Brian
On Sun, Jul 26, 2009 at 9:14 PM, Felipe Lessa
On Sun, Jul 26, 2009 at 09:01:22PM -0700, Brian Troutwine wrote:
Hello all.
I would like to define a data type that is the super-set of several types and then each of the proper subset types. For example:
data Foo = O !Odd | E !Even
data Odd = One | Three data Even = Two | Four
This, of course, does not work. It seems that such a thing should possible to express entirely in the type system, but I cannot think of how. Would someone be so kind as to explain how this sort of thing can be accomplished?
Do you have any reason not to do the above?
-- Felipe. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Brian Troutwine wrote:
Do you have any reason not to do the above?
Yes, the subset types that I wish to define are not clean partitions, though my example does suggest this. Let's say that the definition of Foo is now
data Foo = One | Two | Three | Four | Five | Six
while Odd and Even remain the same. I would further like to define Triangular, which I will do incorrectly for consistency.
data Triangular = One | Three | Six
I could not accommodate this definition using your scheme, correct?
A variation on scheme proposed by Ross Mellgren earlier in this thread. It's a bit tedious but allows for definition of arbitrary subsets thus it may work for you: {-# LANGUAGE GADTs, EmptyDataDecls #-} data One data Two data Three data Four data Foo a where FOne :: Foo One FTwo :: Foo Two FThree :: Foo Three FFour :: Foo Four class IsEven a instance IsEven Two instance IsEven Four class IsOdd a instance IsOdd One instance IsOdd Three class IsLessThanThree a instance IsLessThanThree One instance IsLessThanThree Two quux :: IsEven a => Foo a -> String quux FTwo = "2" quux FFour = "4" bzzt :: IsLessThanThree a => Foo a -> String bzzt FOne = "1" bzzt FTwo = "2"
Brian Troutwine wrote:
Hello all.
I would like to define a data type that is the super-set of several types and then each of the proper subset types. For example:
data Foo = One | Two | Three | Four data Odd = One | Three data Even = Two | Four
This, of course, does not work. It seems that such a thing should possible to express entirely in the type system, but I cannot think of how. Would someone be so kind as to explain how this sort of thing can be accomplished?
You might want to look at Johan Nordlander's O'Haskell. It's a dialect of Haskell with such subtyping, designed and implemented while ago. Recently there was a proposal (but not an implementation yet) of subtyping data types in general with recursion and including GADTs http://portal.acm.org/citation.cfm?id=1411286.1411297 (I want to work on this again some time later again). But neither of these work is not implemented as an extension feature in major Haskell implementations like GHC or Hugs. I want to push this work further some time later on. FYI, there exist a functional language which you can express this kind of idea though. For example, in OCaml, you can use polymorphic variants.
Hi Brian, If I understand you correctly, you've run into the "Expression Problem". Phil Wadler posed the problem in a widely-cited e-mail, formulating it much more clearly than I ever could: http://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt There are lots of ways to tackle this problem in Haskell - just google "Expression Problem Haskell". My (completely biased) personal favourite is: http://www.cse.chalmers.se/~wouter/Publications/DataTypesALaCarte.pdf Hope this helps, Wouter
Hello Wouter.
I've had a go at the paper linked and perused other references found
with Google. Unfortunately, such sophisticated use of the type system
is pretty far out of my normal problem domain and I can't see how to
apply the techniques presented to my motivating example. Would you be
so kind as to elaborate?
Thank you,
Brian
On Mon, Jul 27, 2009 at 2:37 AM, Wouter Swierstra
Hi Brian,
If I understand you correctly, you've run into the "Expression Problem". Phil Wadler posed the problem in a widely-cited e-mail, formulating it much more clearly than I ever could:
http://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt
There are lots of ways to tackle this problem in Haskell - just google "Expression Problem Haskell". My (completely biased) personal favourite is:
http://www.cse.chalmers.se/~wouter/Publications/DataTypesALaCarte.pdf
Hope this helps,
Wouter
Would you be so kind as to elaborate?
Sure. I'll just sketch how to deal the example in your e-mail. If you want to use recursive data types (like Lists or Trees), you'll need to use the Expr data type from the paper. Instead of defining:
data Foo = One | Two | Three | Four
Define the following data types:
data One = One data Two = Two data Three = Three data Four = Four
You can define the following data type to assemble the pieces:
infixr 6 :+: data (a :+: b) = Inl a | Inr b
So, for example you could define:
type Odd = One :+: Three type Even = Two :+: Four type Foo = One :+: Two :+: Three :+: Four
To define functions modularly, it's a good idea to use Haskell's clasess to do some of the boring work for you. Here's another example:
class ToNumber a where toNumber :: a -> Int
instance ToNumber One where toNumber One = 1
(and similar instances for Two, Three, and Four) The key instance, however, is the following:
instance (ToNumber a, ToNumber b) => ToNumber (a :+: b) where toNumber (Inl a) = toNumber a toNumber (Inr b) = toNumber b
This instance explains how to build instances for Odd, Even, and Foo from the instances for One, Two, Three, and Four. An example ghci sessions might look like: *Main> let x = Inl One :: Odd *Main> toNumber x 1 *Main> let y = Inr (Inr (Inl Three) :: Foo *Main> toNumber y 3 Of course, writing all these injections (Inr (Inr (Inl ...))) gets dull quite quickly. The (<) class in the paper explains how to avoid this. I hope this gives you a better idea of how you might go about solving your problem. All the best, Wouter
Brian Troutwine wrote:
Hello Wouter.
I've had a go at the paper linked and perused other references found with Google. Unfortunately, such sophisticated use of the type system is pretty far out of my normal problem domain and I can't see how to apply the techniques presented to my motivating example. Would you be so kind as to elaborate?
data Foo = One | Two | Three | Four data Odd = One | Three data Even = Two | Four ==> {- data Fix f = Fix { unFix :: f (Fix f) } data (:+:) f g x = Inl (f x) | Inr (g x) ... -} data One r = One data Two r = Two data Three r = Three data Four r = Four instance Functor One where fmap _ One = One instance Functor Two where fmap _ Two = Two instance Functor Three where fmap _ Three = Three instance Functor Four where fmap _ Four = Four type Foo = Fix (One :+: Two :+: Three :+: Four) type Odd = Fix (One :+: Three) type Even = Fix (Two :+: Four) If your original types were actually recursive, then the unfixed functors should use their r parameter in place of the recursive call, e.g. data List a = Nil | Cons a (List a) ==> data List a r = Nil | Cons a r Also, if you know a certain collection of component types must always occur together, then you can flatten parts of the coproduct and use normal unions as well. E.g. data Odd r = One | Three data Two r = Two data Four r = Four type Foo = Fix (Odd :+: Two :+: Four) -- Live well, ~wren
participants (8)
-
Ahn, Ki Yung -
Brian Troutwine -
Felipe Lessa -
Gleb Alexeyev -
Ross Mellgren -
Wouter Swierstra -
Wouter Swierstra
-
wren ng thornton