Skip to content

Commit 5a1bc36

Browse files
committed
Add GADTs section
1 parent 9995c31 commit 5a1bc36

File tree

1 file changed

+28
-0
lines changed

1 file changed

+28
-0
lines changed

haskell-exts-cs.tex

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,5 +110,33 @@ \section{Generalized Algebraic Datatypes
110110
\begin{ldesc}
111111
\li[enabling] \C{\{-\# LANGUAGE GADTs\#-\}}
112112
\end{ldesc}\\[1ex]
113+
\begin{tabular}{CC}
114+
\theads{GADT}{regular data definition}
115+
\\
116+
data Maybe a where~~~~~~~~~~ & data~Maybe~a \\
117+
~~Nothing~::~Maybe~a & ~~=~Nothing \\
118+
~~Just~~~~::~a~->~Maybe~a & ~~|~Just~a \\
119+
\\
120+
data List a where & data List a \\
121+
~~Nil~~::~List a & ~~= Nil \\
122+
~~Cons~::~a -> List a -> List a & ~~| Cons a (List a) \\
123+
\\
124+
data [a] where & data [a] = [] | a:[a] \\
125+
~~[]~~::~[a] & ~~\rotatebox{90}{$\Rsh$}\textnormal{\footnotesize ~(not real Haskell)} \\
126+
~~(:)~::~a -> [a] -> [a] & \\
127+
\\
128+
data Thing a where & \textnormal{regular defn.~impossible} \\
129+
~~Thing ::~a -> Thing a & \\
130+
~~AnInt ::~Int -> Thing Int & \\
131+
~~ABool ::~Bool -> Thing Bool & \\
132+
\\
133+
data Nat where & data Nat = Z | S Nat \\
134+
~~Z~::~Nat & \\
135+
~~S~::~Nat -> Nat & \\
136+
\\
137+
data Vec n a where & \textnormal{regular defn.~impossible} \\
138+
~~Nil~~~::~Vec Z a & \\
139+
~~(:::)~::~a -> Vec n a -> Vec (S n) a \hspace{-8ex} & \\
140+
\end{tabular}
113141

114142
\end{document}

0 commit comments

Comments
 (0)