Commit 80ab5945e5e1417efdcfa7098d9aea5592250401 - gcct

Added a few more code examples Getty Ritter 9 years ago

1 changed file(s) with 32 addition(s) and 4 deletion(s). Collapse all Expand all

+32

-4

gcct.tex less more

128	128
129	129	Copatterns are also practically expressive, as in this concise
130	130	and readable definition of the fibonacci numbers in terms of
131		the \dual{\texttt{merge}} expression:
132
133		{\color{NavyBlue}
134		\begin{verbatim}
	131	the \dualtt{merge} expression:
	132
	133	{\color{NavyBlue}
	134	\begin{verbatim}
	135	codata Stream a
	136	= head a
	137	& tail (Stream a)
	138
	139	zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
	140	zipWith f s1 s2 = merge x from
	141	head x <- f (head s1) (head s2)
	142	tail x <- zipWith f (tail s1) (tail s2)
	143
135	144	fibs : Stream Int
136	145	fibs = merge x from
137	146	head x <- 0

253	262	extracted using the projection \dualtt{contents}. However, if the value
254	263	contained in the ``record'' is an \texttt{Int}, we have a second projection
255	264	available to us: we can also use \dualtt{isZero} to project out a boolean.
	265
	266	In fact, because of the type machinery afforded us by GCCTs, we can
	267	actually collapse both \dualtt{mkStringW} and \dualtt{mkIntW} into a
	268	single function, \dualtt{mkWrapper}, like so:
	269
	270	{\color{NavyBlue}
	271	\begin{verbatim}
	272	mkWrapper : a -> Wrapper a
	273	mkWrapper x = merge r from
	274	contents r <- x
	275	isZero r <- x == 0
	276	\end{verbatim}
	277	}
	278
	279	The reason this is valid is that, like with GADTs, copattern matching on
	280	\dualtt{isZero} gives us extra type information about \dualtt{x}, and so
	281	will only be a valid branch when \dualtt{mkWrapper} is called with a
	282	value of type \dualtt{Int}; otherwise it is merely a redundant branch
	283	and is ignored.
256	284
257	285	\subsection{Finite State Automata}
258	286