~fgaz/bachelor-thesis

b6cf95aceaed9f8f2b88f7d7faee690db0dbbcf6 — Francesco Gazzetta 1 year, 1 month ago ceafff7 master v1.0
Some more
2 files changed, 4 insertions(+), 0 deletions(-)

M Gazzetta_Francesco_Informatica_19.tex
M content.tex
M Gazzetta_Francesco_Informatica_19.tex => Gazzetta_Francesco_Informatica_19.tex +2 -0
@@ 35,6 35,8 @@
  \mainmatter

    \tableofcontents
    \vspace*{\fill}
    Note: the \LaTeX{} source from which this document was generated, along with eventual future corrections and improvements, can be found in the repository located at \url{https://git.sr.ht/~fgaz/bachelor-thesis/} and mirrored at \url{https://github.com/fgaz/bachelor-thesis/}.
    \clearpage



M content.tex => content.tex +2 -0
@@ 33,6 33,8 @@ GADTs (Generalized Algebraic Data Types) are a powerful generalization of Haskel
An explicit signature can be strictly more expressive than the standard syntax, since it can, for example, restrict the type variables of the return type to a specific instantiation depending on the constructor.
Similarly, given a type variable instantiation, we can know the type constructor that was used, or at least restrict the subset of possible ones.

In general, GADTs can be used to encode properties of the data in its type and enforce invariants in functions.

To briefly remind the reader of the usefulness of GADTs, an example follows:

\begin{lstlisting}[caption=A GADT describing a simple language with ints and pairs]