# Extensible datatypes

### From HaskellWiki

m (→The problem) |
TomLokhorst (Talk | contribs) (Fixed link) |
||

(5 intermediate revisions by one user not shown) | |||

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 18: | ||

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 25: | Line 25: | ||

== Extensible datatypes == |
== 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: |
+ | '''Extensible datatypes''' allow a type to be defined as "open", which can later be extended by disjoint union. Here's the Löh-Hinze syntax that achieves the above OO test: |

− | module P where |
+ | <haskell> |

− | data A = .. |
+ | module P where |

− | module Q where |
+ | -- define open datatype |

− | import P |
+ | open data A :: * |

− | A |= MkB B |
+ | module Q where |

+ | import P |
||

− | up = MkB |
+ | -- add constructor to A |

− | down (MkB b) = Just b |
+ | MkB :: B -> A |

− | down _ = Nothing |
+ | |

+ | up = MkB |
||

+ | down (MkB b) = Just b |
||

+ | down _ = Nothing |
||

+ | </haskell> |
||

== Deriving Dynamic == |
== Deriving Dynamic == |
||

Line 43: | Line 43: | ||

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

+ | open 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 |
+ | MkBool :: Bool -> Dynamic |

+ | |||

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

+ | open data Dynamic0 :: (* -> *) -> * |
||

− | data Dynamic1 (g :: (* -> *) -> *) = .. |
+ | open data Dynamic1 :: ((* -> *) -> *) -> * |

− | 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)) |
+ | MkDynamic1 :: (Dynamic1 (Compose1 Dynamic0 f)) -> 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) |
+ | MkInt :: (f Int) -> Dynamic0 f |

− | 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) |
+ | MkMaybe :: (g Maybe) -> Dynamic1 g |

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

+ | |||

+ | == Open functions == |
||

+ | |||

+ | {{stub}} |
||

+ | |||

+ | == References == |
||

+ | |||

+ | * Andres Löh and Ralf Hinze. [http://people.cs.uu.nl/andres/OpenDatatypes.pdf Open Data Types and Open Functions] |
||

[[Category:Proposals]] |
[[Category:Proposals]] |

## Latest revision as of 07:43, 16 May 2009

## Contents |

## [edit] 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 `B`s 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.

## [edit] 2 Extensible datatypes

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

module P where -- define open datatype open data A :: * module Q where import P -- add constructor to A MkB :: B -> A up = MkB down (MkB b) = Just b down _ = Nothing

## [edit] 3 Deriving Dynamic

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

open Dynamic :: * class Typeable' a where toDyn :: a -> Dynamic fromDynamic :: Dynamic -> Maybe a -- for each type... MkBool :: Bool -> Dynamic 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:

open data Dynamic0 :: (* -> *) -> * open data Dynamic1 :: ((* -> *) -> *) -> * 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)) MkDynamic1 :: (Dynamic1 (Compose1 Dynamic0 f)) -> 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 MkInt :: (f Int) -> Dynamic0 f instance Typeable0 Int where toDyn0 = MkInt fromDynamic0 (MkInt fi) = Just fi fromDynamic0 _ = Nothing MkMaybe :: (g Maybe) -> Dynamic1 g 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...

## [edit] 4 Open functions

*This article is a stub. You can help by expanding it.*

## [edit] 5 References

- Andres Löh and Ralf Hinze. Open Data Types and Open Functions