Difference between revisions of "Extensible datatypes"
m (→The problem: wikify) |
m (Fix link to reference) |
||
(13 intermediate revisions by 2 users 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 |
||
+ | <haskell> |
||
− | up :: B -> A |
||
− | + | up :: B -> A |
|
+ | down :: A -> Maybe B |
||
+ | </haskell> |
||
:such that |
:such that |
||
+ | <haskell> |
||
− | down . up = Just |
||
+ | down . up = Just |
||
+ | </haskell> |
||
− | You can do this quite easily in Java or C++, mutatis mutandis. You can't do this in 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 a weaker form of this with Haskell's <tt>[[Dynamic]]</tt>, where you only have to deal with |
+ | You can do a weaker form of this with Haskell's <tt>[[Dynamic]]</tt>, where you only have to deal with <tt>B</tt>s that are instances of <tt>Typeable</tt>. But even with that, note that <tt>Dynamic</tt>/<tt>Typeable</tt>/<tt>TypeRep</tt> are a bit messy, with instances for <tt>Typeable</tt> defined for a wide range of known types. |
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 |
||
+ | <haskell> |
||
− | down1 . up2 = 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 31: | ||
== Extensible datatypes == |
== 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: |
|
+ | <haskell> |
||
− | module P where |
||
+ | module P where |
||
− | data A = .. |
||
+ | -- define open datatype |
||
− | module Q where |
||
+ | open data A :: * |
||
− | import P |
||
+ | module Q where |
||
− | A |= MkB B |
||
+ | import P |
||
+ | -- add constructor to A |
||
− | up = MkB |
||
− | + | MkB :: B -> A |
|
+ | |||
− | down _ = Nothing |
||
+ | up = MkB |
||
+ | down (MkB b) = Just b |
||
+ | down _ = Nothing |
||
+ | </haskell> |
||
== Deriving Dynamic == |
== Deriving Dynamic == |
||
Line 43: | Line 54: | ||
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: |
||
+ | <haskell> |
||
− | data Dynamic = .. |
||
+ | 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 |
||
+ | </haskell> |
||
+ | |||
+ | |||
+ | 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: |
||
+ | <haskell> |
||
− | class Typeable' a where |
||
− | + | open data Dynamic0 :: (* -> *) -> * |
|
− | fromDynamic :: Dynamic -> Maybe a |
||
+ | open data Dynamic1 :: ((* -> *) -> *) -> * |
||
− | -- for each type... |
||
− | + | type Dynamic = Dynamic0 Identity |
|
+ | data Type a = MkType |
||
− | instance Typeable' Bool where |
||
− | toDyn = MkBool |
||
− | fromDynamic (MkBool b) = Just b |
||
− | fromDynamic _ = Nothing |
||
+ | type TypeRep = Dynamic0 Type |
||
− | This attempt however doesn't allow easy creation of Typeable1, Typeable2 etc. A better way is to use type-constructor parameters: |
||
+ | class Typeable0 a where |
||
− | data Dynamic0 (f :: * -> *) = .. |
||
+ | toDyn0 :: f a -> Dynamic0 f |
||
+ | fromDynamic0 :: Dynamic0 f -> Maybe (f a) |
||
+ | class Typeable1 p where |
||
− | data Dynamic1 (g :: (* -> *) -> *) = .. |
||
+ | toDyn1 :: g p -> Dynamic1 g |
||
+ | fromDynamic1 :: Dynamic1 g -> Maybe (g p) |
||
+ | data Compose p q a = MkCompose (p (q a)) |
||
− | type Dynamic = Dynamic0 Identity |
||
+ | data Compose1 d0 f p = MkCompose1 (d0 (Compose f p)) |
||
+ | MkDynamic1 :: (Dynamic1 (Compose1 Dynamic0 f)) -> Dynamic0 f |
||
− | data Type a = MkType |
||
− | + | 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 a) |
||
+ | -- 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 |
||
− | class Typeable1 p where |
||
− | toDyn1 :: g p -> Dynamic1 g |
||
− | fromDynamic1 :: Dynamic1 g -> Maybe (g p) |
||
+ | MkInt :: (f Int) -> Dynamic0 f |
||
− | data Compose p q a = MkCompose (p (q a)) |
||
− | data Compose1 d0 f p = MkCompose1 (d0 (Compose f p)) |
||
+ | instance Typeable0 Int where |
||
− | Dynamic0 f |= MkDynamic1 (Dynamic1 (Compose1 Dynamic0 f)) |
||
+ | toDyn0 = MkInt |
||
+ | fromDynamic0 (MkInt fi) = Just fi |
||
+ | fromDynamic0 _ = Nothing |
||
− | + | MkMaybe :: (g Maybe) -> Dynamic1 g |
|
− | unDynamic1 (MkDynamic1 xx) = Just xx |
||
− | unDynamic1 _ = Nothing |
||
− | + | instance Typeable1 Maybe where |
|
+ | toDyn1 = MkMaybe |
||
− | -- toDyn0 :: f (p a) -> Dynamic0 f |
||
+ | fromDynamic1 (MkMaybe gm) = Just gm |
||
− | toDyn0 = MkDynamic1 . toDyn1 . MkCompose1 . toDyn0 . MkCompose |
||
+ | fromDynamic1 _ = Nothing |
||
− | -- fromDynamic0 :: Dynamic0 f -> Maybe (f (p a)) |
||
+ | </haskell> |
||
− | fromDynamic0 dyn = do |
||
− | dcdf <- unDynamic1 dyn |
||
− | (MkCompose1 dcfp) <- fromDynamic1 dcdf |
||
− | (MkCompose fpa) <- fromDynamic0 dcfp |
||
− | return fpa |
||
+ | 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... |
||
− | -- for each type |
||
+ | == Open functions == |
||
− | Dynamic0 f |= MkInt (f Int) |
||
+ | {{stub}} |
||
− | instance Typeable0 Int where |
||
− | toDyn0 = MkInt |
||
− | fromDynamic0 (MkInt fi) = Just fi |
||
− | fromDynamic0 _ = Nothing |
||
+ | == References == |
||
− | Dynamic1 g |= MkMaybe (g Maybe) |
||
+ | * Andres Löh and Ralf Hinze. [https://www.andres-loeh.de/OpenDatatypes.pdf Open Data Types and Open Functions] |
||
− | instance Typeable1 Maybe where |
||
− | toDyn1 = MkMaybe |
||
− | fromDynamic1 (MkMaybe gm) = Just gm |
||
− | fromDynamic1 _ = Nothing |
||
+ | [[Category:Proposals]] |
||
− | 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... |
Latest revision as of 11:16, 28 March 2018
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.
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
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...
Open functions
This article is a stub. You can help by expanding it.
References
- Andres Löh and Ralf Hinze. Open Data Types and Open Functions