Existential type
From HaskellWiki
m (category) |
(Add other simple examples with more notes, alternate ways.) |
||
| Line 1: | Line 1: | ||
__TOC__ | __TOC__ | ||
| + | This is a extension of Haskell available in [[GHC]]. See the GHC documentation: | ||
| + | http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html | ||
| - | == Dynamic dispatch mechanism of OOP == | + | ==Introduction to existential types== |
| + | |||
| + | ===A short example=== | ||
| + | |||
| + | This illustrates creating a heterogeneous list, all of whose members implement "Show", and progressing through that list to show these items: | ||
| + | |||
| + | <haskell> | ||
| + | data Obj = forall a. (Show a) => Obj a | ||
| + | |||
| + | xs = [Obj 1, Obj "foo", Obj 'c'] | ||
| + | |||
| + | doShow :: [Obj] -> String | ||
| + | doShow [] = "" | ||
| + | doShow ((Obj x):xs) = show x ++ doShow xs | ||
| + | </haskell> | ||
| + | |||
| + | With output: <code>doShow xs ==> "1\"foo\"'c'"</code> | ||
| + | |||
| + | ===Expanded example - rendering objects in a raytracer=== | ||
| + | |||
| + | ====Problem statement==== | ||
| + | |||
| + | In a raytracer, a requirement is to be able to render several different objects (like a ball, mesh or whatever). The first step is a type class for Renderable like so: | ||
| + | |||
| + | <haskell> | ||
| + | class Renderable a where | ||
| + | boundingSphere :: a -> Sphere | ||
| + | hit :: a -> [Fragment] -- returns the "fragments" of all hits with ray | ||
| + | {- ... etc ... -} | ||
| + | </haskell> | ||
| + | |||
| + | To solve the problem, the <hask>hit</hask> function must apply to several objects (like a sphere and a polygon for instance). | ||
| + | |||
| + | <haskell> | ||
| + | hits :: Renderable a => [a] -> [Fragment] | ||
| + | hits xs = sortByDistance $ concatMap hit xs | ||
| + | </haskell> | ||
| + | |||
| + | However, this does not work as written since the elements of the list can be of '''SEVERAL''' different types (like a sphere and a polygon and a mesh etc. etc.) but | ||
| + | lists need to have elements of the same type. | ||
| + | |||
| + | ====The solution==== | ||
| + | |||
| + | Use 'existential types' - an extension to Haskell that can be found in most compilers. | ||
| + | |||
| + | The following example is based on GHC : | ||
| + | |||
| + | <haskell> | ||
| + | {-# OPTIONS -fglasgow-exts #-} | ||
| + | |||
| + | {- ...-} | ||
| + | |||
| + | data AnyRenderable = forall a. Renderable a => AnyRenderable a | ||
| + | |||
| + | instance Renderable AnyRenderable where | ||
| + | boundingSphere (AnyRenderable a) = boundingSphere a | ||
| + | hit (AnyRenderable a) = hit a | ||
| + | {- ... -} | ||
| + | </haskell> | ||
| + | |||
| + | Now, create lists with type <hask>[AnyRenderable]</hask>, for example, | ||
| + | <haskell> | ||
| + | [ AnyRenderable x | ||
| + | , AnyRenderable y | ||
| + | , AnyRenderable z ] | ||
| + | </haskell> | ||
| + | where x, y, z can be from different instances of <hask>Renderable</hask>. | ||
| + | === Dynamic dispatch mechanism of OOP === | ||
'''Existential types''' in conjunction with type classes can be used to emulate the dynamic dispatch mechanism of object oriented programming languages. To illustrate this concept I show how a classic example from object oriented programming can be encoded in Haskell. | '''Existential types''' in conjunction with type classes can be used to emulate the dynamic dispatch mechanism of object oriented programming languages. To illustrate this concept I show how a classic example from object oriented programming can be encoded in Haskell. | ||
| Line 56: | Line 125: | ||
(You may see other [[Smart constructors]] for other purposes). | (You may see other [[Smart constructors]] for other purposes). | ||
| - | == [[Generalised algebraic datatype]] == | + | === [[Generalised algebraic datatype]] === |
The type of the <hask>parse</hask> function for [[Generalised algebraic datatype#Motivating example|this GADT]] is a good example to illustrate the concept of existential type. | The type of the <hask>parse</hask> function for [[Generalised algebraic datatype#Motivating example|this GADT]] is a good example to illustrate the concept of existential type. | ||
| + | |||
| + | ==Alternate methods== | ||
| + | ===Concrete data types=== | ||
| + | ====Universal instance of a Class==== | ||
| + | Here one way to simulate existentials (Hawiki note: (Borrowed from somewhere...)) | ||
| + | |||
| + | |||
| + | Suppose I have a type class Shape a | ||
| + | <haskell> | ||
| + | type Point = (Float,Float) | ||
| + | |||
| + | class Shape a where | ||
| + | draw :: a -> IO () | ||
| + | translate :: a-> Point -> a | ||
| + | |||
| + | </haskell> | ||
| + | |||
| + | Then we can pack shapes up into a [[concrete data type]] like this: | ||
| + | <haskell> | ||
| + | data SHAPE = SHAPE (IO ()) (Point -> SHAPE) | ||
| + | </haskell> | ||
| + | with a function like this | ||
| + | <haskell> | ||
| + | packShape :: Shape a => a -> SHAPE | ||
| + | packShape s = SHAPE (draw s) (\(x,y) -> packShape (translate s (x,y))) | ||
| + | </haskell> | ||
| + | This would be useful if we needed a list of shapes that we would need to translate and draw. | ||
| + | |||
| + | In fact we can make <hask>SHAPE</hask> an instance of <hask>Shape</hask>: | ||
| + | <haskell> | ||
| + | instance Shape SHAPE where | ||
| + | draw (SHAPE d t) = d | ||
| + | translate (SHAPE d t) = t | ||
| + | </haskell> | ||
| + | |||
| + | So SHAPE is a sort of universal instance. | ||
| + | |||
| + | ====Using constructors and combinators==== | ||
| + | Why bother with class <hask>Shape</hask>? Why not just go straight to | ||
| + | |||
| + | <haskell> | ||
| + | data Shape = Shape { | ||
| + | draw :: IO() | ||
| + | translate :: (Int, Int) -> Shape | ||
| + | } | ||
| + | </haskell> | ||
| + | |||
| + | Then you can create a library of shape [[constructor]]s and [[combinator]]s | ||
| + | that each have defined "draw" and "translate" in their "where" clauses. | ||
| + | |||
| + | <haskell> | ||
| + | circle :: (Int, Int) -> Int -> Shape | ||
| + | circle (x,y) r = | ||
| + | Shape draw1 translate1 | ||
| + | where | ||
| + | draw1 = ... | ||
| + | translate1 (x1,y1) = circle (x+x1, y+y1) r | ||
| + | |||
| + | shapeGroup :: [Shape] -> Shape | ||
| + | shapeGroup shapes = Shape draw1 translate1 | ||
| + | where | ||
| + | draw1 = sequence_ $ map draw shapes | ||
| + | translate1 v = shapeGroup $ map (translate v) shapes | ||
| + | </haskell> | ||
| + | |||
| + | ===Cases that really require existentials=== | ||
| + | |||
| + | There are cases where this sort of trick doesnt work. Here are two examples from a haskell mailing list discussion (from K. Claussen) that don't seem expressible without | ||
| + | existentials. (But maybe one can rethink the whole thing :) | ||
| + | <haskell> | ||
| + | data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b) | ||
| + | </haskell> | ||
| + | and | ||
| + | <haskell> | ||
| + | data Action = forall b . Act (IORef b) (b -> IO ()) | ||
| + | </haskell> | ||
| + | (Maybe this last one could be done as a <hask>type Act (IORef b) (IORef b -> IO ())</hask> then we could hide the <hask>IORef</hask> as above, that is go ahead and apply the second argument to the first) | ||
== Examples from the [http://www.cs.uu.nl/wiki/Ehc/ Essential Haskell Compiler] project == | == Examples from the [http://www.cs.uu.nl/wiki/Ehc/ Essential Haskell Compiler] project == | ||
| Line 67: | Line 213: | ||
* [http://www.cs.uu.nl/wiki/Ehc/Examples#EH_4_forall_and_exists_everywher Examples] | * [http://www.cs.uu.nl/wiki/Ehc/Examples#EH_4_forall_and_exists_everywher Examples] | ||
| - | == Trac == | + | ==See also== |
| + | * A mailinglist discussion: http://haskell.org/pipermail/haskell-cafe/2003-October/005231.html | ||
| + | *An example of encoding existentials using RankTwoPolymorphism : http://haskell.org/pipermail/haskell-cafe/2003-October/005304.html | ||
| + | === Trac === | ||
[http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification Existential Quantification] is a detailed material on the topic. It has link also to the smaller [http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantifier Existential Quantifier] page. | [http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification Existential Quantification] is a detailed material on the topic. It has link also to the smaller [http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantifier Existential Quantifier] page. | ||
Revision as of 16:15, 21 December 2006
Contents |
This is a extension of Haskell available in GHC. See the GHC documentation: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html
1 Introduction to existential types
1.1 A short example
This illustrates creating a heterogeneous list, all of whose members implement "Show", and progressing through that list to show these items:
data Obj = forall a. (Show a) => Obj a xs = [Obj 1, Obj "foo", Obj 'c'] doShow :: [Obj] -> String doShow [] = "" doShow ((Obj x):xs) = show x ++ doShow xs
With output: doShow xs ==> "1\"foo\"'c'"
1.2 Expanded example - rendering objects in a raytracer
1.2.1 Problem statement
In a raytracer, a requirement is to be able to render several different objects (like a ball, mesh or whatever). The first step is a type class for Renderable like so:
class Renderable a where boundingSphere :: a -> Sphere hit :: a -> [Fragment] -- returns the "fragments" of all hits with ray {- ... etc ... -}
hits :: Renderable a => [a] -> [Fragment] hits xs = sortByDistance $ concatMap hit xs
However, this does not work as written since the elements of the list can be of SEVERAL different types (like a sphere and a polygon and a mesh etc. etc.) but lists need to have elements of the same type.
1.2.2 The solution
Use 'existential types' - an extension to Haskell that can be found in most compilers.
The following example is based on GHC :
{-# OPTIONS -fglasgow-exts #-} {- ...-} data AnyRenderable = forall a. Renderable a => AnyRenderable a instance Renderable AnyRenderable where boundingSphere (AnyRenderable a) = boundingSphere a hit (AnyRenderable a) = hit a {- ... -}
[ AnyRenderable x , AnyRenderable y , AnyRenderable z ]
1.3 Dynamic dispatch mechanism of OOP
Existential types in conjunction with type classes can be used to emulate the dynamic dispatch mechanism of object oriented programming languages. To illustrate this concept I show how a classic example from object oriented programming can be encoded in Haskell.
class Shape_ a where perimeter :: a -> Double area :: a -> Double data Shape = forall a. Shape_ a => Shape a type Radius = Double type Side = Double data Circle = Circle Radius data Rectangle = Rectangle Side Side data Square = Square Side instance Shape_ Circle where perimeter (Circle r) = 2 * pi * r area (Circle r) = pi * r * r instance Shape_ Rectangle where perimeter (Rectangle x y) = 2*(x + y) area (Rectangle x y) = x * y instance Shape_ Square where perimeter (Square s) = 4*s area (Square s) = s*s instance Shape_ Shape where perimeter (Shape shape) = perimeter shape area (Shape shape) = area shape -- -- Smart constructor -- circle :: Radius -> Shape circle r = Shape (Circle r) rectangle :: Side -> Side -> Shape rectangle x y = Shape (Rectangle x y) square :: Side -> Shape square s = Shape (Square s) shapes :: [Shape] shapes = [circle 2.4, rectangle 3.1 4.4, square 2.1]
(You may see other Smart constructors for other purposes).
1.4 Generalised algebraic datatype
The type of the2 Alternate methods
2.1 Concrete data types
2.1.1 Universal instance of a Class
Here one way to simulate existentials (Hawiki note: (Borrowed from somewhere...))
Suppose I have a type class Shape a
type Point = (Float,Float) class Shape a where draw :: a -> IO () translate :: a-> Point -> a
Then we can pack shapes up into a concrete data type like this:
data SHAPE = SHAPE (IO ()) (Point -> SHAPE)
with a function like this
packShape :: Shape a => a -> SHAPE packShape s = SHAPE (draw s) (\(x,y) -> packShape (translate s (x,y)))
This would be useful if we needed a list of shapes that we would need to translate and draw.
In fact we can makeinstance Shape SHAPE where draw (SHAPE d t) = d translate (SHAPE d t) = t
So SHAPE is a sort of universal instance.
2.1.2 Using constructors and combinators
Why bother with classdata Shape = Shape { draw :: IO() translate :: (Int, Int) -> Shape }
Then you can create a library of shape constructors and combinators that each have defined "draw" and "translate" in their "where" clauses.
circle :: (Int, Int) -> Int -> Shape circle (x,y) r = Shape draw1 translate1 where draw1 = ... translate1 (x1,y1) = circle (x+x1, y+y1) r shapeGroup :: [Shape] -> Shape shapeGroup shapes = Shape draw1 translate1 where draw1 = sequence_ $ map draw shapes translate1 v = shapeGroup $ map (translate v) shapes
2.2 Cases that really require existentials
There are cases where this sort of trick doesnt work. Here are two examples from a haskell mailing list discussion (from K. Claussen) that don't seem expressible without existentials. (But maybe one can rethink the whole thing :)
data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
and
data Action = forall b . Act (IORef b) (b -> IO ())
3 Examples from the Essential Haskell Compiler project
See the documentation on EHC, each paper at the Version 4 part:
- Chapter 8 (EH4) of Atze Dijksta's Essential Haskell PhD thesis (most recent version). A detailed explanation. It explains also that existential types can be expressed in Haskell, but their use is restricted to data declarations, and the notation (using keyword ) may be confusing. In Essential Haskell, existential types can occur not only in data declarations, and a separate keywordforallis used for their notation.exists
- Essential Haskell Compiler overview
- Examples
4 See also
- A mailinglist discussion: http://haskell.org/pipermail/haskell-cafe/2003-October/005231.html
- An example of encoding existentials using RankTwoPolymorphism : http://haskell.org/pipermail/haskell-cafe/2003-October/005304.html
4.1 Trac
Existential Quantification is a detailed material on the topic. It has link also to the smaller Existential Quantifier page.
