Unverified Commit 58d5344e authored by Philip K.'s avatar Philip K. 🌝
Browse files

system-f: wrote up initial draft

parent ccf0b870
\section{System-F \hfill 8 Punkte}
\section{System F \hfill 8 Punkte}
In Funktionalen Programmiersprachen werden Maybe Datentypen benutzt um
eine Berechnung mit Fehlermöglichkeit darzustellen. Dieses kann in
System F mit dem Typen \[ \mathbb{M}a := \forall r \,.\, (a \rightarrow r)
\rightarrow r \rightarrow r \] kodiert werden. Nehmen Sie zudem an,
dass Listen den Typ \[ \mathbb{L}a := \forall r \,.\, r \rightarrow (a
\rightarrow r \rightarrow r) \rightarrow r \] besitzt.
\item \points{2}
\item \points{5}
\item \points{1}
\item Definieren \points{2} Sie die Konstruktoren für
"`$\mathrm{some} : \forall a \,.\, a \rightarrow \mathbb{M}a$"' und
"`$\mathrm{none} : \forall a \,.\, \mathbb{M}a$"' (d.h. geben sie die
Lambda-Terme an).
\item Sei \points{5}
$t : \forall a \,.\, \mathbb{L}a \rightarrow \mathbb{M}a$ definiert
\[ t = \lambda l \,.\, l \; \mathrm{none}\;(\lambda xq\,.\,
\mathrm{some}\;x) \] Geben Sie die Typeherleitung in System F für
\[ \{ \mathrm{some} : \forall a \,.\, a \rightarrow \mathbb{M}a,
\mathrm{none} : \forall a \,.\, \mathbb{M}a \} \vdash t : \forall a
\,.\, \mathbb{L}a \rightarrow \mathbb{M}a \]
\item Welche \points{1} bekannte Funktion auf Listen stellt $t$ dar?
%%% Local Variables:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment