# Existential type

### From HaskellWiki

m (Idiot-features here doesn't know left from right... >_<) |
Hairy Dude (Talk | contribs) (→SomeException: catching SomeException) |
||

(11 intermediate revisions by 9 users not shown) | |||

Line 1: | Line 1: | ||

__TOC__ | __TOC__ | ||

− | This is | + | This is an extension of Haskell available in [[GHC]]. See the GHC documentation: |

− | http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html | + | http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html |

==Introduction to existential types== | ==Introduction to existential types== | ||

Line 36: | Line 36: | ||

<haskell> | <haskell> | ||

− | data Worker x y = forall | + | data Worker x y = forall b. Buffer b => Worker {buffer :: b, input :: x, output :: y} |

foo :: Worker Int Int | foo :: Worker Int Int | ||

Line 58: | Line 58: | ||

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

+ | xs :: [Obj] | ||

xs = [Obj 1, Obj "foo", Obj 'c'] | xs = [Obj 1, Obj "foo", Obj 'c'] | ||

Line 174: | Line 175: | ||

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

+ | |||

+ | === SomeException === | ||

+ | <hask>Control.Exception</hask> (see [http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Exception.html documentation]) provides extensible exceptions by making the core exception type, <hask>SomeException</hask>, an existential: | ||

+ | |||

+ | <haskell> | ||

+ | class (Show e, Typeable e) => Exception e where | ||

+ | toException :: e -> SomeException | ||

+ | fromException :: SomeException -> Maybe e | ||

+ | data SomeException = forall a. Exception a => SomeException a | ||

+ | </haskell> | ||

+ | |||

+ | You can define your own exceptions by making them an instance of the <hask>Exception</hask> class. Then there are two basic ways of dealing with exceptions: | ||

+ | #If you have a <hask>SomeException</hask> value, use <hask>fromException</hask>. This returns <hask>Just e</hask> if the exception is the type you want. If it's something else, you get <hask>Nothing</hask>. You could check multiple types using a guard. This is what you'll have to use if you're dealing with <hask>SomeException</hask>s in pure code. | ||

+ | #If you're in IO and have an expression that might throw an exception, <hask>catch</hask> lets you catch it. (There's also a version generalised to other instances of <hask>MonadIO</hask> in the <hask>lifted-base</hask> 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, <hask>catch</hask> uses the <hask>Typeable</hask> 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 <hask>catch</hask> many times to the same expression with handlers for different exception types. | ||

+ | #Even if <hask>fromException</hask> doesn't turn up an exception type you know, and <hask>catch</hask> doesn't catch an exception type you know, you can still <hask>show</hask> the unknown exception, maybe after catching <hask>SomeException</hask>. | ||

==Alternate methods== | ==Alternate methods== | ||

Line 235: | Line 251: | ||

shapeGroup shapes = Shape draw1 translate1 | shapeGroup shapes = Shape draw1 translate1 | ||

where | where | ||

− | draw1 = | + | draw1 = mapM_ draw shapes |

translate1 v = shapeGroup $ map (translate v) shapes | translate1 v = shapeGroup $ map (translate v) shapes | ||

</haskell> | </haskell> | ||

Line 241: | Line 257: | ||

===Cases that really require existentials=== | ===Cases that really require existentials=== | ||

− | There are cases where this sort of trick | + | 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 :) | existentials. (But maybe one can rethink the whole thing :) | ||

<haskell> | <haskell> | ||

Line 251: | Line 267: | ||

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

+ | |||

+ | === Existentials in terms of "forall" === | ||

+ | It is also possible to express existentials as type expressions directly (without a <hask>data</hask> declaration) with RankNTypes. Taking the above example: | ||

+ | |||

+ | <haskell>data Obj = forall a. (Show a) => Obj a</haskell> | ||

+ | |||

+ | the type <hask>Obj</hask> is equivalent to: | ||

+ | |||

+ | <haskell>forall r. (forall a. Show a => a -> r) -> r</haskell> | ||

+ | |||

+ | (the leading <hask>forall r.</hask> is optional unless the expression is part of another expression). The conversions are: | ||

+ | |||

+ | <haskell> | ||

+ | 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 | ||

+ | </haskell> | ||

== 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 261: | Line 298: | ||

==See also== | ==See also== | ||

* A mailinglist discussion: http://haskell.org/pipermail/haskell-cafe/2003-October/005231.html | * 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 | + | * 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" | ||

+ | |||

=== Trac === | === Trac === | ||

## Revision as of 19:22, 22 July 2012

## Contents |

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### 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*any*type 'b' so long as it belongs to some particular class. Then every function that uses a

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

*not*appear in the

*no idea*what type the

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

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

[ AnyRenderable x , AnyRenderable y , AnyRenderable z ]

### 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### 2.5 SomeException

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

- If you have a value, useSomeException. This returnsfromExceptionif the exception is the type you want. If it's something else, you getJust e. You could check multiple types using a guard. This is what you'll have to use if you're dealing withNothings in pure code.SomeException
- If you're in IO and have an expression that might throw an exception, lets you catch it. (There's also a version generalised to other instances ofcatchin theMonadIOpackage). 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,lifted-baseuses thecatchlibrary's typesafe cast to try to convert it to the type you want, then (if it succeeded) passes it to the handler. You can applyTypeablemany times to the same expression with handlers for different exception types.catch
- Even if doesn't turn up an exception type you know, andfromExceptiondoesn't catch an exception type you know, you can stillcatchthe unknown exception, maybe after catchingshow.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 makeinstance 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 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 = 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 ())

### 3.3 Existentials in terms of "forall"

It is also possible to express existentials as type expressions directly (without adata Obj = forall a. (Show a) => Obj a

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

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

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

### 5.1 Trac

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