Existential type

From HaskellWiki

(Difference between revisions)

Current revision

This is an extension of Haskell available in GHC. See the GHC documentation: http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html

1 Introduction to existential types

1.1 Overview

Normally when creating a new type using

type

newtype

data

, etc., every type variable that appears on the right-hand side must also appear on the left-hand side. Existential types are a way of turning this off.

1.2 Basics

Existential types can be used for several different purposes. But what they do is to 'hide' a type variable on the right-hand side.

Normally, any type variable appearing on the right must also appear on the left:

data Worker x y = Worker {buffer :: b, input :: x, output :: y}

This is an error, since the type of the buffer isn't specified on the right (it's a type variable rather than a type) but also isn't specified on the left (there's no 'b' in the left part). In Haskell98, you would have to write

data Worker b x y = Worker {buffer :: b, input :: x, output :: y}

That may or may not be an actual problem.

Usually there is no problem at all with this state of affairs (which is why Haskell98 works this way). However, suppose that a

Worker

can use any type 'b' so long as it belongs to some particular class. Then every function that uses a

Worker

will have a type like

foo :: (Buffer b) => Worker b Int Int

or something. (In particular, failing to write an explicit type signature will invoke the dreaded monomorphism restriction.) Using existential types, we can avoid this:

data Worker x y = forall b. Buffer b => Worker {buffer :: b, input :: x, output :: y}
 
foo :: Worker Int Int

The type of the buffer now does not appear in the

Worker

type at all. This has a number of consequences. First of all, it is now impossible for a function to demand a

Worker

having a specific type of buffer. Second, the type of

foo

can now be derived automatically without needing an explicit type signature. (No monomorphism restriction.) Thirdly, since code now has no idea what type the

buffer

function returns, you are more limited in what you can do to it.

In general, when you use a 'hidden' type in this way, you will usually want that type to belong to a specific class, or you will want to pass some functions along that can work on that type. Otherwise you'll have some value belonging to a random unknown type, and you won't be able to do anything to it!

Note: You can use existential types to convert a more specific type into a less specific one. (See the examples below.) There is no way to perform the reverse conversion!

2 Examples

2.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]
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'"

2.2 Expanded example - rendering objects in a raytracer

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

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

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

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

Control.Exception

(see documentation) provides extensible exceptions by making the core exception type,

SomeException

, an existential:

class (Show e, Typeable e) => Exception e where
    toException :: e -> SomeException
    fromException :: SomeException -> Maybe e
data SomeException = forall a. Exception a => SomeException a

You can define your own exceptions by making them an instance of the

Exception

class. Then there are two basic ways of dealing with exceptions:

If you have a
SomeException
value, use
fromException
. This returns
Just e
if the exception is the type you want. If it's something else, you get
Nothing
. You could check multiple types using a guard. This is what you'll have to use if you're dealing with
SomeException
s in pure code.
If you're in IO and have an expression that might throw an exception,
catch
lets you catch it. (There's also a version generalised to other instances of
MonadIO
in the
lifted-base
package). Its second argument takes a handler, which is a function accepting an exception of the type you want. If the first argument throws an exception,
catch
uses the
Typeable
library's typesafe cast to try to convert it to the type you want, then (if it succeeded) passes it to the handler. You can apply
catch
many times to the same expression with handlers for different exception types.
Even if
fromException
doesn't turn up an exception type you know, and
catch
doesn't catch an exception type you know, you can still
show
the unknown exception, maybe after catching
SomeException
.

3 Alternate methods

3.1 Concrete data types

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

3.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 = mapM_ draw shapes
       translate1 v = shapeGroup $ map (translate v) shapes

3.2 Cases that really require existentials

There are cases where this sort of trick doesn't 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.3 Existentials in terms of "forall"

It is also possible to express existentials as type expressions directly (without a

data

declaration) with RankNTypes. Taking the above example:

data Obj = forall a. (Show a) => Obj a

the type

Obj

is equivalent to:

forall r. (forall a. Show a => a -> r) -> r

(the leading

forall r.

is optional unless the expression is part of another expression). The conversions are:

fromObj ::  Obj 
        -> forall r. (forall a. Show a => a -> r) -> r
fromObj (Obj x) k = k x
 
toObj :: (forall r. (forall a. Show a => a -> r) -> r) 
      ->  Obj
toObj f = f Obj

4 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

5 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
Another mailing list discussion (functional vs OO approaches): http://www.haskell.org/pipermail/haskell/2005-June/016058.html
Just another one: http://www.haskell.org/pipermail/haskell-cafe/2008-January/037950.html "type question again"
Haskell antipattern: Existential typeclass http://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-typeclass/

5.1 Trac

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

Retrieved from "http://www.haskell.org/haskellwiki/Existential_type"

Categories: Idioms | Glossary | Language extensions

Personal tools

Views