Difference between revisions of "Existential type"
(Add to categroy "Language extensions") 
(→Examples from the Essential Haskell Compiler project: fix headline link) 

(20 intermediate revisions by 12 users not shown)  
Line 1:  Line 1:  
__TOC__ 
__TOC__ 

−  This is 
+  This is an extension of Haskell available in [[GHC]]. 
−  +  
+  {{GHCUsersGuideglasgow_extsexistentiallyquantifieddataconstructorsan Existential Quantification section}} 

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

+  
+  === Overview === 

+  
+  Normally when creating a new type using <hask>type</hask>, <hask>newtype</hask>, <hask>data</hask>, etc., every type variable that appears on the righthand side must also appear on the lefthand side. Existential types are a way of turning this off. 

+  
+  === Basics === 

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

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

+  
+  <haskell> 

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

+  </haskell> 

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

+  
+  <haskell> 

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

+  </haskell> 

+  
+  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 <hask>Worker</hask> can use ''any'' type 'b' so long as it belongs to some particular class. Then every function that uses a <hask>Worker</hask> will have a type like 

+  
+  <haskell> 

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

+  </haskell> 

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

+  
+  <haskell> 

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

+  
+  foo :: Worker Int Int 

+  </haskell> 

+  
+  The type of the buffer now does ''not'' appear in the <hask>Worker</hask> type at all. 

+  
+  This has a number of consequences. First of all, it is now impossible for a function to demand a <hask>Worker</hask> having a specific type of buffer. Second, the type of <hask>foo</hask> can now be derived automatically without needing an explicit type signature. (No [[monomorphism restriction]].) Thirdly, since code now has ''no idea'' what type the <hask>buffer</hask> 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! 

+  
+  == Examples == 

===A short example=== 
===A short example=== 

Line 12:  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 128:  Line 175:  
The type of the <hask>parse</hask> function for [[Generalised algebraic datatype#Motivating examplethis 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 examplethis 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/ControlException.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>liftedbase</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 189:  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 195:  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 206:  Line 268:  
(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> 

+  
⚫  
See the [http://www.cs.uu.nl/wiki/Ehc/#On_EHC documentation on EHC], each paper at the ''Version 4'' part: 
See the [http://www.cs.uu.nl/wiki/Ehc/#On_EHC documentation on EHC], each paper at the ''Version 4'' part: 

* Chapter 8 (EH4) of Atze Dijkstra's [http://www.cs.uu.nl/groups/ST/Projects/ehc/ehcbook.pdf 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 <hask>forall</hask>) may be confusing. In Essential Haskell, existential types can occur not only in data declarations, and a separate keyword <hask>exists</hask> is used for their notation. 
* Chapter 8 (EH4) of Atze Dijkstra's [http://www.cs.uu.nl/groups/ST/Projects/ehc/ehcbook.pdf 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 <hask>forall</hask>) may be confusing. In Essential Haskell, existential types can occur not only in data declarations, and a separate keyword <hask>exists</hask> is used for their notation. 

* [http://www.cs.uu.nl/wiki/pub/Ehc/WebHome/20050107ehintro.pdf Essential Haskell Compiler overview] 
* [http://www.cs.uu.nl/wiki/pub/Ehc/WebHome/20050107ehintro.pdf Essential Haskell Compiler overview] 

−  * [http:// 
+  * [http://web.archive.org/web/20160917160644/http://foswiki.cs.uu.nl/foswiki/Ehc/Examples#EH_4_forall_and_exists_everywher Examples] 
==See also== 
==See also== 

* A mailinglist discussion: http://haskell.org/pipermail/haskellcafe/2003October/005231.html 
* A mailinglist discussion: http://haskell.org/pipermail/haskellcafe/2003October/005231.html 

−  *An example of encoding existentials using RankTwoPolymorphism 
+  * An example of encoding existentials using RankTwoPolymorphism: http://haskell.org/pipermail/haskellcafe/2003October/005304.html 
−  +  * Another mailing list discussion (functional vs OO approaches): http://www.haskell.org/pipermail/haskell/2005June/016058.html 

+  * Just another one: http://www.haskell.org/pipermail/haskellcafe/2008January/037950.html "type question again" 

+  * Haskell antipattern: Existential typeclass http://lukepalmer.wordpress.com/2010/01/24/haskellantipatternexistentialtypeclass/ 

+  
+  === Prime Trac === 

−  [http:// 
+  [http://prime.haskell.org/wiki/ExistentialQuantification Existential Quantification] is a detailed material on the topic. It has link also to the smaller [http://prime.haskell.org/wiki/ExistentialQuantifier Existential Quantifier] page. 
[[Category:Idioms]] 
[[Category:Idioms]] 
Latest revision as of 19:13, 4 April 2019
Contents
This is an extension of Haskell available in GHC.
The GHC Users Guide has an Existential Quantification section.
Introduction to existential types
Overview
Normally when creating a new type using type
, newtype
, data
, etc., every type variable that appears on the righthand side must also appear on the lefthand side. Existential types are a way of turning this off.
Basics
Existential types can be used for several different purposes. But what they do is to 'hide' a type variable on the righthand 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!
Examples
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'"
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 fglasgowexts #}
{ ...}
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.
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, usefromException
. This returnsJust e
if the exception is the type you want. If it's something else, you getNothing
. You could check multiple types using a guard. This is what you'll have to use if you're dealing withSomeException
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 ofMonadIO
in theliftedbase
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 theTypeable
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 applycatch
many times to the same expression with handlers for different exception types.  Even if
fromException
doesn't turn up an exception type you know, andcatch
doesn't catch an exception type you know, you can stillshow
the unknown exception, maybe after catchingSomeException
.
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 = mapM_ draw shapes
translate1 v = shapeGroup $ map (translate v) shapes
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)
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
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 keywordexists
is used for their notation.  Essential Haskell Compiler overview
 Examples
See also
 A mailinglist discussion: http://haskell.org/pipermail/haskellcafe/2003October/005231.html
 An example of encoding existentials using RankTwoPolymorphism: http://haskell.org/pipermail/haskellcafe/2003October/005304.html
 Another mailing list discussion (functional vs OO approaches): http://www.haskell.org/pipermail/haskell/2005June/016058.html
 Just another one: http://www.haskell.org/pipermail/haskellcafe/2008January/037950.html "type question again"
 Haskell antipattern: Existential typeclass http://lukepalmer.wordpress.com/2010/01/24/haskellantipatternexistentialtypeclass/
Prime Trac
Existential Quantification is a detailed material on the topic. It has link also to the smaller Existential Quantifier page.