Difference between revisions of "Existential type"

From HaskellWiki
Jump to navigation Jump to search
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
   
  +
==Introduction to existential types==
== Dynamic dispatch mechanism of OOP ==
 
  +
  +
===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

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

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:

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

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:

class Renderable a where
 boundingSphere :: a -> Sphere
 hit :: a -> [Fragment] -- returns the "fragments" of all hits with ray
{- ... etc ... -}

To solve the problem, the hit function must apply to several objects (like a sphere and a polygon for instance).

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.

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
  {-      ... -}

Now, create lists with type [AnyRenderable], for example,

    [ AnyRenderable x
    , AnyRenderable y
    , AnyRenderable z ]

where x, y, z can be from different instances of Renderable.

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

Generalised algebraic datatype

The type of the parse function for 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

 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 make SHAPE an instance of Shape:

  instance Shape SHAPE where
    draw (SHAPE d t) = d
    translate (SHAPE d t) = t

So SHAPE is a sort of universal instance.

Using constructors and combinators

Why bother with class Shape? Why not just go straight to

 data 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

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

(Maybe this last one could be done as a type Act (IORef b) (IORef b -> IO ()) then we could hide the IORef as above, that is go ahead and apply the second argument to the first)

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 forall) may be confusing. In Essential Haskell, existential types can occur not only in data declarations, and a separate keyword exists is used for their notation.
  • Essential Haskell Compiler overview
  • Examples

See also

Trac

Existential Quantification is a detailed material on the topic. It has link also to the smaller Existential Quantifier page.