Personal tools

Existential type

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m
(Add to categroy "Language extensions")
Line 222: Line 222:
 
[[Category:Idioms]]
 
[[Category:Idioms]]
 
[[Category:Glossary]]
 
[[Category:Glossary]]
  +
[[Category:Language extensions]]

Revision as of 14:59, 23 June 2007

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

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

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 the
parse
function for this GADT is a good example to illustrate the concept of existential type.

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

2.1.2 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

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

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

4 See also

4.1 Trac

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