https://wiki.haskell.org/api.php?action=feedcontributions&user=Davesque&feedformat=atomHaskellWiki - User contributions [en]2024-03-29T06:18:10ZUser contributionsMediaWiki 1.35.5https://wiki.haskell.org/index.php?title=GADTs_for_dummies&diff=56425GADTs for dummies2013-07-20T01:42:35Z<p>Davesque: </p>
<hr />
<div>[[Category:Tutorials]]<br />
[[Category:Language extensions]]<br />
<br />
For a long time, I didn't understand what GADTs were or how they could be used. It was sort of a conspiracy of silence &mdash; people who understood GADTs thought<br />
that everything was obvious and didn't need further explanation, but I still<br />
couldn't understand them.<br />
<br />
Now that I have an idea of how it works, I think that it was really obvious. :) So, I want to share my understanding of GADTs. Maybe the way I realized how GADTs work could help<br />
someone else. See also [[Generalised algebraic datatype]]<br />
<br />
== Type functions ==<br />
<br />
A "data" declaration is a way to declare both type constructor and data<br />
constructors. For example,<br />
<br />
<haskell><br />
data Either a b = Left a | Right b<br />
</haskell><br />
<br />
declares type constructor "Either" and two data constructors "Left"<br />
and "Right". Ordinary Haskell functions works with data constructors:<br />
<br />
<haskell><br />
isLeft (Left a) = True<br />
isLeft (Right b) = False<br />
</haskell><br />
<br />
but there is also an analogous way to work with type constructors!<br />
<br />
<haskell><br />
type X a = Either a a<br />
</haskell><br />
<br />
declares a TYPE FUNCTION named "X". Its parameter "a" must be some type<br />
and it returns some type as its result. We can't use "X" on data values,<br />
but we can use it on type values. Type constructors declared with<br />
"data" statements and type functions declared with "type" statements<br />
can be used together to build arbitrarily complex types. In such<br />
"computations" type constructors serves as basic "values" and type<br />
functions as a way to process them.<br />
<br />
Indeed, type functions in Haskell are very limited compared to<br />
ordinary functions - they don't support pattern matching,<br />
nor multiple statements, nor recursion.<br />
<br />
== Hypothetical Haskell extension - Full-featured type functions ==<br />
<br />
Let's build a hypothetical Haskell extension that mimics, for type<br />
functions, the well-known ways to define ordinary functions, including<br />
pattern matching:<br />
<br />
<haskell><br />
type F [a] = Set a<br />
</haskell><br />
<br />
multiple statements (this is meaningful only in the presence of pattern matching):<br />
<br />
<haskell><br />
type F Bool = Char<br />
F String = Int<br />
</haskell><br />
<br />
and recursion (which again needs pattern matching and multiple statements):<br />
<br />
<haskell><br />
type F [a] = F a<br />
F (Map a b) = F b<br />
F (Set a) = F a<br />
F a = a<br />
</haskell><br />
<br />
As you may already have guessed, this last definition calculates a simple base type of arbitrarily-nested collections, e.g.: <br />
<br />
<haskell><br />
F [[[Set Int]]] = <br />
F [[Set Int]] =<br />
F [Set Int] = <br />
F (Set Int) =<br />
F Int =<br />
Int<br />
</haskell><br />
<br />
Let's not forget about statement guards:<br />
<br />
<haskell><br />
type F a | IsSimple a == TrueType = a<br />
</haskell><br />
<br />
Here we define type function F only for simple datatypes by using a<br />
guard type function "IsSimple":<br />
<br />
<haskell><br />
type IsSimple Bool = TrueType<br />
IsSimple Int = TrueType<br />
....<br />
IsSimple Double = TrueType<br />
IsSimple a = FalseType<br />
<br />
data TrueType = T<br />
data FalseType = F<br />
</haskell><br />
<br />
These definitions seem a bit odd, and while we are in imaginary land,<br />
let's consider a way to write this shorter:<br />
<br />
<haskell><br />
type F a | IsSimple a = a<br />
<br />
type IsSimple Bool<br />
IsSimple Int<br />
....<br />
IsSimple Double<br />
</haskell><br />
<br />
Here, we defined a list of simple types. The implied result of all<br />
written statements for "IsSimple" is True, and False for<br />
everything else. Essentially, "IsSimple" is a TYPE PREDICATE!<br />
<br />
I really love it! :) How about constructing a predicate that traverses a<br />
complex type trying to decide whether it contains "Int" anywhere?<br />
<br />
<haskell><br />
type HasInt Int<br />
HasInt [a] = HasInt a<br />
HasInt (Set a) = HasInt a<br />
HasInt (Map a b) | HasInt a<br />
HasInt (Map a b) | HasInt b<br />
</haskell><br />
<br />
or a type function that substitutes one type with another inside<br />
arbitrarily-deep types:<br />
<br />
<haskell><br />
type Replace t a b | t==a = b<br />
Replace [t] a b = [Replace t a b]<br />
Replace (Set t) a b = Set (Replace t a b)<br />
Replace (Map t1 t2) a b = Map (Replace t1 a b) (Replace t2 a b)<br />
Replace t a b = t<br />
</haskell><br />
<br />
== One more hypothetical extension - multi-value type functions ==<br />
<br />
Let's add more fun! We will introduce one more hypothetical Haskell<br />
extension - type functions that may have MULTIPLE VALUES. Say,<br />
<br />
<haskell><br />
type Collection a = [a]<br />
Collection a = Set a<br />
Collection a = Map b a<br />
</haskell><br />
<br />
So, "Collection Int" has "[Int]", "Set Int" and "Map String Int" as<br />
its values, i.e. different collection types with elements of type<br />
"Int".<br />
<br />
Pay attention to the last statement of the "Collection" definition, where<br />
we used the type variable "b" that was not mentioned on the left side,<br />
nor defined in any other way. Since it's perfectly possible for the<br />
"Collection" function to have multiple values, using some free variable on<br />
the right side that can be replaced with any type is not a problem<br />
at all. "Map Bool Int", "Map [Int] Int" and "Map Int Int" all are<br />
possible values of "Collection Int" along with "[Int]" and "Set Int".<br />
<br />
At first glance, it seems that multiple-value functions are meaningless - they<br />
can't be used to define datatypes, because we need concrete types here. But<br />
if we take another look, they can be useful to define type constraints and<br />
type families.<br />
<br />
We can also represent a multiple-value function as a predicate:<br />
<br />
<haskell><br />
type Collection a [a]<br />
Collection a (Set a)<br />
Collection a (Map b a)<br />
</haskell><br />
<br />
If you're familiar with Prolog, you should know that a predicate, in contrast to<br />
a function, is a multi-directional thing - it can be used to deduce any<br />
parameter from the other ones. For example, in this hypothetical definition:<br />
<br />
<haskell><br />
head | Collection Int a :: a -> Int<br />
</haskell><br />
<br />
we define a 'head' function for any Collection containing Ints.<br />
<br />
And in this, again, hypothetical definition:<br />
<br />
<haskell><br />
data Safe c | Collection c a = Safe c a<br />
</haskell><br />
<br />
we deduced element type 'a' from collection type 'c' passed as the<br />
parameter to the type constructor.<br />
<br />
<br />
<br />
== Back to real Haskell - type classes ==<br />
<br />
After reading about all of these glorious examples, you may be wondering<br />
"Why doesn't Haskell support full-featured type functions?" Hold your breath...<br />
Haskell already contains them, and GHC has implemented all of the<br />
capabilities mentioned above for more than 10 years! They were just named...<br />
TYPE CLASSES! Let's translate all of our examples to their language:<br />
<br />
<haskell><br />
class IsSimple a<br />
instance IsSimple Bool<br />
instance IsSimple Int<br />
....<br />
instance IsSimple Double<br />
</haskell><br />
<br />
The Haskell'98 standard supports type classes with only one parameter.<br />
That limits us to only defining type predicates like this one. But GHC and<br />
Hugs support multi-parameter type classes that allow us to define<br />
arbitrarily-complex type functions<br />
<br />
<haskell><br />
class Collection a c<br />
instance Collection a [a]<br />
instance Collection a (Set a)<br />
instance Collection a (Map b a)<br />
</haskell><br />
<br />
All of the "hypothetical" Haskell extensions we investigated earlier are<br />
actually implemented at the type class level!<br />
<br />
Pattern matching:<br />
<br />
<haskell><br />
instance Collection a [a]<br />
</haskell><br />
<br />
Multiple statements:<br />
<br />
<haskell><br />
instance Collection a [a]<br />
instance Collection a (Set a)<br />
</haskell><br />
<br />
Recursion:<br />
<br />
<haskell><br />
instance (Collection a c) => Collection a [c]<br />
</haskell><br />
<br />
Pattern guards:<br />
<br />
<haskell><br />
instance (IsSimple a) => Collection a (UArray a)<br />
</haskell><br />
<br />
<br />
<br />
Let's define a type class which contains any collection which uses Int in<br />
its elements or indexes:<br />
<br />
<haskell><br />
class HasInt a<br />
instance HasInt Int<br />
instance (HasInt a) => HasInt [a]<br />
instance (HasInt a) => HasInt (Map a b)<br />
instance (HasInt b) => HasInt (Map a b)<br />
</haskell><br />
<br />
<br />
Another example is a class that replaces all occurrences of 'a' with<br />
'b' in type 't' and return the result as 'res':<br />
<br />
<haskell><br />
class Replace t a b res<br />
instance Replace t a a t<br />
instance Replace [t] a b [Replace t a b]<br />
instance (Replace t a b res)<br />
=> Replace (Set t) a b (Set res)<br />
instance (Replace t1 a b res1, Replace t2 a b res2)<br />
=> Replace (Map t1 t2) a b (Map res1 res2)<br />
instance Replace t a b t<br />
</haskell><br />
<br />
You can compare it to the hypothetical definition we gave earlier.<br />
It's important to note that type class instances, as opposed to<br />
function statements, are not checked in order. Instead, the most<br />
_specific_ instance is automatically selected. So, in the Replace case, the<br />
last instance, which is the most general instance, will be selected only if all the others<br />
fail to match, which is what we want.<br />
<br />
In many other cases this automatic selection is not powerful enough<br />
and we are forced to use some artificial tricks or complain to the<br />
language developers. The two most well-known language extensions<br />
proposed to solve such problems are instance priorities, which allow<br />
us to explicitly specify instance selection order, and '/=' constraints,<br />
which can be used to explicitly prohibit unwanted matches:<br />
<br />
<haskell><br />
instance Replace t a a t<br />
instance (a/=b) => Replace [t] a b [Replace t a b]<br />
instance (a/=b, t/=[_]) => Replace t a b t<br />
</haskell><br />
<br />
You can check that these instances no longer overlap.<br />
<br />
<br />
In practice, type-level arithmetic by itself is not very useful. It becomes a<br />
fantastic tool when combined with another feature that type classes provide -<br />
member functions. For example:<br />
<br />
<haskell><br />
class Collection a c where<br />
foldr1 :: (a -> a -> a) -> c -> a<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
sum :: (Num a, Collection a c) => c -> a<br />
sum = foldr1 (+)<br />
</haskell><br />
<br />
<br />
I'll also be glad to see the possibility of using type classes in data<br />
declarations, like this:<br />
<br />
<haskell><br />
data Safe c = (Collection c a) => Safe c a<br />
</haskell><br />
<br />
but as far as I know, this is not yet implemented.<br />
<br />
<br />
UNIFICATION<br />
...<br />
<br />
<br />
<br />
== Back to GADTs ==<br />
<br />
If you are wondering how all of these interesting type manipulations relate to<br />
GADTs, here is the answer. As you know, Haskell contains highly<br />
developed ways to express data-to-data functions. We also know that<br />
Haskell contains rich facilities to write type-to-type functions in the form of<br />
"type" statements and type classes. But how do "data" statements fit into this<br />
infrastructure?<br />
<br />
My answer: they just define a type-to-data constructor translation. Moreover,<br />
this translation may give multiple results. Say, the following definition:<br />
<br />
<haskell><br />
data Maybe a = Just a | Nothing<br />
</haskell><br />
<br />
defines type-to-data constructors function "Maybe" that has a parameter<br />
"a" and for each "a" has two possible results - "Just a" and<br />
"Nothing". We can rewrite it in the same hypothetical syntax that was<br />
used above for multi-value type functions:<br />
<br />
<haskell><br />
data Maybe a = Just a<br />
Maybe a = Nothing<br />
</haskell><br />
<br />
Or how about this:<br />
<br />
<haskell><br />
data List a = Cons a (List a)<br />
List a = Nil<br />
</haskell><br />
<br />
and this:<br />
<br />
<haskell><br />
data Either a b = Left a<br />
Either a b = Right b<br />
</haskell><br />
<br />
But how flexible are "data" definitions? As you should remember, "type"<br />
definitions were very limited in their features, while type classes,<br />
on the other hand, were more developed than ordinary Haskell functions<br />
facilities. What about features of "data" definitions examined as sort of functions?<br />
<br />
On the one hand, they supports multiple statements and multiple results and<br />
can be recursive, like the "List" definition above. On the other, that's all -<br />
no pattern matching or even type constants on the left side and no guards.<br />
<br />
Lack of pattern matching means that the left side can contain only free type<br />
variables. That in turn means that the left sides of all "data" statements for a<br />
type will be essentially the same. Therefore, repeated left sides in<br />
multi-statement "data" definitions are omitted and instead of<br />
<br />
<haskell><br />
data Either a b = Left a<br />
Either a b = Right b<br />
</haskell><br />
<br />
we write just<br />
<br />
<haskell><br />
data Either a b = Left a<br />
| Right b<br />
</haskell><br />
<br />
<br />
And here we finally come to GADTs! It's just a way to define data types using<br />
pattern matching and constants on the left side of "data" statements!<br />
Let's say we want to do this:<br />
<br />
<haskell><br />
data T String = D1 Int<br />
T Bool = D2<br />
T [a] = D3 (a,a)<br />
</haskell><br />
<br />
<br />
We cannot do this using a standard data definition. So, now we must use a GADT definition:<br />
<br />
<haskell><br />
data T a where<br />
D1 :: Int -> T String<br />
D2 :: T Bool<br />
D3 :: (a,a) -> T [a]<br />
</haskell><br />
<br />
Amazed? After all, GADTs seem to be a really simple and obvious extension to<br />
data type definition facilities.<br />
<br />
<br />
<br />
<br />
<br />
<br />
<br />
The idea here is to allow a data constructor's return type to be specified<br />
directly:<br />
<br />
<haskell><br />
data Term a where<br />
Lit :: Int -> Term Int<br />
Pair :: Term a -> Term b -> Term (a,b)<br />
...<br />
</haskell><br />
<br />
In a function that performs pattern matching on Term, the pattern match gives<br />
type as well as value information. For example, consider this function:<br />
<br />
<haskell><br />
eval :: Term a -> a<br />
eval (Lit i) = i<br />
eval (Pair a b) = (eval a, eval b)<br />
...<br />
</haskell><br />
<br />
If the argument matches Lit, it must have been built with a Lit constructor,<br />
so type 'a' must be Int, and hence we can return 'i' (an Int) in the right<br />
hand side. The same thing applies to the Pair constructor.<br />
<br />
<br />
<br />
<br />
<br />
<br />
== Further reading ==<br />
<br />
The best paper on type level arithmetic using type classes I've seen<br />
is "Faking it: simulating dependent types in Haskell"<br />
( http://www.cs.nott.ac.uk/~ctm/faking.ps.gz ). Most of<br />
this article comes from his work.<br />
<br />
A great demonstration of type-level arithmetic is in the TypeNats package,<br />
which "defines type-level natural numbers and arithmetic operations on<br />
them including addition, subtraction, multiplication, division and GCD"<br />
( darcs get --partial --tag '0.1' http://www.eecs.tufts.edu/~rdocki01/typenats/ )<br />
<br />
I should also mention here Oleg Kiselyov's page on type-level<br />
programming in Haskell: http://okmij.org/ftp/Haskell/types.html<br />
<br />
<br />
There are plenty of GADT-related papers, but the best one for beginners<br />
is "Fun with phantom types"<br />
(http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf).<br />
Phantom types is another name of GADT. You should also know that this<br />
paper uses old GADT syntax. This paper is a must-read because it<br />
contains numerous examples of practical GADT usage - a theme completely<br />
omitted from my article.<br />
<br />
<br />
Other GADT-related papers:<br />
<br />
"Dynamic Optimization for Functional Reactive Programming using<br />
Generalized Algebraic Data Types"<br />
http://www.cs.nott.ac.uk/~nhn/Publications/icfp2005.pdf<br />
<br />
"Phantom types" (actually more scientific version of "Fun with phantom types")<br />
http://citeseer.ist.psu.edu/rd/0,606209,1,0.25,Download/http:qSqqSqwww.informatik.uni-bonn.deqSq~ralfqSqpublicationsqSqPhantom.ps.gz<br />
<br />
"Phantom types and subtyping" http://arxiv.org/ps/cs.PL/0403034<br />
<br />
"Existentially quantified type classes" by Stuckey, Sulzmann and Wazny (URL?)</div>Davesquehttps://wiki.haskell.org/index.php?title=GADTs_for_dummies&diff=56424GADTs for dummies2013-07-20T01:42:00Z<p>Davesque: </p>
<hr />
<div>[[Category:Tutorials]]<br />
[[Category:Language extensions]]<br />
<br />
For a long time, I didn't understand what GADTs were or how they could be used. It was sort of a conspiracy of silence &mdash; people who understood GADTs thought<br />
that everything was obvious and didn't need further explanation, but I still<br />
couldn't understand them.<br />
<br />
Now that I have an idea how it works, I think that it was really obvious. :) So, I want to share my understanding of GADTs. Maybe the way I realized how GADTs work could help<br />
someone else. See also [[Generalised algebraic datatype]]<br />
<br />
== Type functions ==<br />
<br />
A "data" declaration is a way to declare both type constructor and data<br />
constructors. For example,<br />
<br />
<haskell><br />
data Either a b = Left a | Right b<br />
</haskell><br />
<br />
declares type constructor "Either" and two data constructors "Left"<br />
and "Right". Ordinary Haskell functions works with data constructors:<br />
<br />
<haskell><br />
isLeft (Left a) = True<br />
isLeft (Right b) = False<br />
</haskell><br />
<br />
but there is also an analogous way to work with type constructors!<br />
<br />
<haskell><br />
type X a = Either a a<br />
</haskell><br />
<br />
declares a TYPE FUNCTION named "X". Its parameter "a" must be some type<br />
and it returns some type as its result. We can't use "X" on data values,<br />
but we can use it on type values. Type constructors declared with<br />
"data" statements and type functions declared with "type" statements<br />
can be used together to build arbitrarily complex types. In such<br />
"computations" type constructors serves as basic "values" and type<br />
functions as a way to process them.<br />
<br />
Indeed, type functions in Haskell are very limited compared to<br />
ordinary functions - they don't support pattern matching,<br />
nor multiple statements, nor recursion.<br />
<br />
== Hypothetical Haskell extension - Full-featured type functions ==<br />
<br />
Let's build a hypothetical Haskell extension that mimics, for type<br />
functions, the well-known ways to define ordinary functions, including<br />
pattern matching:<br />
<br />
<haskell><br />
type F [a] = Set a<br />
</haskell><br />
<br />
multiple statements (this is meaningful only in the presence of pattern matching):<br />
<br />
<haskell><br />
type F Bool = Char<br />
F String = Int<br />
</haskell><br />
<br />
and recursion (which again needs pattern matching and multiple statements):<br />
<br />
<haskell><br />
type F [a] = F a<br />
F (Map a b) = F b<br />
F (Set a) = F a<br />
F a = a<br />
</haskell><br />
<br />
As you may already have guessed, this last definition calculates a simple base type of arbitrarily-nested collections, e.g.: <br />
<br />
<haskell><br />
F [[[Set Int]]] = <br />
F [[Set Int]] =<br />
F [Set Int] = <br />
F (Set Int) =<br />
F Int =<br />
Int<br />
</haskell><br />
<br />
Let's not forget about statement guards:<br />
<br />
<haskell><br />
type F a | IsSimple a == TrueType = a<br />
</haskell><br />
<br />
Here we define type function F only for simple datatypes by using a<br />
guard type function "IsSimple":<br />
<br />
<haskell><br />
type IsSimple Bool = TrueType<br />
IsSimple Int = TrueType<br />
....<br />
IsSimple Double = TrueType<br />
IsSimple a = FalseType<br />
<br />
data TrueType = T<br />
data FalseType = F<br />
</haskell><br />
<br />
These definitions seem a bit odd, and while we are in imaginary land,<br />
let's consider a way to write this shorter:<br />
<br />
<haskell><br />
type F a | IsSimple a = a<br />
<br />
type IsSimple Bool<br />
IsSimple Int<br />
....<br />
IsSimple Double<br />
</haskell><br />
<br />
Here, we defined a list of simple types. The implied result of all<br />
written statements for "IsSimple" is True, and False for<br />
everything else. Essentially, "IsSimple" is a TYPE PREDICATE!<br />
<br />
I really love it! :) How about constructing a predicate that traverses a<br />
complex type trying to decide whether it contains "Int" anywhere?<br />
<br />
<haskell><br />
type HasInt Int<br />
HasInt [a] = HasInt a<br />
HasInt (Set a) = HasInt a<br />
HasInt (Map a b) | HasInt a<br />
HasInt (Map a b) | HasInt b<br />
</haskell><br />
<br />
or a type function that substitutes one type with another inside<br />
arbitrarily-deep types:<br />
<br />
<haskell><br />
type Replace t a b | t==a = b<br />
Replace [t] a b = [Replace t a b]<br />
Replace (Set t) a b = Set (Replace t a b)<br />
Replace (Map t1 t2) a b = Map (Replace t1 a b) (Replace t2 a b)<br />
Replace t a b = t<br />
</haskell><br />
<br />
== One more hypothetical extension - multi-value type functions ==<br />
<br />
Let's add more fun! We will introduce one more hypothetical Haskell<br />
extension - type functions that may have MULTIPLE VALUES. Say,<br />
<br />
<haskell><br />
type Collection a = [a]<br />
Collection a = Set a<br />
Collection a = Map b a<br />
</haskell><br />
<br />
So, "Collection Int" has "[Int]", "Set Int" and "Map String Int" as<br />
its values, i.e. different collection types with elements of type<br />
"Int".<br />
<br />
Pay attention to the last statement of the "Collection" definition, where<br />
we used the type variable "b" that was not mentioned on the left side,<br />
nor defined in any other way. Since it's perfectly possible for the<br />
"Collection" function to have multiple values, using some free variable on<br />
the right side that can be replaced with any type is not a problem<br />
at all. "Map Bool Int", "Map [Int] Int" and "Map Int Int" all are<br />
possible values of "Collection Int" along with "[Int]" and "Set Int".<br />
<br />
At first glance, it seems that multiple-value functions are meaningless - they<br />
can't be used to define datatypes, because we need concrete types here. But<br />
if we take another look, they can be useful to define type constraints and<br />
type families.<br />
<br />
We can also represent a multiple-value function as a predicate:<br />
<br />
<haskell><br />
type Collection a [a]<br />
Collection a (Set a)<br />
Collection a (Map b a)<br />
</haskell><br />
<br />
If you're familiar with Prolog, you should know that a predicate, in contrast to<br />
a function, is a multi-directional thing - it can be used to deduce any<br />
parameter from the other ones. For example, in this hypothetical definition:<br />
<br />
<haskell><br />
head | Collection Int a :: a -> Int<br />
</haskell><br />
<br />
we define a 'head' function for any Collection containing Ints.<br />
<br />
And in this, again, hypothetical definition:<br />
<br />
<haskell><br />
data Safe c | Collection c a = Safe c a<br />
</haskell><br />
<br />
we deduced element type 'a' from collection type 'c' passed as the<br />
parameter to the type constructor.<br />
<br />
<br />
<br />
== Back to real Haskell - type classes ==<br />
<br />
After reading about all of these glorious examples, you may be wondering<br />
"Why doesn't Haskell support full-featured type functions?" Hold your breath...<br />
Haskell already contains them, and GHC has implemented all of the<br />
capabilities mentioned above for more than 10 years! They were just named...<br />
TYPE CLASSES! Let's translate all of our examples to their language:<br />
<br />
<haskell><br />
class IsSimple a<br />
instance IsSimple Bool<br />
instance IsSimple Int<br />
....<br />
instance IsSimple Double<br />
</haskell><br />
<br />
The Haskell'98 standard supports type classes with only one parameter.<br />
That limits us to only defining type predicates like this one. But GHC and<br />
Hugs support multi-parameter type classes that allow us to define<br />
arbitrarily-complex type functions<br />
<br />
<haskell><br />
class Collection a c<br />
instance Collection a [a]<br />
instance Collection a (Set a)<br />
instance Collection a (Map b a)<br />
</haskell><br />
<br />
All of the "hypothetical" Haskell extensions we investigated earlier are<br />
actually implemented at the type class level!<br />
<br />
Pattern matching:<br />
<br />
<haskell><br />
instance Collection a [a]<br />
</haskell><br />
<br />
Multiple statements:<br />
<br />
<haskell><br />
instance Collection a [a]<br />
instance Collection a (Set a)<br />
</haskell><br />
<br />
Recursion:<br />
<br />
<haskell><br />
instance (Collection a c) => Collection a [c]<br />
</haskell><br />
<br />
Pattern guards:<br />
<br />
<haskell><br />
instance (IsSimple a) => Collection a (UArray a)<br />
</haskell><br />
<br />
<br />
<br />
Let's define a type class which contains any collection which uses Int in<br />
its elements or indexes:<br />
<br />
<haskell><br />
class HasInt a<br />
instance HasInt Int<br />
instance (HasInt a) => HasInt [a]<br />
instance (HasInt a) => HasInt (Map a b)<br />
instance (HasInt b) => HasInt (Map a b)<br />
</haskell><br />
<br />
<br />
Another example is a class that replaces all occurrences of 'a' with<br />
'b' in type 't' and return the result as 'res':<br />
<br />
<haskell><br />
class Replace t a b res<br />
instance Replace t a a t<br />
instance Replace [t] a b [Replace t a b]<br />
instance (Replace t a b res)<br />
=> Replace (Set t) a b (Set res)<br />
instance (Replace t1 a b res1, Replace t2 a b res2)<br />
=> Replace (Map t1 t2) a b (Map res1 res2)<br />
instance Replace t a b t<br />
</haskell><br />
<br />
You can compare it to the hypothetical definition we gave earlier.<br />
It's important to note that type class instances, as opposed to<br />
function statements, are not checked in order. Instead, the most<br />
_specific_ instance is automatically selected. So, in the Replace case, the<br />
last instance, which is the most general instance, will be selected only if all the others<br />
fail to match, which is what we want.<br />
<br />
In many other cases this automatic selection is not powerful enough<br />
and we are forced to use some artificial tricks or complain to the<br />
language developers. The two most well-known language extensions<br />
proposed to solve such problems are instance priorities, which allow<br />
us to explicitly specify instance selection order, and '/=' constraints,<br />
which can be used to explicitly prohibit unwanted matches:<br />
<br />
<haskell><br />
instance Replace t a a t<br />
instance (a/=b) => Replace [t] a b [Replace t a b]<br />
instance (a/=b, t/=[_]) => Replace t a b t<br />
</haskell><br />
<br />
You can check that these instances no longer overlap.<br />
<br />
<br />
In practice, type-level arithmetic by itself is not very useful. It becomes a<br />
fantastic tool when combined with another feature that type classes provide -<br />
member functions. For example:<br />
<br />
<haskell><br />
class Collection a c where<br />
foldr1 :: (a -> a -> a) -> c -> a<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
sum :: (Num a, Collection a c) => c -> a<br />
sum = foldr1 (+)<br />
</haskell><br />
<br />
<br />
I'll also be glad to see the possibility of using type classes in data<br />
declarations, like this:<br />
<br />
<haskell><br />
data Safe c = (Collection c a) => Safe c a<br />
</haskell><br />
<br />
but as far as I know, this is not yet implemented.<br />
<br />
<br />
UNIFICATION<br />
...<br />
<br />
<br />
<br />
== Back to GADTs ==<br />
<br />
If you are wondering how all of these interesting type manipulations relate to<br />
GADTs, here is the answer. As you know, Haskell contains highly<br />
developed ways to express data-to-data functions. We also know that<br />
Haskell contains rich facilities to write type-to-type functions in the form of<br />
"type" statements and type classes. But how do "data" statements fit into this<br />
infrastructure?<br />
<br />
My answer: they just define a type-to-data constructor translation. Moreover,<br />
this translation may give multiple results. Say, the following definition:<br />
<br />
<haskell><br />
data Maybe a = Just a | Nothing<br />
</haskell><br />
<br />
defines type-to-data constructors function "Maybe" that has a parameter<br />
"a" and for each "a" has two possible results - "Just a" and<br />
"Nothing". We can rewrite it in the same hypothetical syntax that was<br />
used above for multi-value type functions:<br />
<br />
<haskell><br />
data Maybe a = Just a<br />
Maybe a = Nothing<br />
</haskell><br />
<br />
Or how about this:<br />
<br />
<haskell><br />
data List a = Cons a (List a)<br />
List a = Nil<br />
</haskell><br />
<br />
and this:<br />
<br />
<haskell><br />
data Either a b = Left a<br />
Either a b = Right b<br />
</haskell><br />
<br />
But how flexible are "data" definitions? As you should remember, "type"<br />
definitions were very limited in their features, while type classes,<br />
on the other hand, were more developed than ordinary Haskell functions<br />
facilities. What about features of "data" definitions examined as sort of functions?<br />
<br />
On the one hand, they supports multiple statements and multiple results and<br />
can be recursive, like the "List" definition above. On the other, that's all -<br />
no pattern matching or even type constants on the left side and no guards.<br />
<br />
Lack of pattern matching means that the left side can contain only free type<br />
variables. That in turn means that the left sides of all "data" statements for a<br />
type will be essentially the same. Therefore, repeated left sides in<br />
multi-statement "data" definitions are omitted and instead of<br />
<br />
<haskell><br />
data Either a b = Left a<br />
Either a b = Right b<br />
</haskell><br />
<br />
we write just<br />
<br />
<haskell><br />
data Either a b = Left a<br />
| Right b<br />
</haskell><br />
<br />
<br />
And here we finally come to GADTs! It's just a way to define data types using<br />
pattern matching and constants on the left side of "data" statements!<br />
Let's say we want to do this:<br />
<br />
<haskell><br />
data T String = D1 Int<br />
T Bool = D2<br />
T [a] = D3 (a,a)<br />
</haskell><br />
<br />
<br />
We cannot do this using a standard data definition. So, now we must use a GADT definition:<br />
<br />
<haskell><br />
data T a where<br />
D1 :: Int -> T String<br />
D2 :: T Bool<br />
D3 :: (a,a) -> T [a]<br />
</haskell><br />
<br />
Amazed? After all, GADTs seem to be a really simple and obvious extension to<br />
data type definition facilities.<br />
<br />
<br />
<br />
<br />
<br />
<br />
<br />
The idea here is to allow a data constructor's return type to be specified<br />
directly:<br />
<br />
<haskell><br />
data Term a where<br />
Lit :: Int -> Term Int<br />
Pair :: Term a -> Term b -> Term (a,b)<br />
...<br />
</haskell><br />
<br />
In a function that performs pattern matching on Term, the pattern match gives<br />
type as well as value information. For example, consider this function:<br />
<br />
<haskell><br />
eval :: Term a -> a<br />
eval (Lit i) = i<br />
eval (Pair a b) = (eval a, eval b)<br />
...<br />
</haskell><br />
<br />
If the argument matches Lit, it must have been built with a Lit constructor,<br />
so type 'a' must be Int, and hence we can return 'i' (an Int) in the right<br />
hand side. The same thing applies to the Pair constructor.<br />
<br />
<br />
<br />
<br />
<br />
<br />
== Further reading ==<br />
<br />
The best paper on type level arithmetic using type classes I've seen<br />
is "Faking it: simulating dependent types in Haskell"<br />
( http://www.cs.nott.ac.uk/~ctm/faking.ps.gz ). Most of<br />
this article comes from his work.<br />
<br />
A great demonstration of type-level arithmetic is in the TypeNats package,<br />
which "defines type-level natural numbers and arithmetic operations on<br />
them including addition, subtraction, multiplication, division and GCD"<br />
( darcs get --partial --tag '0.1' http://www.eecs.tufts.edu/~rdocki01/typenats/ )<br />
<br />
I should also mention here Oleg Kiselyov's page on type-level<br />
programming in Haskell: http://okmij.org/ftp/Haskell/types.html<br />
<br />
<br />
There are plenty of GADT-related papers, but the best one for beginners<br />
is "Fun with phantom types"<br />
(http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf).<br />
Phantom types is another name of GADT. You should also know that this<br />
paper uses old GADT syntax. This paper is a must-read because it<br />
contains numerous examples of practical GADT usage - a theme completely<br />
omitted from my article.<br />
<br />
<br />
Other GADT-related papers:<br />
<br />
"Dynamic Optimization for Functional Reactive Programming using<br />
Generalized Algebraic Data Types"<br />
http://www.cs.nott.ac.uk/~nhn/Publications/icfp2005.pdf<br />
<br />
"Phantom types" (actually more scientific version of "Fun with phantom types")<br />
http://citeseer.ist.psu.edu/rd/0,606209,1,0.25,Download/http:qSqqSqwww.informatik.uni-bonn.deqSq~ralfqSqpublicationsqSqPhantom.ps.gz<br />
<br />
"Phantom types and subtyping" http://arxiv.org/ps/cs.PL/0403034<br />
<br />
"Existentially quantified type classes" by Stuckey, Sulzmann and Wazny (URL?)</div>Davesquehttps://wiki.haskell.org/index.php?title=GADTs_for_dummies&diff=56423GADTs for dummies2013-07-20T01:39:11Z<p>Davesque: </p>
<hr />
<div>[[Category:Tutorials]]<br />
[[Category:Language extensions]]<br />
<br />
For a long time, I didn't understand what GADTs were or how they could be used. It was sort of a conspiracy of silence - people who understood GADTs thought<br />
that everything was obvious and didn't need further explanation, but I still<br />
couldn't understand them.<br />
<br />
Now that I have an idea how it works, I think that it was really obvious. :) So, I want to share my understanding of GADTs. Maybe the way I realized how GADTs work could help<br />
someone else. See also [[Generalised algebraic datatype]]<br />
<br />
== Type functions ==<br />
<br />
A "data" declaration is a way to declare both type constructor and data<br />
constructors. For example,<br />
<br />
<haskell><br />
data Either a b = Left a | Right b<br />
</haskell><br />
<br />
declares type constructor "Either" and two data constructors "Left"<br />
and "Right". Ordinary Haskell functions works with data constructors:<br />
<br />
<haskell><br />
isLeft (Left a) = True<br />
isLeft (Right b) = False<br />
</haskell><br />
<br />
but there is also an analogous way to work with type constructors!<br />
<br />
<haskell><br />
type X a = Either a a<br />
</haskell><br />
<br />
declares a TYPE FUNCTION named "X". Its parameter "a" must be some type<br />
and it returns some type as its result. We can't use "X" on data values,<br />
but we can use it on type values. Type constructors declared with<br />
"data" statements and type functions declared with "type" statements<br />
can be used together to build arbitrarily complex types. In such<br />
"computations" type constructors serves as basic "values" and type<br />
functions as a way to process them.<br />
<br />
Indeed, type functions in Haskell are very limited compared to<br />
ordinary functions - they don't support pattern matching,<br />
nor multiple statements, nor recursion.<br />
<br />
== Hypothetical Haskell extension - Full-featured type functions ==<br />
<br />
Let's build a hypothetical Haskell extension that mimics, for type<br />
functions, the well-known ways to define ordinary functions, including<br />
pattern matching:<br />
<br />
<haskell><br />
type F [a] = Set a<br />
</haskell><br />
<br />
multiple statements (this is meaningful only in the presence of pattern matching):<br />
<br />
<haskell><br />
type F Bool = Char<br />
F String = Int<br />
</haskell><br />
<br />
and recursion (which again needs pattern matching and multiple statements):<br />
<br />
<haskell><br />
type F [a] = F a<br />
F (Map a b) = F b<br />
F (Set a) = F a<br />
F a = a<br />
</haskell><br />
<br />
As you may already have guessed, this last definition calculates a simple base type of arbitrarily-nested collections, e.g.: <br />
<br />
<haskell><br />
F [[[Set Int]]] = <br />
F [[Set Int]] =<br />
F [Set Int] = <br />
F (Set Int) =<br />
F Int =<br />
Int<br />
</haskell><br />
<br />
Let's not forget about statement guards:<br />
<br />
<haskell><br />
type F a | IsSimple a == TrueType = a<br />
</haskell><br />
<br />
Here we define type function F only for simple datatypes by using a<br />
guard type function "IsSimple":<br />
<br />
<haskell><br />
type IsSimple Bool = TrueType<br />
IsSimple Int = TrueType<br />
....<br />
IsSimple Double = TrueType<br />
IsSimple a = FalseType<br />
<br />
data TrueType = T<br />
data FalseType = F<br />
</haskell><br />
<br />
These definitions seem a bit odd, and while we are in imaginary land,<br />
let's consider a way to write this shorter:<br />
<br />
<haskell><br />
type F a | IsSimple a = a<br />
<br />
type IsSimple Bool<br />
IsSimple Int<br />
....<br />
IsSimple Double<br />
</haskell><br />
<br />
Here, we defined a list of simple types. The implied result of all<br />
written statements for "IsSimple" is True, and False for<br />
everything else. Essentially, "IsSimple" is a TYPE PREDICATE!<br />
<br />
I really love it! :) How about constructing a predicate that traverses a<br />
complex type trying to decide whether it contains "Int" anywhere?<br />
<br />
<haskell><br />
type HasInt Int<br />
HasInt [a] = HasInt a<br />
HasInt (Set a) = HasInt a<br />
HasInt (Map a b) | HasInt a<br />
HasInt (Map a b) | HasInt b<br />
</haskell><br />
<br />
or a type function that substitutes one type with another inside<br />
arbitrarily-deep types:<br />
<br />
<haskell><br />
type Replace t a b | t==a = b<br />
Replace [t] a b = [Replace t a b]<br />
Replace (Set t) a b = Set (Replace t a b)<br />
Replace (Map t1 t2) a b = Map (Replace t1 a b) (Replace t2 a b)<br />
Replace t a b = t<br />
</haskell><br />
<br />
== One more hypothetical extension - multi-value type functions ==<br />
<br />
Let's add more fun! We will introduce one more hypothetical Haskell<br />
extension - type functions that may have MULTIPLE VALUES. Say,<br />
<br />
<haskell><br />
type Collection a = [a]<br />
Collection a = Set a<br />
Collection a = Map b a<br />
</haskell><br />
<br />
So, "Collection Int" has "[Int]", "Set Int" and "Map String Int" as<br />
its values, i.e. different collection types with elements of type<br />
"Int".<br />
<br />
Pay attention to the last statement of the "Collection" definition, where<br />
we used the type variable "b" that was not mentioned on the left side,<br />
nor defined in any other way. Since it's perfectly possible for the<br />
"Collection" function to have multiple values, using some free variable on<br />
the right side that can be replaced with any type is not a problem<br />
at all. "Map Bool Int", "Map [Int] Int" and "Map Int Int" all are<br />
possible values of "Collection Int" along with "[Int]" and "Set Int".<br />
<br />
At first glance, it seems that multiple-value functions are meaningless - they<br />
can't be used to define datatypes, because we need concrete types here. But<br />
if we take another look, they can be useful to define type constraints and<br />
type families.<br />
<br />
We can also represent a multiple-value function as a predicate:<br />
<br />
<haskell><br />
type Collection a [a]<br />
Collection a (Set a)<br />
Collection a (Map b a)<br />
</haskell><br />
<br />
If you're familiar with Prolog, you should know that a predicate, in contrast to<br />
a function, is a multi-directional thing - it can be used to deduce any<br />
parameter from the other ones. For example, in this hypothetical definition:<br />
<br />
<haskell><br />
head | Collection Int a :: a -> Int<br />
</haskell><br />
<br />
we define a 'head' function for any Collection containing Ints.<br />
<br />
And in this, again, hypothetical definition:<br />
<br />
<haskell><br />
data Safe c | Collection c a = Safe c a<br />
</haskell><br />
<br />
we deduced element type 'a' from collection type 'c' passed as the<br />
parameter to the type constructor.<br />
<br />
<br />
<br />
== Back to real Haskell - type classes ==<br />
<br />
After reading about all of these glorious examples, you may be wondering<br />
"Why doesn't Haskell support full-featured type functions?" Hold your breath...<br />
Haskell already contains them, and GHC has implemented all of the<br />
capabilities mentioned above for more than 10 years! They were just named...<br />
TYPE CLASSES! Let's translate all of our examples to their language:<br />
<br />
<haskell><br />
class IsSimple a<br />
instance IsSimple Bool<br />
instance IsSimple Int<br />
....<br />
instance IsSimple Double<br />
</haskell><br />
<br />
The Haskell'98 standard supports type classes with only one parameter.<br />
That limits us to only defining type predicates like this one. But GHC and<br />
Hugs support multi-parameter type classes that allow us to define<br />
arbitrarily-complex type functions<br />
<br />
<haskell><br />
class Collection a c<br />
instance Collection a [a]<br />
instance Collection a (Set a)<br />
instance Collection a (Map b a)<br />
</haskell><br />
<br />
All of the "hypothetical" Haskell extensions we investigated earlier are<br />
actually implemented at the type class level!<br />
<br />
Pattern matching:<br />
<br />
<haskell><br />
instance Collection a [a]<br />
</haskell><br />
<br />
Multiple statements:<br />
<br />
<haskell><br />
instance Collection a [a]<br />
instance Collection a (Set a)<br />
</haskell><br />
<br />
Recursion:<br />
<br />
<haskell><br />
instance (Collection a c) => Collection a [c]<br />
</haskell><br />
<br />
Pattern guards:<br />
<br />
<haskell><br />
instance (IsSimple a) => Collection a (UArray a)<br />
</haskell><br />
<br />
<br />
<br />
Let's define a type class which contains any collection which uses Int in<br />
its elements or indexes:<br />
<br />
<haskell><br />
class HasInt a<br />
instance HasInt Int<br />
instance (HasInt a) => HasInt [a]<br />
instance (HasInt a) => HasInt (Map a b)<br />
instance (HasInt b) => HasInt (Map a b)<br />
</haskell><br />
<br />
<br />
Another example is a class that replaces all occurrences of 'a' with<br />
'b' in type 't' and return the result as 'res':<br />
<br />
<haskell><br />
class Replace t a b res<br />
instance Replace t a a t<br />
instance Replace [t] a b [Replace t a b]<br />
instance (Replace t a b res)<br />
=> Replace (Set t) a b (Set res)<br />
instance (Replace t1 a b res1, Replace t2 a b res2)<br />
=> Replace (Map t1 t2) a b (Map res1 res2)<br />
instance Replace t a b t<br />
</haskell><br />
<br />
You can compare it to the hypothetical definition we gave earlier.<br />
It's important to note that type class instances, as opposed to<br />
function statements, are not checked in order. Instead, the most<br />
_specific_ instance is automatically selected. So, in the Replace case, the<br />
last instance, which is the most general instance, will be selected only if all the others<br />
fail to match, which is what we want.<br />
<br />
In many other cases this automatic selection is not powerful enough<br />
and we are forced to use some artificial tricks or complain to the<br />
language developers. The two most well-known language extensions<br />
proposed to solve such problems are instance priorities, which allow<br />
us to explicitly specify instance selection order, and '/=' constraints,<br />
which can be used to explicitly prohibit unwanted matches:<br />
<br />
<haskell><br />
instance Replace t a a t<br />
instance (a/=b) => Replace [t] a b [Replace t a b]<br />
instance (a/=b, t/=[_]) => Replace t a b t<br />
</haskell><br />
<br />
You can check that these instances no longer overlap.<br />
<br />
<br />
In practice, type-level arithmetic by itself is not very useful. It becomes a<br />
fantastic tool when combined with another feature that type classes provide -<br />
member functions. For example:<br />
<br />
<haskell><br />
class Collection a c where<br />
foldr1 :: (a -> a -> a) -> c -> a<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
sum :: (Num a, Collection a c) => c -> a<br />
sum = foldr1 (+)<br />
</haskell><br />
<br />
<br />
I'll also be glad to see the possibility of using type classes in data<br />
declarations, like this:<br />
<br />
<haskell><br />
data Safe c = (Collection c a) => Safe c a<br />
</haskell><br />
<br />
but as far as I know, this is not yet implemented.<br />
<br />
<br />
UNIFICATION<br />
...<br />
<br />
<br />
<br />
== Back to GADTs ==<br />
<br />
If you are wondering how all of these interesting type manipulations relate to<br />
GADTs, here is the answer. As you know, Haskell contains highly<br />
developed ways to express data-to-data functions. We also know that<br />
Haskell contains rich facilities to write type-to-type functions in the form of<br />
"type" statements and type classes. But how do "data" statements fit into this<br />
infrastructure?<br />
<br />
My answer: they just define a type-to-data constructor translation. Moreover,<br />
this translation may give multiple results. Say, the following definition:<br />
<br />
<haskell><br />
data Maybe a = Just a | Nothing<br />
</haskell><br />
<br />
defines type-to-data constructors function "Maybe" that has a parameter<br />
"a" and for each "a" has two possible results - "Just a" and<br />
"Nothing". We can rewrite it in the same hypothetical syntax that was<br />
used above for multi-value type functions:<br />
<br />
<haskell><br />
data Maybe a = Just a<br />
Maybe a = Nothing<br />
</haskell><br />
<br />
Or how about this:<br />
<br />
<haskell><br />
data List a = Cons a (List a)<br />
List a = Nil<br />
</haskell><br />
<br />
and this:<br />
<br />
<haskell><br />
data Either a b = Left a<br />
Either a b = Right b<br />
</haskell><br />
<br />
But how flexible are "data" definitions? As you should remember, "type"<br />
definitions were very limited in their features, while type classes,<br />
on the other hand, were more developed than ordinary Haskell functions<br />
facilities. What about features of "data" definitions examined as sort of functions?<br />
<br />
On the one hand, they supports multiple statements and multiple results and<br />
can be recursive, like the "List" definition above. On the other, that's all -<br />
no pattern matching or even type constants on the left side and no guards.<br />
<br />
Lack of pattern matching means that the left side can contain only free type<br />
variables. That in turn means that the left sides of all "data" statements for a<br />
type will be essentially the same. Therefore, repeated left sides in<br />
multi-statement "data" definitions are omitted and instead of<br />
<br />
<haskell><br />
data Either a b = Left a<br />
Either a b = Right b<br />
</haskell><br />
<br />
we write just<br />
<br />
<haskell><br />
data Either a b = Left a<br />
| Right b<br />
</haskell><br />
<br />
<br />
And here we finally come to GADTs! It's just a way to define data types using<br />
pattern matching and constants on the left side of "data" statements!<br />
Let's say we want to do this:<br />
<br />
<haskell><br />
data T String = D1 Int<br />
T Bool = D2<br />
T [a] = D3 (a,a)<br />
</haskell><br />
<br />
<br />
We cannot do this using a standard data definition. So, now we must use a GADT definition:<br />
<br />
<haskell><br />
data T a where<br />
D1 :: Int -> T String<br />
D2 :: T Bool<br />
D3 :: (a,a) -> T [a]<br />
</haskell><br />
<br />
Amazed? After all, GADTs seem to be a really simple and obvious extension to<br />
data type definition facilities.<br />
<br />
<br />
<br />
<br />
<br />
<br />
<br />
The idea here is to allow a data constructor's return type to be specified<br />
directly:<br />
<br />
<haskell><br />
data Term a where<br />
Lit :: Int -> Term Int<br />
Pair :: Term a -> Term b -> Term (a,b)<br />
...<br />
</haskell><br />
<br />
In a function that performs pattern matching on Term, the pattern match gives<br />
type as well as value information. For example, consider this function:<br />
<br />
<haskell><br />
eval :: Term a -> a<br />
eval (Lit i) = i<br />
eval (Pair a b) = (eval a, eval b)<br />
...<br />
</haskell><br />
<br />
If the argument matches Lit, it must have been built with a Lit constructor,<br />
so type 'a' must be Int, and hence we can return 'i' (an Int) in the right<br />
hand side. The same thing applies to the Pair constructor.<br />
<br />
<br />
<br />
<br />
<br />
<br />
== Further reading ==<br />
<br />
The best paper on type level arithmetic using type classes I've seen<br />
is "Faking it: simulating dependent types in Haskell"<br />
( http://www.cs.nott.ac.uk/~ctm/faking.ps.gz ). Most of<br />
this article comes from his work.<br />
<br />
A great demonstration of type-level arithmetic is in the TypeNats package,<br />
which "defines type-level natural numbers and arithmetic operations on<br />
them including addition, subtraction, multiplication, division and GCD"<br />
( darcs get --partial --tag '0.1' http://www.eecs.tufts.edu/~rdocki01/typenats/ )<br />
<br />
I should also mention here Oleg Kiselyov's page on type-level<br />
programming in Haskell: http://okmij.org/ftp/Haskell/types.html<br />
<br />
<br />
There are plenty of GADT-related papers, but the best one for beginners<br />
is "Fun with phantom types"<br />
(http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf).<br />
Phantom types is another name of GADT. You should also know that this<br />
paper uses old GADT syntax. This paper is a must-read because it<br />
contains numerous examples of practical GADT usage - a theme completely<br />
omitted from my article.<br />
<br />
<br />
Other GADT-related papers:<br />
<br />
"Dynamic Optimization for Functional Reactive Programming using<br />
Generalized Algebraic Data Types"<br />
http://www.cs.nott.ac.uk/~nhn/Publications/icfp2005.pdf<br />
<br />
"Phantom types" (actually more scientific version of "Fun with phantom types")<br />
http://citeseer.ist.psu.edu/rd/0,606209,1,0.25,Download/http:qSqqSqwww.informatik.uni-bonn.deqSq~ralfqSqpublicationsqSqPhantom.ps.gz<br />
<br />
"Phantom types and subtyping" http://arxiv.org/ps/cs.PL/0403034<br />
<br />
"Existentially quantified type classes" by Stuckey, Sulzmann and Wazny (URL?)</div>Davesquehttps://wiki.haskell.org/index.php?title=Error_vs._Exception&diff=54865Error vs. Exception2012-12-07T03:12:19Z<p>Davesque: /* Examples */ Some style and wording edits in first paragraph.</p>
<hr />
<div>There has been confusion about the distinction between [[error]]s and [[exception]]s for a long time,<br />
repeated threads in Haskell-Cafe and more and more packages that handle errors and exceptions or something between.<br />
Although both terms are related and sometimes hard to distinguish, it is important to do it carefully.<br />
This is like the confusion between [[Parallelism vs. Concurrency|parallelism and concurrency]].<br />
<br />
The first problem is that "exception" seems to me to be the historically younger term.<br />
Before there were only "errors", independent of whether they were programming, I/O or user errors.<br />
In this article we use the term '''exception''' for expected but irregular situations at runtime<br />
and the term '''error''' for mistakes in the running program that can be resolved only by fixing the program.<br />
We do not want to distinguish between different ways of representing exceptions:<br />
<hask>Maybe</hask>, <hask>Either</hask>, exceptions in <hask>IO</hask> monad, or return codes,<br />
they all represent exceptions and are worth considering for exception handling.<br />
<br />
The history may have led to the identifiers we find today in the Haskell language and standard Haskell modules.<br />
<br />
* Exceptions: <hask>Prelude.catch</hask>, <hask>Control.Exception.catch</hask>, <hask>Control.Exception.try</hask>, <hask>IOError</hask>, <hask>Control.Monad.Error</hask><br />
* Errors: <hask>error</hask>, <hask>assert</hask>, <hask>Control.Exception.catch</hask>, <hask>Debug.Trace.trace</hask><br />
<br />
Note, that the <hask>catch</hask> function from <hask>Prelude</hask> handles exclusively exceptions,<br />
whereas its counterpart from <hask>Control.Exception</hask> also catches certain kinds of undefined values.<br />
<haskell><br />
Prelude> catch (error "bla") (\msg -> putStrLn $ "caught " ++ show msg)<br />
*** Exception: bla<br />
<br />
Prelude> Control.Exception.catch (error "bla") (\msg -> putStrLn $ "caught " ++ show (msg::Control.Exception.SomeException))<br />
caught bla<br />
</haskell><br />
This is unsafe, since Haskell's <hask>error</hask> is just sugar for <hask>undefined</hask>, that shall help spotting a programming error.<br />
A program should work as well when all <hask>error</hask>s and <hask>undefined</hask>s are replaced by infinite loops.<br />
However infinite loops in general cannot be caught, whereas calls to sugared functions like <hask>error</hask> can.<br />
<br />
Even more confusion was initiated by the Java programming language<br />
to use the term "exceptions" for programming errors like the <code>NullPointerException</code><br />
and introducing the distinction between<br />
[http://java.sun.com/docs/books/tutorial/essential/exceptions/runtime.html checked and unchecked exceptions].<br />
<br />
<br />
== Examples ==<br />
<br />
Let's give some examples for explaining the difference between errors and exceptions and why the distinction is important.<br />
<br />
First, consider a compiler like [[GHC]].<br />
If you feed it a program that contains invalid syntax or inconsistent types, it emits a description of the problem.<br />
Such occurrences are considered to be exceptions.<br />
GHC anticipates bad syntax and mismatched types and handles them by generating useful messages for the user.<br />
However, if GHC spits out a message like "Panic! This should not happen: ... Send a bug report to ghc@haskell.org", then you've encountered a situation which indicates a flaw in GHC.<br />
This would be considered an error.<br />
It cannot be handled by GHC or by the user.<br />
The error message, "Panic!...", is only useful to the GHC developers in fixing the problem.<br />
<br />
Ok, these are possible reactions to user input.<br />
Now a more difficult question:<br />
How should GHC handle corruptions in the files it has generated itself like the interface (.hi) and object files (.o)?<br />
These corruptions can be introduced easily by the user by editing the files in a simple text editor,<br />
or by network problems or by exchanging files between operating systems or different GHC versions, or by virus programs.<br />
Thus GHC must be prepared for them, which means, it must generate and handle exceptions here.<br />
It must tell the user at least that there is some problem with the read file.<br />
Next question: Must GHC also be prepared for corrupt memory or damages in the CPU?<br />
Good question. According to the above definition corrupt memory is an exception, not an error.<br />
However, GHC cannot do much about such situations. So I don't think it must be prepared for that.<br />
<br />
<!-- User enters number as string, pass to function that expects non-negative number --><br />
<br />
Now we proceed with two examples that show, what happens if you try to treat errors like exceptions:<br><br />
I was involved in the development of a library that was written in C++.<br />
One of the developers told me, that the developers are divided into the ones who like exceptions<br />
and the other ones who prefer return codes.<br />
As it seem to me, the friends of return codes won.<br />
However, I got the impression that they debated the wrong point:<br />
Exceptions and return codes are equally expressive, they should however not be used to describe errors.<br />
Actually the return codes contained definitions like ARRAY_INDEX_OUT_OF_RANGE.<br />
But I wondered: How shall my function react, when it gets this return code from a subroutine?<br />
Shall it send a mail to its programmer?<br />
It could return this code to its caller in turn, but it will also not know how to cope with it.<br />
Even worse, since I cannot make assumptions about the implementation of a function,<br />
I have to expect an ARRAY_INDEX_OUT_OF_RANGE from every subroutine.<br />
My conclusion is, that ARRAY_INDEX_OUT_OF_RANGE is a (programming) error.<br />
It cannot be handled or fixed at runtime, it can only be fixed by its developer.<br />
Thus there should be no according return code, but instead there should be <code>assert</code>s.<br />
<br />
The second example is a library for advanced arithmetic in Modula-3.<br />
I decided to use exceptions for signalling problems.<br />
One of the exceptions was VectorSizeMismatch,<br />
that was raised whenever two vectors of different sizes should be added or multiplied by a scalar product.<br />
However I found, that quickly almost every function in the library could potentially raise this exception<br />
and Modula-3 urges you to declare all potential exceptions.<br />
(However, ignoring potential exceptions only yields a compiler warning, that can even be suppressed.)<br />
I also noticed that due to the way I generated and combined the vectors and matrices<br />
the sizes would always match.<br />
Thus in case of a mismatch this means, there is not a problem with user input but with my program.<br />
Consequently, I removed this exception and replaced the checks by <code>ASSERT</code>.<br />
These <code>ASSERT</code>s can be disabled by a compiler switch for efficiency concerns.<br />
A correct program fulfils all <code>ASSERT</code>s and thus it does not make a difference<br />
whether they are present in the compiled program or not.<br />
In a faulty program the presence of <code>ASSERT</code>s only controls the way a program fails:<br />
either by giving wrong results or segmentation faults.<br />
<br />
With the new handling of vector size compatibility,<br />
if the operands of a vector addition originate from user input,<br />
then you have to check that their sizes match before you call vector addition.<br />
However this is a cheap check.<br />
Thus if you want another criterion for distinction of errors and exceptions:<br />
Errors can be prevented by (cheap) checks in advance,<br />
whereas exceptions can only be handled after a risky action was run.<br />
You can easily check for array indices being within array bounds, pointers for being not <code>NULL</code>,<br />
divisors for being not zero before calling according functions.<br />
In many cases you will not need those checks,<br />
because e.g. you have a loop traversing all valid indices of an array,<br />
and consequently you know that every index is allowed.<br />
You do not need to check exceptions afterwards.<br />
In contrast to that, memory full, disk full, file not existing, file without write permission<br />
and even overflows are clearly exceptions.<br />
Even if you check that there is enough memory available before allocating,<br />
the required chunk of memory might just be allocated by someone else between your memory check and your allocation.<br />
The file permission might be just changed between checking the permission and writing to the file.<br />
Permissions might even change while you write.<br />
Overflows are deterministic, but in order to prevent an overflow say for a multiplication,<br />
you have to reimplement the multiplication in an overflow-proof way.<br />
This will be slower than the actual multiplication.<br />
(Processors always show overflows by flags,<br />
but almost none of the popular high-level languages allows to query this information.)<br />
<br />
My conclusion is that (programming) errors can only be handled by the programmer,<br />
not by the running program.<br />
Thus the term "error handling" sounds contradictory to me.<br />
However supporting a programmer with finding errors (bugs) in their programs is a good thing.<br />
I just wouldn't call it "error handling" but "debugging".<br />
An important example in Haskell is the module <hask>Debug.Trace</hask>. It provides the function <hask>trace</hask> that looks like a non-I/O function<br />
but actually outputs something on the console.<br />
It is natural that debugging functions employ hacks.<br />
For finding a programming error it would be inappropriate to transform the program code<br />
to allow I/O in a set of functions that do not need it otherwise.<br />
The change would only persist until the bug is detected and fixed.<br />
Summarized, hacks in debugging functions<br />
are necessary for quickly finding problems without large restructuring of the program<br />
and they are not problematic, because they only exist until the bug is removed.<br />
<br />
Different from that exceptions are things you cannot fix in advance.<br />
You will always have to live with files that cannot be found and user input that is malformed.<br />
You can insist that the user does not hit the X key, but your program has to be prepared to receive a "X key pressed" message nonetheless.<br />
Thus exceptions belong to the program and<br />
the program must be adapted to treat exceptional values where they can occur.<br />
No hacks can be accepted for exception handling.<br />
<br />
== When exceptions become errors ==<br />
<br />
Another issue that makes distinction between exceptions and errors difficult is,<br />
that sometimes the one gets converted into the other one.<br />
<br />
It is an error to not handle an exception.<br />
If a file cannot be opened you must respect that result.<br />
You can proceed as if the file could be opened, though.<br />
If you do so you might crash the machine<br />
or the runtime system terminates your program.<br />
All of these effects are possible consequences of a (programming) error.<br />
Again, it does not matter whether the exceptional situation is signaled by a return code that you ignore or an IO exception for which you did not run a <hask>catch</hask>.<br />
<br />
== When errors become exceptions ==<br />
<br />
Often there is criticism about the distinction between errors and exceptions<br />
because there are software architectures<br />
where even programming errors of a part shall not crash a larger piece of software.<br />
Typical examples are:<br />
A process in an operating system shall not crash the whole system if it crashes itself.<br />
A buggy browser plugin shall not terminate the browser.<br />
A corrupt CGI script shall not bring the web server down, where it runs on.<br />
<br />
In these cases errors are handled like exceptions.<br />
But there is no reason to dismiss the distinction of errors and exceptions, at all.<br />
Obviously there are levels, and when crossing level boundaries it is ok to turn an error into an exception.<br />
The part that contains an error cannot do anything to recover from it.<br />
Also the next higher level cannot fix it, but it can restrict the damage.<br />
Within one encapsulated part of an architecture errors and exceptions shall be strictly separated.<br />
(Or put differently: If at one place you think you have to handle an error like an exception,<br />
why not dividing the program into two parts at this position? :-) )<br />
<br />
There is an important reason to not simply catch an error and proceed as if it were only an exception:<br />
The error might have corrupted some data and there is no general way to recover from that.<br />
Say, after detecting an error you might want to close a file that you were working on.<br />
But since you are coping with an error, something you did not foresee,<br />
you cannot know whether the file was already closed again or never opened.<br />
So it is better to just abort the program.<br />
<br />
The next higher level, the shell calling your program or the browser calling your plugin,<br />
shall have registered what has been opened and allocated and can reliably free those resources.<br />
<br />
<br />
== Errors and type system ==<br />
<br />
It is generally considered, that errors in a program imply a lack in the type system. If the type system would be strong enough and the programmers would be patient enough to work out the proofs imposed by library functions, then there would be no errors in programs at all, only exceptions.<br />
<br />
An alternative to extending the type system to [[dependent type]] system that allows for a wide range of proofs<br />
is the [[Extended Static Checking]].<br />
For example:<br />
<haskell><br />
{-# CONTRACT head :: { xs | not (null xs) } -> Ok #-}<br />
head :: [a] -> a<br />
head [] = error "head: empty list"<br />
head (x:_) = x<br />
</haskell><br />
<br />
When there is a pre-condition (or a contract) like here, it is a programming error to give an empty list to <hask>head</hask>. This means that checking if the list is empty must be done before the call. It has to statically deductible from the call site.<br />
<br />
If you write a function and cannot prove that you will not call head on the empty list then either you check before calling, or you use a safe-head function like <hask>viewL :: [a] -> Maybe (a, [a])</hask> or a <hask>case xs of x:_ -> doSomethingWithHead a; [] -> doSomethingElse</hask> or you add a pre-condition to your function.<br />
<br />
These contracts somehow look like the exception declarations, but they specify something about preconditions, not about possible results. There would be no sense to give the contracts names in order to handle different ways of violating the contracts after the function has been called with inappropriate arguments.<br />
<br />
== Call stacks ==<br />
<br />
Both for errors and exceptions some kind of call stack might be helpful to be reported to the programmer or user, respectively.<br />
However the call stacks for programmers (for debugging) noticably differ from those for users generated as result of an exception.<br />
<br />
For errors we might prefer something like:<br />
<br />
Prelude.head:42:23: empty list<br />
when calling recursively MyModule.scan.go:2009:12 and MyModule.scan.view:2009:7<br />
when calling MyGUI.promptString:1234:321<br />
... many more details ...<br />
<br />
whereas users would certainly more like to see<br />
<br />
Program could not be started,<br />
because Config file could not be read<br />
because Config file does not exist in dir0, dir1, dir2<br />
<br />
but the exception handler may also decide to use a default configuration instead or ask the user, how to proceed.<br />
<br />
== Escaping from control structures ==<br />
<br />
In imperative languages we often find statements that escape from a control structure.<br />
These escapers are refered to as exceptions, as well.<br />
E.g. in C/C++/Java <code>break</code> escapes <code>for</code> loops and <code>return</code> escapes functions and methods.<br />
Analogously in Modula-3 <code>EXIT</code> escapes <code>LOOP</code>s<br />
and <code>RETURN</code> escapes <code>PROCEDURE</code>s.<br />
The analogy between these statements and using the explicit exception handling mechanism of the particular language<br />
is also helpful in order to describe the interaction between these statements and handling of regular exceptions.<br />
E.g. what exception handlers and resource deallocators shall be run when you leave a loop or function using <code>break</code>?<br />
Analogously exceptions can also be used to escape from custom control structures<br />
(yeah, higher order functions are also possible in imperative languages)<br />
or deep recursive searches.<br />
In imperative languages exceptions are often implemented in a way that is especially efficient<br />
when deep recursions have to be aborted.<br />
<br />
You might debate intensively about whether using exceptions for escaping control structures is abuse of exceptions or not.<br />
At least escaping from control structures is more exception than error.<br />
Escaping from a control structure is just the irregular case with respect to the regular case of looping/descending in recursion.<br />
In Haskell, when you use exception monads like <code>Control.Monad.Exception.Synchronous</code> or <code>Control.Monad.Error</code>,<br />
exceptions are just an automated handling of return codes.<br />
<br />
<br />
== See also ==<br />
<br />
* [[Error]]<br />
* [[Exception]]<br />
<br />
<br />
''This article is written by Henning Thielemann. Other authors may use the terms 'error' and 'exceptions' in different ways or do not distinguish them at all.''<br />
<br />
<br />
[[Category:Idioms]]</div>Davesque