Personal tools

Extensible datatypes

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (The problem)
m (fmt)
Line 5: Line 5:
:Define a type <tt>A</tt> such that for any type <tt>B</tt> you can define
:Define a type <tt>A</tt> such that for any type <tt>B</tt> you can define
-
up :: B -> A
+
<haskell>
-
down :: A -> Maybe B
+
up :: B -> A
 +
down :: A -> Maybe B
 +
</haskell>
:such that
:such that
-
down . up = Just
+
<haskell>
 +
down . up = Just
 +
</haskell>
You can do this quite easily in Java or C++, ''mutatis mutandis''. You can't do this in Haskell (or [[O'Haskell]] either).
You can do this quite easily in Java or C++, ''mutatis mutandis''. You can't do this in Haskell (or [[O'Haskell]] either).
Line 18: Line 22:
An alternative approach would be to identify your <tt>B</tt> within <tt>A</tt> not per-<tt>B</tt> but per-(up,down). This would allow for instance separate (up,down) for the same <tt>B</tt> such that
An alternative approach would be to identify your <tt>B</tt> within <tt>A</tt> not per-<tt>B</tt> but per-(up,down). This would allow for instance separate (up,down) for the same <tt>B</tt> such that
-
down1 . up2 = Nothing
+
<haskell>
-
down2 . up1 = Nothing
+
down1 . up2 = Nothing
 +
down2 . up1 = Nothing
 +
</haskell>
Of course this can be done with <tt>Dynamic</tt> too, by defining dummy types. But it's ugly.
Of course this can be done with <tt>Dynamic</tt> too, by defining dummy types. But it's ugly.
Line 27: Line 33:
'''Extensible datatypes''' allow a type to be defined as "open", which can later be extended by disjoint union. Here's a sample syntax that achieves the above OO test:
'''Extensible datatypes''' allow a type to be defined as "open", which can later be extended by disjoint union. Here's a sample syntax that achieves the above OO test:
-
module P where
+
<haskell>
-
data A = ..
+
module P where
 +
data A = ..
-
module Q where
+
module Q where
-
import P
+
import P
-
A |= MkB B
+
A |= MkB B
-
up = MkB
+
up = MkB
-
down (MkB b) = Just b
+
down (MkB b) = Just b
-
down _ = Nothing
+
down _ = Nothing
 +
</haskell>
== Deriving Dynamic ==
== Deriving Dynamic ==
Line 43: Line 51:
It's possible to define [[Dynamic]] using extensible datatypes. Here's a naive attempt:
It's possible to define [[Dynamic]] using extensible datatypes. Here's a naive attempt:
-
data Dynamic = ..
+
<haskell>
 +
data Dynamic = ..
-
class Typeable' a where
+
class Typeable' a where
-
toDyn :: a -> Dynamic
+
toDyn :: a -> Dynamic
-
fromDynamic :: Dynamic -> Maybe a
+
fromDynamic :: Dynamic -> Maybe a
-
-- for each type...
+
-- for each type...
-
Dynamic |= MkBool Bool
+
Dynamic |= MkBool Bool
 +
 
 +
instance Typeable' Bool where
 +
toDyn = MkBool
 +
fromDynamic (MkBool b) = Just b
 +
fromDynamic _ = Nothing
 +
</haskell>
-
instance Typeable' Bool where
 
-
toDyn = MkBool
 
-
fromDynamic (MkBool b) = Just b
 
-
fromDynamic _ = Nothing
 
This attempt however doesn't allow easy creation of <tt>Typeable1</tt>, <tt>Typeable2</tt> etc. A better way is to use type-constructor parameters:
This attempt however doesn't allow easy creation of <tt>Typeable1</tt>, <tt>Typeable2</tt> etc. A better way is to use type-constructor parameters:
-
data Dynamic0 (f :: * -> *) = ..
+
<haskell>
 +
data Dynamic0 (f :: * -> *) = ..
-
data Dynamic1 (g :: (* -> *) -> *) = ..
+
data Dynamic1 (g :: (* -> *) -> *) = ..
-
type Dynamic = Dynamic0 Identity
+
type Dynamic = Dynamic0 Identity
-
data Type a = MkType
+
data Type a = MkType
-
type TypeRep = Dynamic0 Type
+
type TypeRep = Dynamic0 Type
-
class Typeable0 a where
+
class Typeable0 a where
-
toDyn0 :: f a -> Dynamic0 f
+
toDyn0 :: f a -> Dynamic0 f
-
fromDynamic0 :: Dynamic0 f -> Maybe (f a)
+
fromDynamic0 :: Dynamic0 f -> Maybe (f a)
-
class Typeable1 p where
+
class Typeable1 p where
-
toDyn1 :: g p -> Dynamic1 g
+
toDyn1 :: g p -> Dynamic1 g
-
fromDynamic1 :: Dynamic1 g -> Maybe (g p)
+
fromDynamic1 :: Dynamic1 g -> Maybe (g p)
-
data Compose p q a = MkCompose (p (q a))
+
data Compose p q a = MkCompose (p (q a))
-
data Compose1 d0 f p = MkCompose1 (d0 (Compose f p))
+
data Compose1 d0 f p = MkCompose1 (d0 (Compose f p))
-
Dynamic0 f |= MkDynamic1 (Dynamic1 (Compose1 Dynamic0 f))
+
Dynamic0 f |= MkDynamic1 (Dynamic1 (Compose1 Dynamic0 f))
-
unDynamic1 :: Dynamic0 f -> Maybe (Dynamic1 (Compose1 Dynamic0 f))
+
unDynamic1 :: Dynamic0 f -> Maybe (Dynamic1 (Compose1 Dynamic0 f))
-
unDynamic1 (MkDynamic1 xx) = Just xx
+
unDynamic1 (MkDynamic1 xx) = Just xx
-
unDynamic1 _ = Nothing
+
unDynamic1 _ = Nothing
-
instance (Typeable1 p,Typeable0 a) => Typeable0 (p a)
+
instance (Typeable1 p,Typeable0 a) => Typeable0 (p a)
-
-- toDyn0 :: f (p a) -> Dynamic0 f
+
-- toDyn0 :: f (p a) -> Dynamic0 f
-
toDyn0 = MkDynamic1 . toDyn1 . MkCompose1 . toDyn0 . MkCompose
+
toDyn0 = MkDynamic1 . toDyn1 . MkCompose1 . toDyn0 . MkCompose
-
-- fromDynamic0 :: Dynamic0 f -> Maybe (f (p a))
+
-- fromDynamic0 :: Dynamic0 f -> Maybe (f (p a))
-
fromDynamic0 dyn = do
+
fromDynamic0 dyn = do
-
dcdf <- unDynamic1 dyn
+
dcdf <- unDynamic1 dyn
-
(MkCompose1 dcfp) <- fromDynamic1 dcdf
+
(MkCompose1 dcfp) <- fromDynamic1 dcdf
-
(MkCompose fpa) <- fromDynamic0 dcfp
+
(MkCompose fpa) <- fromDynamic0 dcfp
-
return fpa
+
return fpa
-
-- for each type
+
-- for each type
-
Dynamic0 f |= MkInt (f Int)
+
Dynamic0 f |= MkInt (f Int)
-
instance Typeable0 Int where
+
instance Typeable0 Int where
-
toDyn0 = MkInt
+
toDyn0 = MkInt
-
fromDynamic0 (MkInt fi) = Just fi
+
fromDynamic0 (MkInt fi) = Just fi
-
fromDynamic0 _ = Nothing
+
fromDynamic0 _ = Nothing
-
Dynamic1 g |= MkMaybe (g Maybe)
+
Dynamic1 g |= MkMaybe (g Maybe)
-
instance Typeable1 Maybe where
+
instance Typeable1 Maybe where
-
toDyn1 = MkMaybe
+
toDyn1 = MkMaybe
-
fromDynamic1 (MkMaybe gm) = Just gm
+
fromDynamic1 (MkMaybe gm) = Just gm
-
fromDynamic1 _ = Nothing
+
fromDynamic1 _ = Nothing
 +
</haskell>
I submit that this is "hairy" rather than "ugly", but I suspect the Type-Constructors Of Unusual Kind (TCOUKs) get even hairier for <tt>Typeable2</tt>, <tt>Typeable3</tt> etc...
I submit that this is "hairy" rather than "ugly", but I suspect the Type-Constructors Of Unusual Kind (TCOUKs) get even hairier for <tt>Typeable2</tt>, <tt>Typeable3</tt> etc...
[[Category:Proposals]]
[[Category:Proposals]]

Revision as of 23:05, 2 April 2006

1 The problem

Here's a simple test for object orientation (for some reasonable definition):

Define a type A such that for any type B you can define
up :: B -> A
down :: A -> Maybe B
such that
down . up = Just

You can do this quite easily in Java or C++, mutatis mutandis. You can't do this in Haskell (or O'Haskell either).

You can do a weaker form of this with Haskell's Dynamic, where you only have to deal with Bs that are instances of Typeable. But even with that, note that Dynamic/Typeable/TypeRep are a bit messy, with instances for Typeable defined for a wide range of known types.

An alternative approach would be to identify your B within A not per-B but per-(up,down). This would allow for instance separate (up,down) for the same B such that

down1 . up2 = Nothing
down2 . up1 = Nothing

Of course this can be done with Dynamic too, by defining dummy types. But it's ugly.

2 Extensible datatypes

Extensible datatypes allow a type to be defined as "open", which can later be extended by disjoint union. Here's a sample syntax that achieves the above OO test:

module P where
data A = ..
 
module Q where
import P
 
A |= MkB B
 
up = MkB
down (MkB b) = Just b
down _ = Nothing

3 Deriving Dynamic

It's possible to define Dynamic using extensible datatypes. Here's a naive attempt:

data Dynamic = ..
 
class Typeable' a where
  toDyn :: a -> Dynamic
  fromDynamic :: Dynamic -> Maybe a
 
-- for each type...
 
Dynamic |= MkBool Bool
 
instance Typeable' Bool where
  toDyn = MkBool
  fromDynamic (MkBool b) = Just b
  fromDynamic _ = Nothing


This attempt however doesn't allow easy creation of Typeable1, Typeable2 etc. A better way is to use type-constructor parameters:

data Dynamic0 (f :: * -> *) = ..
 
data Dynamic1 (g :: (* -> *) -> *) = ..
 
type Dynamic = Dynamic0 Identity
 
data Type a = MkType
 
type TypeRep = Dynamic0 Type
 
class Typeable0 a where
  toDyn0 :: f a -> Dynamic0 f
  fromDynamic0 :: Dynamic0 f -> Maybe (f a)
 
class Typeable1 p where
  toDyn1 :: g p -> Dynamic1 g
  fromDynamic1 :: Dynamic1 g -> Maybe (g p)
 
data Compose p q a = MkCompose (p (q a))
data Compose1 d0 f p = MkCompose1 (d0 (Compose f p))
 
Dynamic0 f |= MkDynamic1 (Dynamic1 (Compose1 Dynamic0 f))
 
unDynamic1 :: Dynamic0 f -> Maybe (Dynamic1 (Compose1 Dynamic0 f))
unDynamic1 (MkDynamic1 xx) = Just xx
unDynamic1 _ = Nothing
 
instance (Typeable1 p,Typeable0 a) => Typeable0 (p a)
  -- toDyn0 :: f (p a) -> Dynamic0 f
  toDyn0 = MkDynamic1 . toDyn1 . MkCompose1 . toDyn0 . MkCompose
  -- fromDynamic0 :: Dynamic0 f -> Maybe (f (p a))
  fromDynamic0 dyn = do
    dcdf <- unDynamic1 dyn
    (MkCompose1 dcfp) <- fromDynamic1 dcdf
    (MkCompose fpa) <- fromDynamic0 dcfp
    return fpa
 
-- for each type
 
Dynamic0 f |= MkInt (f Int)
 
instance Typeable0 Int where
   toDyn0 = MkInt
   fromDynamic0 (MkInt fi) = Just fi
   fromDynamic0 _ = Nothing
 
Dynamic1 g |= MkMaybe (g Maybe)
 
instance Typeable1 Maybe where
   toDyn1 = MkMaybe
   fromDynamic1 (MkMaybe gm) = Just gm
   fromDynamic1 _ = Nothing

I submit that this is "hairy" rather than "ugly", but I suspect the Type-Constructors Of Unusual Kind (TCOUKs) get even hairier for Typeable2, Typeable3 etc...